Clarified reservation range and that SC only pairs with immediately preceding LR.

1 files changed, 25 insertions, 20 deletions

diff --git a/src/a.tex b/src/a.tex
index 0dac426..c8528ac 100644
--- a/src/a.tex
+++ b/src/a.tex
@@ -86,9 +86,10 @@ Complex atomic memory operations on a single memory word are performed
 with the load-reserved (LR) and store-conditional (SC) instructions.
 LR loads a word from the address in {\em rs1}, places the
 sign-extended value in {\em rd}, and registers a reservation on the
-memory address.  SC writes a word in {\em rs2} to the address in {\em
-  rs1}, provided a valid reservation still exists on that address.  SC
-writes zero to {\em rd} on success or a nonzero code on failure.
+memory address and a range of bytes including at least all bytes of
+the addressed word.  SC writes a word in {\em rs2} to the address in
+{\em rs1}, provided a valid reservation still exists on that address.
+SC writes zero to {\em rd} on success or a nonzero code on failure.
 
 \begin{commentary}
 Both compare-and-swap (CAS) and LR/SC can be used to build lock-free
@@ -182,23 +183,27 @@ Implementations are permitted to simply always fail any LR/SC sequence that does
 not meet the forward-progress guarantee.
 \end{commentary}
 
-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.  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}.
+An implementation can reserve an arbitrarily large subset of the
+address space on each LR, provided the memory range includes all bytes
+of the addressed data word.  The reserved address range does not have
+to be constant on each dynamic invocation of a static LR instruction,
+or on each time a given address and data word size are used by an LR.
+An SC can only pair with the most recent LR in program order.  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.  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