Closes #107

Fixes #64

Courtesy @gameboo in #205

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

Closes #263.

Closes #271.

Closes #279

h/t @pmundkur

Resolves #278

Resolves #276

Resolves #272

Clarified that LR/SC forward progress guarantee might only hold for a subset of instruction and data memory space depending on execution environment.

In the CA format, funct is changed to funct2, for consistency with the base ISA (which distinguishes between funct7 and funct3).

Closed #267

"logical AND" usually means C's "&&" operator, not "&" operator.  Thanks
to Bodhisattva Debnath for pointing out the issue!

This reverts commit 327be43b.

This is not a functional change, just an improvement to the description.

Resolves #45

Rationale is provided in the unprivileged manual (counters.tex).

Resolves #249