Clarification of ordering annotation semantics (#246)

* Clarification of ordering annotation semantics

As discussed (and approved) in the weekly memory model meeting, this change is the sister of a similar change in the RVWMO chapter. In each case the intent is to clarify that these memory models are completely defined in this specification. More specifically, the axiomatic definitions of the annotations are sufficient and should be used instead of any other understanding of these terms.

* Added links, corrected emdash

* Tweaks to the commentary

Reworded "programatically load"  to "Subsequent (in program order)" - there is no need to specify this is the same hart as this is implicit in "program order". Likewise, there is no need to say "to the same address" as the store buffer would not forward to a different address. 
The point of specifying the  Load Value Axiom, is to make it clear that it is the axiom that allows the expected TSO behavior, not the RCpc annotation.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/ztso.tex b/src/ztso.tex
index 36ab2a8..39683c4 100644
--- a/src/ztso.tex
+++ b/src/ztso.tex
@@ -20,7 +20,9 @@ RVTSO makes the following adjustments to RVWMO:
 \begin{commentary}
   These rules render all PPO rules except \ref{ppo:fence}--\ref{ppo:rcsc} redundant.
   They also make redundant any non-I/O fences that do not have both PW and SR set.
-  Finally, they also imply that no instruction will be reordered past an AMO in either direction.
+  Finally, they also imply that no memory operation will be reordered past an AMO in either direction.
+  
+  In the context of RVTSO, as is the case for RVWMO, the storage ordering annotations are concisely and completely defined by PPO rules \ref{ppo:acquire}--\ref{ppo:rcsc}. In both of these memory models, it is the \nameref{rvwmo:ax:load} that allows a hart to forward a value from its store buffer to a subsequent (in program order) load---that is to say that stores can be forwarded locally before they are visible to other harts.
 \end{commentary}
 
 In spite of the fact that Ztso adds no new instructions to the ISA, code written assuming RVTSO will not run correctly on implementations not supporting Ztso.