Fixed some conversion issues.

Fixed conversion issues with some text.
Fixed escaping of characters.

1 files changed, 16 insertions, 16 deletions

diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc
index a5c6fb3..4625eaa 100644
--- a/src/mm-formal.adoc
+++ b/src/mm-formal.adoc
@@ -8,10 +8,10 @@ discrepancies are unintended; the expectation is that the models
 describe exactly the same sets of legal behaviors.
 
 This appendix should be treated as commentary; all normative material is
-provided in <<memorymodel>> and in the rest of
+provided in <<memorymodel, Chapter 17>> and in the rest of
 the main body of the ISA specification. All currently known
 discrepancies are listed in
-<<discrepancies>>. Any other
+<<discrepancies, Section A.7>>. Any other
 discrepancies are unintentional.
 
 [[alloy]]
@@ -26,8 +26,8 @@ how Alloy can be used to model check some of the mappings in <<memory_porting>>.
 
 .The RVWMO memory model formalized in Alloy (1/5: PPO)
 [source%linenums,c]
-....
-  // =RVWMO PPO=
+----
+// =RVWMO PPO=
 
 // Preserved Program Order
 fun ppo : Event->Event {
@@ -53,9 +53,9 @@ fun ppo : Event->Event {
   + addrdep.^po :> Store
 }
 
-  / the global memory order respects preserved program order
+// the global memory order respects preserved program order
 fact { ppo in ^gmo }
-....
+----
 
 .The RVWMO memory model formalized in Alloy (2/5: Axioms)
 [source%linenums,io]
@@ -255,13 +255,13 @@ The tool [.sans-serif]#herd# takes a memory model and a litmus test as
 input and simulates the execution of the test on top of the memory
 model. Memory models are written in the domain specific language Cat.
 This section provides two Cat memory model of RVWMO. The first model,
-Figure #fig:herd2[[fig:herd2]], follows the _global memory order_,
-Chapter <<memorymodel>>, definition of RVWMO, as much
+Figure #fig:herd2[[fig:herd2]], follows the _global memory order_,
+Chapter <<memorymodel>>, definition of RVWMO, as much
 as is possible for a Cat model. The second model,
-Figure #fig:herd3[[fig:herd3]], is an equivalent, more efficient,
+Figure #fig:herd3[[fig:herd3]], is an equivalent, more efficient,
 partial order based RVWMO model.
 
-The simulator [.sans-serif]#herd# is part of the [.sans-serif]#diy# tool
+The simulator `herd` is part of the `diy` tool
 suite — see http://diy.inria.fr for software and documentation. The
 models and more are available online at http://diy.inria.fr/cats7/riscv/.
 
@@ -481,7 +481,7 @@ way).
 
 Each hart state consists principally of a tree of instruction instances,
 some of which have been _finished_, and some of which have not.
-Non-finished instruction instances can be subject to _restart_, e.g. if
+Non-finished instruction instances can be subject to _restart_, e.g. if
 they depend on an out-of-order or speculative load that turns out to be
 unsound.
 
@@ -495,7 +495,7 @@ pseudocode for this instruction). The model uses a formalization of the
 intra-instruction semantics in Sail. One can think of the execution
 state of an instruction as a representation of the pseudocode control
 state, pseudocode call stack, and local variable values. An instruction
-instance state also includes information about the instance’s memory and
+instance state also includes information about the instance's memory and
 register footprints, its register reads and writes, its memory
 operations, whether it is finished, etc.
 
@@ -552,7 +552,7 @@ load operation, from memory.
 been entirely satisfied and the instruction pseudocode can continue
 executing. A load instruction can be subject to being restarted until
 the transition. But, under some conditions, the model might treat a load
-instruction as non-restartable even before it is finished (e.g. see ).
+instruction as non-restartable even before it is finished (e.g. see ).
 
 Transitions specific to store instructions:
 
@@ -767,7 +767,7 @@ size). Each memory store operations includes a memory footprint, and,
 when available, a value.
 
 A load instruction instance with a non-empty _mem_loads_, for which all
-the load operations are satisfied (i.e. there are no unsatisfied load
+the load operations are satisfied (i.e. there are no unsatisfied load
 slices) is said to be _entirely satisfied_.
 
 Informally, an instruction instance is said to have _fully determined
@@ -1041,7 +1041,7 @@ unsatisfied slices of the memory load operation.
 A load instruction instance latexmath:[$i$] in state
 Pending_mem_loads(_load_continuation_) can be completed (not to be
 confused with finished) if all the memory load operations
-latexmath:[$i.\textit{mem\_loads}$] are entirely satisfied (i.e. there
+latexmath:[$i.\textit{mem\_loads}$] are entirely satisfied (i.e. there
 are no unsatisfied slices). Action: update the state of latexmath:[$i$]
 to Plain(_load_continuation(mem_value)_), where _mem_value_ is assembled
 from all the memory store operation slices that satisfied
@@ -1105,7 +1105,7 @@ Pending_mem_stores(_store_continuation_).
 ===== Commit store instruction
 
 An uncommitted instruction instance latexmath:[$i$] of a non-`sc` store
-instruction or an `sc` instruction in the context of the ````
+instruction or an `sc` instruction in the context of the \````
 transition, in state Pending_mem_stores(_store_continuation_), can be
 committed (not to be confused with propagated) if: