Incorporate aspects of PR #444

h/t Marc

1 files changed, 17 insertions, 5 deletions

diff --git a/src/a.tex b/src/a.tex
index ca21955..bee6abc 100644
--- a/src/a.tex
+++ b/src/a.tex
@@ -168,10 +168,13 @@ An implementation can register an arbitrarily large reservation set on each
 LR, provided the reservation set includes all bytes of the addressed data word
 or doubleword.
 An SC can only pair with the most recent LR in program order.
-An SC may succeed if no store from another hart, nor a write from some other
-device, to the reservation set can be observed to have occurred between the LR
+An SC may succeed only if no store from another hart
+to the reservation set 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.
+An SC may succeed only if no write from a device other than a hart
+to the bytes accessed by the LR instruction can be observed to have occurred
+between the LR and SC.
 Note this LR might have had a different effective address and data size, but
 reserved the SC's address as part of the reservation set.
 \begin{commentary}
@@ -180,12 +183,21 @@ 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.
 \end{commentary}
+\begin{commentary}
+To accommodate legacy devices and buses, writes from devices other than RISC-V
+harts are only required to invalidate reservations when they overlap the bytes
+accessed by the LR.  These writes are not required to invalidate the
+reservation when they access other bytes in the reservation set.
+\end{commentary}
 
 The SC must fail if the address is not within the reservation set of the most
 recent LR in program order.
-The SC must fail if a store from another hart, or a write from some other
-device, to the reservation set can be observed to occur between the LR and the
-SC.
+The SC must fail if a store to the reservation set from another hart can be
+observed to occur between the LR and SC.
+The SC must fail if a write from some other device to the bytes accessed by
+the LR can be observed to occur between the LR and SC.
+(If such a device writes the reservation set but does not write the bytes
+accessed by the LR, the SC may or may not fail.)
 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