|
* 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.
|
