Various RVWMO adoc fixes

1 files changed, 40 insertions, 40 deletions

diff --git a/src/rvwmo.adoc b/src/rvwmo.adoc
index 885e7ca..dad2ae1 100644
--- a/src/rvwmo.adoc
+++ b/src/rvwmo.adoc
@@ -17,7 +17,7 @@ instructions from the first hart being executed in a different order.
 Therefore, multithreaded code may require explicit synchronization to
 guarantee ordering between memory instructions from different harts. The
 base RISC-V ISA provides a FENCE instruction for this purpose, described
-in <<fence>>, while the atomics extension ^A^
+in <<fence>>, while the atomics extension _A_
 additionally defines load-reserved/store-conditional and atomic
 read-modify-write instructions.
 (((atomics, misaligned)))
@@ -30,8 +30,8 @@ with additional rules specific to those extensions.
 The appendices to this specification provide both axiomatic and
 operational formalizations of the memory consistency model as well as
 additional explanatory material.
-((FENCE))
-((SFENCE))
+(((FENCE)))
+(((SFENCE)))
 
 [NOTE]
 ====
@@ -84,7 +84,7 @@ Among instructions in RV32GC and RV64GC, each aligned memory instruction
 gives rise to exactly one memory operation, with two exceptions. First,
 an unsuccessful SC instruction does not give rise to any memory
 operations. Second, FLD and FSD instructions may each give rise to
-multiple memory operations if XLENlatexmath:[$<$]64, as stated in
+multiple memory operations if XLEN<64, as stated in
 <<fld_fsd>> and clarified below. An aligned AMO
 gives rise to a single memory operation that is both a load operation
 and a store operation simultaneously.
@@ -92,25 +92,25 @@ and a store operation simultaneously.
 [NOTE]
 ====
 Instructions in the RV128 base instruction set and in future ISA
-extensions such as V (vector) and P (SIMD) may give rise to multiple
+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.
 ====
 
 A misaligned load or store instruction may be decomposed into a set of
 component memory operations of any granularity. An FLD or FSD
-instruction for which XLENlatexmath:[$<$]64 may also be decomposed into
+instruction for which XLEN<64 may also be decomposed into
 a set of component memory operations of any granularity. The memory
 operations generated by such instructions 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
+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_
+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 <<zam>>.
-((decomposition))
+(((decomposition)))
 
 [NOTE]
 ====
@@ -155,7 +155,7 @@ consistent synchronization operations.
 While there are many different definitions for acquire and release
 annotations in the literature, in the context of RVWMO these terms are
 concisely and completely defined by Preserved Program Order rules
-<<rcsc>>.
+5-7.
 
 *RCpc* annotations are currently only used when implicitly assigned to
 every memory access per the standard extension *Ztso*
@@ -218,7 +218,7 @@ register for _i_
 
 Most non-memory instructions _carry a dependency_ from each of their
 source registers to each of their destination registers. However, there
-are exceptions to this rule; see <<>>source-dest-regs>>.
+are exceptions to this rule; see <<source-dest-regs>>.
 
 Instruction _j_ has a _syntactic dependency_ on instruction
 _i_ via destination register _s_ of
@@ -237,22 +237,22 @@ destination register _s_ and source register _p_
 . _m_ carries a dependency from _p_ to
 _q_
 
-Finally, in the definitions that follow, let ^A^ and
+Finally, in the definitions that follow, let _a_ and
 _b_ be two memory operations, and let _i_ and
-_j_ be the instructions that generate l^A^ and
+_j_ be the instructions that generate _a_ and
 _b_, respectively.
 
-_b_ has a _syntactic address dependency_ on l^A^
+_b_ has a _syntactic address dependency_ on _a_
 if _r_ is an address source register for _j_ and
 _j_ has a syntactic dependency on _i_ via source
 register _r_
 
-_b_ has a _syntactic data dependency_ on l^A^ if
+_b_ has a _syntactic data dependency_ on _a_ if
 _b_ is a store operation, _r_ is a data source
 register for _j_, and _j_ has a syntactic
 dependency on _i_ via source register _r_
 
-_b_ has a _syntactic control dependency_ on l^A^
+_b_ has a _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
@@ -278,52 +278,52 @@ _preserved program order_.
 
 The complete definition of preserved program order is as follows (and
 note that AMOs are simultaneously both loads and stores): memory
-operation l^A^ precedes memory operation _b_ in
+operation _a_ precedes memory operation _b_ in
 preserved program order (and hence also in the global memory order) if
-l^A^ precedes _b_ in program order,
-l^A^ and _b_ both access regular main memory
+_a_ precedes _b_ in program order,
+_a_ and _b_ both access regular main memory
 (rather than I/O regions), and any of the following hold:
 
-[[overlapping-orering]]
+[[overlapping-ordering]]
 * Overlapping-Address Orderings:
 . _b_ is a store, and
-l^A^ and _b_ access overlapping memory addresses
-. l^A^ and _b_ are loads,
-_x_ is a byte read by both l^A^ and
+_a_ and _b_ access overlapping memory addresses
+. _a_ and _b_ are loads,
+_x_ is a byte read by both _a_ and
 _b_, there is no store to _x_ between
-l^A^ and _b_ in program order, and
-l^A^ and _b_ return values for _x_
+_a_ and _b_ in program order, and
+_a_ and _b_ return values for _x_
 written by different memory operations
-. l^A^ is
+. _a_ is
 generated by an AMO or SC instruction, _b_ is a load, and
-_b_ returns a value written by l^A^
+_b_ returns a value written by _a_
 * Explicit Synchronization
 . There is a FENCE instruction that
-orders l^A^ before _b_
-. l^A^ has an acquire
+orders _a_ before _b_
+. _a_ has an acquire
 annotation
 . _b_ has a release annotation
-. l^A^ and _b_ both have
+. _a_ and _b_ both have
 RCsc annotations
-. {empty} l^A^ is paired with
+. _a_ is paired with
 _b_
 * Syntactic Dependencies
 . _b_ has a syntactic address
-dependency on l^A^
+dependency on _a_
 . _b_ has a syntactic data
-dependency on l^A^
+dependency on _a_
 . _b_ is a store, and
-_b_ has a syntactic control dependency on l^A^
+_b_ has a syntactic control dependency on _a_
 * Pipeline Dependencies
 . _b_ is a
 load, and there exists some store _m_ between
-l^A^ and _b_ in program order such that
-_m_ has an address or data dependency on l^A^,
+_a_ and _b_ in program order such that
+_m_ has an address or data dependency on _a_,
 and _b_ returns a value written by _m_
 . _b_ is a store, and
-there exists some instruction _m_ between l^A^
+there exists some instruction _m_ between _a_
 and _b_ in program order such that _m_ has an
-address dependency on l^A^
+address dependency on _a_
 
 ==== Memory Model Axioms
 
@@ -367,7 +367,7 @@ such patterns to be rare, and their use is discouraged.
 No memory operation may be preceded in the global memory order by an
 infinite sequence of other memory operations.
 
-[[sec:csr-granularity]]
+[[csr-granularity]]
 === CSR Dependency Tracking Granularity
 
 .Granularities at which syntactic dependencies are tracked through CSRs
@@ -382,7 +382,7 @@ infinite sequence of other memory operations.
 Note: read-only CSRs are not listed, as they do not participate in the
 definition of syntactic dependencies.
 
-[[sec:source-dest-regs]]
+[[source-dest-regs]]
 === Source and Destination Register Listings
 
 This section provides a concrete listing of the source and destination