Clarified A definitions.

2 files changed, 20 insertions, 29 deletions

diff --git a/src/a.tex b/src/a.tex
index b2bd899..0dac426 100644
--- a/src/a.tex
+++ b/src/a.tex
@@ -167,7 +167,7 @@ lost, but eventually the atomic sequence can complete.  We restricted
 the length of LR/SC sequences to fit within 64 contiguous instruction
 bytes in the base ISA to avoid undue restrictions on instruction cache
 and TLB size and associativity.  Similarly, we disallowed other loads
-and stores within the sequences to avoid restrictions on data cache
+and stores within the sequences to avoid restrictions on data-cache
 associativity.  The restrictions on branches and jumps limits the time
 that can be spent in the sequence.  Floating-point operations and
 integer multiply/divide were disallowed to simplify the operating
@@ -178,30 +178,27 @@ Although software is not forbidden from using LR/SC sequences that do not meet
 the forward-progress constraints, portable software must detect the case that
 the sequence repeatedly fails, then fall back to an alternate code sequence
 that does not run afoul of the forward-progress constraints.
-Implementations are permitted to simply always fail any LR/SC sequences that do
-not meet the forward-progress guarantees.
+Implementations are permitted to simply always fail any LR/SC sequence that does
+not meet the forward-progress guarantee.
 \end{commentary}
 
-Certain LR/SC sequences that do not meet the forward progress
-guarantees may succeed on some implementations.  An implementation can
-reserve an arbitrary subset of the memory space on each LR.  An SC may
-succeed if no store from another hart to the address range reserved by
-the LR can be observed to have occurred between the LR and the SC, and
-if there is no other SC between the LR and itself in program order.
-Note this LR might have had a different address argument, but reserved
-the SC's address as part of the memory subset.  Following this model,
-in systems with memory translation, an SC is allowed to succeed if the
-earlier LR reserved the same location using an alias with a different
-virtual address, but is also allowed to fail if the virtual address is
+An implementation can reserve an arbitrary larger subset of the memory
+space on each LR, provided the memory range includes all bytes of the
+addressed data word.  An SC may succeed if no store from another hart
+to the address range reserved by the LR can be observed to have
+occurred between the LR and the SC, and if there is no other SC
+between the LR and itself in program order.  Note this LR might have
+had a different address argument, but reserved the SC's address as
+part of the memory subset.  Following this model, in systems with
+memory translation, an SC is allowed to succeed if the earlier LR
+reserved the same location using an alias with a different virtual
+address, but is also allowed to fail if the virtual address is
 different.  The SC must fail if a store from another hart to the
 address range reserved by the LR can be observed to occur between the
-LR and the SC.  The precise statement of the atomicity requirements for
-successful LR/SC sequences is defined by the Atomicity Axiom in
-Section~\ref{sec:rvwmo}.
-
-In the standard A extension, an SC must fail if there is another SC (to
-any address) between the LR and the SC in program order.  In other
-words, multiple outstanding reservations are not permitted.
+LR and the SC.  An SC must fail if there is another SC (to any
+address) between the LR and the SC in program order.  The precise
+statement of the atomicity requirements for successful LR/SC sequences
+is defined by the Atomicity Axiom in Section~\ref{sec:rvwmo}.
 
 \begin{commentary}
 A store-conditional instruction to a scratch word of memory should be used
@@ -209,12 +206,6 @@ during a preemptive context switch to forcibly yield any existing load
 reservation.
 \end{commentary}
 
-\begin{commentary}
-The specification explicitly allows implementations to support more
-powerful implementations with wider guarantees, provided they do not
-void the atomicity guarantees for the constrained sequences.
-\end{commentary}
-
 LR/SC can be used to construct lock-free data structures.  An example
 using LR/SC to implement a compare-and-swap function is shown in
 Figure~\ref{cas}.  If inlined, compare-and-swap functionality need
diff --git a/src/riscv-spec.tex b/src/riscv-spec.tex
index 8648fd5..02d77bf 100644
--- a/src/riscv-spec.tex
+++ b/src/riscv-spec.tex
@@ -74,13 +74,13 @@ Andrew Waterman and Krste Asanovi\'{c}, RISC-V Foundation, May 2017.
 \input{rv32e}
 \input{rv64}
 \input{rv128}
-\input{csr}
-\input{rvwmo}
 \input{m}
 \input{a}
+\input{csr}
 \input{f}
 \input{d}
 \input{q}
+\input{rvwmo}
 \input{l}
 \input{c}
 \input{b}