Two more small bits of memory model commentary. (#210)

- The note about RCpc/RCsc in the literature is commentary, not
normative.

- Add a new note to make it a little more obvious that syntactic
dependencies can originate from SC instructions too.

Thanks to Ken Dockser again.

1 files changed, 10 insertions, 6 deletions

diff --git a/src/rvwmo.tex b/src/rvwmo.tex
index e6bc4d2..d289c13 100644
--- a/src/rvwmo.tex
+++ b/src/rvwmo.tex
@@ -60,21 +60,21 @@ An LR instruction and an SC instruction are said to be {\em paired} if the LR pr
 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''.
-In the memory model literature, the term ``RCpc'' stands for release consistency with processor-consistent synchronization operations, and the term ``RCsc'' stands for release consistency with sequentially-consistent synchronization operations~\cite{Gharachorloo90memoryconsistency}.
-
 An AMO or LR instruction with {\em aq} set has an ``acquire-RCsc'' annotation.
 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-release 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.
 Likewise, a ``release annotation'' refers to a release-RCpc annotation or a release-RCsc annotation.
 An ``RCpc annotation'' refers to an acquire-RCpc annotation or a release-RCpc annotation.
 An ``RCsc annotation'' refers to an acquire-RCsc annotation or a release-RCsc annotation.
 
+\begin{commentary}
+  In the memory model literature, the term ``RCpc'' stands for release consistency with processor-consistent synchronization operations, and the term ``RCsc'' stands for release consistency with sequentially-consistent synchronization operations~\cite{Gharachorloo90memoryconsistency}.
+
+  ``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-release 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}
+
 \subsection*{Syntactic Dependencies}
 \label{sec:memorymodel:dependencies}
 The definition of the RVWMO memory model depends in part on the notion of a syntactic dependency, defined as follows.
@@ -123,6 +123,10 @@ $b$ has a {\em syntactic data dependency} on $a$ if $b$ is a store operation, $r
 
 $b$ has a {\em syntactic control dependency} on $a$ if there is an instruction $m$ program-ordered between $i$ and $j$ such that $m$ is a branch or indirect jump and $m$ has a syntactic dependency on $i$.
 
+\begin{commentary}
+  Generally speaking, non-AMO load instructions do not have data source registers, and unconditional non-AMO store instructions do not have destination registers.  However, a successful SC instruction is considered to have the register specified in {\em rd} as a destination register, and hence it is possible for an instruction to have a syntactic dependency on a successful SC instruction that precedes it in program order.
+\end{commentary}
+
 \subsection*{Preserved Program Order}
 The global memory order for any given execution of a program respects some but not all of each hart's program order.
 The subset of program order that must be respected by the global memory order is known as {\em preserved program order}.