Address some feedback from Ken Dockser

1 files changed, 9 insertions, 6 deletions

diff --git a/src/rvwmo.tex b/src/rvwmo.tex
index 59867e8..1a7096c 100644
--- a/src/rvwmo.tex
+++ b/src/rvwmo.tex
@@ -14,7 +14,7 @@ The standard ISA extension for misaligned atomics ``Zam'' (Chapter~\ref{sec:zam}
 The appendices to this specification provide both axiomatic and operational formalizations of the memory consistency model as well as additional explanatory material.
 
 \begin{commentary}
-  This chapter defines the memory model for regular main memory operations.  The interaction of the memory model with I/O memory, instruction fetches, FENCE.I, page table walks, and SFENCE.VMA is not (yet) formalized.  Some or all of the above may be formalized in a future revision of this specification.  Future ISA extensions such as the ``V'' vector, ``T'' transactional memory, and ``J'' JIT extensions will need to be incorporated into a future revision as well.
+  This chapter defines the memory model for regular main memory operations.  The interaction of the memory model with I/O memory, instruction fetches, FENCE.I, page table walks, and SFENCE.VMA is not (yet) formalized.  Some or all of the above may be formalized in a future revision of this specification.  The RV128 base ISA and future ISA extensions such as the ``V'' vector, ``T'' transactional memory, and ``J'' JIT extensions will need to be incorporated into a future revision as well.
 
   Memory consistency models supporting overlapping memory accesses of different widths simultaneously remain an active area of academic research and are not yet fully understood.  The specifics of how memory accesses of different sizes interact under RVWMO are specified to the best of our current abilities, but they are subject to revision should new issues be uncovered.
 \end{commentary}
@@ -37,10 +37,14 @@ Memory-accessing instructions give rise to {\em memory operations}.
 A memory operation can be either a {\em load operation}, a {\em store operation}, or both simultaneously.
 All memory operations are single-copy atomic: they can never be observed in a partially-complete state.
 
-Each aligned memory instruction other than an unsuccessful SC instruction gives rise to exactly one memory operation.
+Among instructions in RV32GC and RV64GC, each aligned memory instruction other than an unsuccessful SC instruction gives rise to exactly one memory operation.
 An aligned AMO gives rise to a single memory operation that is both a load operation and a store operation simultaneously.
 Unsuccessful SC instructions do not generate architecturally-visible memory operations.
 
+\begin{commentary}
+  Instructions in the RV128 base instruction set and in future ISA extensions such as V (vector) and P (SIMD) may give rise to multiple memory operations.  However, the memory model for these extensions has not yet been formalized.
+\end{commentary}
+
 A misaligned load or store instruction may be decomposed into a set of component memory operations of any granularity.
 The memory operations generated by a misaligned instruction are not ordered with respect to each other in program order, but they are ordered normally with respect to the memory operations generated by preceding and subsequent instructions in program order.
 The atomics extension ``A'' does not require execution environments to support misaligned atomic instructions at all; however, if misaligned atomics are supported via the ``Zam'' extension, LRs, SCs, and AMOs may be decomposed subject to the constraints of the atomicity axiom for misaligned atomics, which is defined in Chapter~\ref{sec:zam}.
@@ -50,8 +54,7 @@ The atomics extension ``A'' does not require execution environments to support m
   Such implementations might, for example, simply iterate over the bytes of a misaligned access one by one.
 \end{commentary}
 
-An LR and SC are said to be {\em paired} if the LR precedes the SC in program order and if there are no other LR or SC instructions in between; the corresponding memory operations are said to be paired as well (except in case of a failed SC, where no store operation is generated).
-Both LR and SC instructions, and the memory operations generated by them, may be unpaired if they do not meet the condition above.
+An LR instruction and an SC instruction are said to be {\em paired} if the LR precedes the SC in program order and if there are no other LR or SC instructions in between; the corresponding memory operations are said to be paired as well (except in case of a failed SC, where no store operation is generated).
 The complete list of conditions determining whether an SC must succeed, may succeed, or must fail is defined in Section~\ref{sec:lrsc}.
 
 Load and store operations may also carry one or more ordering annotations from the following set: ``acquire-RCpc'', ``acquire-RCsc'', ``release-RCpc'', and ``release-RCsc''.
@@ -62,7 +65,7 @@ An AMO or SC instruction with {\em rl} set has a ``release-RCsc'' annotation.
 An AMO, LR, or SC instruction with both {\em aq} and {\em rl} set has both ``acquire-RCsc'' and ``release-RCsc'' annotations.
 
 \begin{commentary}
-  ``RCpc'' annotations are currently only used when implicitly assigned to every memory access per the standard extension ``Ztso'' (Chapter~\ref{sec:ztso}).  Furthermore, although the ISA does not currently contain native load-acquire or store-relase instructions, nor RCpc variants thereof the current {\em aq} and {\em rl} bits, the RVWMO model itself is designed to be forwards-compatible with the potential addition of any or all of the above into the ISA in a future extension.
+  ``RCpc'' annotations are currently only used when implicitly assigned to every memory access per the standard extension ``Ztso'' (Chapter~\ref{sec:ztso}).  Furthermore, although the ISA does not currently contain native load-acquire or store-relase instructions, nor RCpc variants thereof, the RVWMO model itself is designed to be forwards-compatible with the potential addition of any or all of the above into the ISA in a future extension.
 \end{commentary}
 
 For convenience, we use the term ``acquire annotation'' to refer to an acquire-RCpc annotation or an acquire-RCsc annotation.
@@ -183,7 +186,7 @@ An execution of a RISC-V program obeys the RVWMO memory consistency model only i
   \end{enumerate}
 }
 
-\newcommand{\atomicityaxiom}{If $r$ and $w$ are paired load and store operations generated by aligned LR and SC instructions in a hart $h$, and if $s$ is any store to byte $x$ from which $r$ returns a value, then $s$ must precede $w$ in the global memory order, and there can be no store from hart other than $h$ to byte $x$ following $s$ and preceding $w$ in the global memory order.}
+\newcommand{\atomicityaxiom}{If $r$ and $w$ are paired load and store operations generated by aligned LR and SC instructions in a hart $h$, $s$ is a store to byte $x$, and $r$ returns a value written by $s$, then $s$ must precede $w$ in the global memory order, and there can be no store from hart other than $h$ to byte $x$ following $s$ and preceding $w$ in the global memory order.}
 
 \newcommand{\progressaxiom}{No memory operation may be preceded in the global memory order by an infinite sequence of other memory operations.}