fixes to appendices, tables and graphics

8 files changed, 148 insertions, 158 deletions

diff --git a/src/f-st-ext.adoc b/src/f-st-ext.adoc
index 88ed2ea..f37ab97 100644
--- a/src/f-st-ext.adoc
+++ b/src/f-st-ext.adoc
@@ -221,10 +221,10 @@ provide exceptional default values.
 ====
 
 === Subnormal Arithmetic
-(((operations, subnormal)))
 
 Operations on subnormal numbers are handled in accordance with the IEEE
 754-2008 standard.
+(((operations, subnormal)))
 
 In the parlance of the IEEE standard, tininess is detected after
 rounding.
diff --git a/src/images/wavedrom/atomic-mem.adoc b/src/images/wavedrom/atomic-mem.adoc
index 7132ddd..014f829 100644
--- a/src/images/wavedrom/atomic-mem.adoc
+++ b/src/images/wavedrom/atomic-mem.adoc
@@ -1,7 +1,6 @@
 //## 9.4 Atomic Memory Operations
 
 
-
 [wavedrom, ,]
 ....
 {reg: [
diff --git a/src/images/wavedrom/spfloat-cn-cmp.adoc b/src/images/wavedrom/spfloat-cn-cmp.adoc
index 3dfafae..4a409de 100644
--- a/src/images/wavedrom/spfloat-cn-cmp.adoc
+++ b/src/images/wavedrom/spfloat-cn-cmp.adoc
@@ -3,24 +3,13 @@
 [wavedrom, ,]
 ....
 {reg: [
-  {bits: 7, name: 'opcode', attr: ['OP-FP','OP-FP'],    type: 8},
-  {bits: 5, name: 'rd',     attr: ['dest','dest'],     type: 2},
-  {bits: 3, name: 'rm',  attr: ['RM','RM'],       type: 8},
-  {bits: 5, name: 'rs1',    attr: ['src','src'],      type: 4},
-  {bits: 5, name: 'rs2',    attr: ['W[U]/L[U]', 'W[U]/L[U]'],     type: 8},
-  {bits: 2, name: 'fmt',    attr: ['S','S'],        type: 8},
-  {bits: 5, name: 'funct5', attr: ['FCVT.int.fmt', 'FCVT.fmt.int'],    type: 8},
-]}
-....
-....
-{reg: [
-  {bits: 7, name: 'opcode', attr: ['OP-FP'],    type: 8},
-  {bits: 5, name: 'rd',     attr: ['dest'],     type: 2},
-  {bits: 3, name: 'rm',  attr: ['J[N]/JX'],       type: 8},
-  {bits: 5, name: 'rs1',    attr: ['src1'],      type: 4},
-  {bits: 5, name: 'rs2',    attr: ['src2'],     type: 8},
-  {bits: 2, name: 'fmt',    attr: ['S'],        type: 8},
-  {bits: 5, name: 'funct5', attr: ['FSGNJ'],    type: 8},
+  {bits: 7, name: 'opcode', attr: 'OP-FP',        type: 8},
+  {bits: 5, name: 'rd',     attr: 'dest',         type: 2},
+  {bits: 3, name: 'func3',  attr: 'RM',           type: 8},
+  {bits: 5, name: 'rs1',    attr: 'src',          type: 4},
+  {bits: 5, name: 'rs2',    attr: ['D', 'S'], type: 4},
+  {bits: 2, name: 'fmt',    attr: ['S','D'],      type: 8},
+  {bits: 5, name: 'funct5', attr: ['FCVT.S.D', 'FCVT.D.S'], type: 8},
 ]}
 ....
 
diff --git a/src/images/wavedrom/spfloat.adoc b/src/images/wavedrom/spfloat.adoc
index 607dc3a..f23744f 100644
--- a/src/images/wavedrom/spfloat.adoc
+++ b/src/images/wavedrom/spfloat.adoc
@@ -14,4 +14,3 @@
 ....
 
 
-
diff --git a/src/mm-eplan.adoc b/src/mm-eplan.adoc
index 1fde4c9..7b8ec81 100644
--- a/src/mm-eplan.adoc
+++ b/src/mm-eplan.adoc
@@ -660,6 +660,8 @@ enforces ordering with respect to all previous loads.
 
 [[spinlock_atomics]]
 .A spinlock with atomics
+[source%linenums,asm]
+[source%linenums,asm]
 ....
           sd           x1, (a1)     # Arbitrary unrelated store
           ld           x2, (a2)     # Arbitrary unrelated load
@@ -685,6 +687,7 @@ load` at the beginning of the example in the global memory order.
 
 [[spinlock_fences]]
 .A spinlock with fences
+[source%linenums,asm]
 ....
           sd           x1, (a1)     # Arbitrary unrelated store
           ld           x2, (a2)     # Arbitrary unrelated load
@@ -786,6 +789,7 @@ _rs1_ to _rd_.
 
 [[fflags]]
 .(c) has a syntactic dependency on both (a) and (b) via fflags, a destination register that both (a) and (b) implicitly accumulate into
+[source%linenums,asm]
 ....
 (a) fadd f3,f1,f2
 (b) fadd f6,f4,f5
@@ -809,6 +813,7 @@ syntactic dependencies as a lightweight ordering mechanism.
 
 [[address]]
 .A syntactic address dependency
+[source%linenums,asm]
 ....
 ld a1,0(s0)
 xor a2,a1,a1
@@ -835,6 +840,7 @@ expensive.
 
 [[control1]]
 .A syntactic control dependency
+[source%linenums,asm]
 ....
 	lw x1,0(x2)
 	bne x1,x0,next
@@ -852,6 +858,7 @@ dependency from the memory operation generated by the first instruction.
 
 [[control2]]
 .Another syntactic control dependency
+[source%linenums,asm]
 ....
 lw x1,0(x2)
 bne x1,x0,next
@@ -1148,14 +1155,14 @@ those external devices and buses.
 
 [[tsomappings]]
 .Mappings from TSO operations to RISC-V operations
-[cols="<,<",options="header",]
+[cols="<,<",options="header",separator=!]
 |===
-|x86/TSO Operation |RVWMO Mapping
-|Load | `l{b|h|w|d}; fence r,rw`
-|Store |`fence rw,w; s{b|h|w|d}`
-|Atomic RMW |`amo<op>.{w|d}.aqrl OR`
-| |`loop:lr.{w|d}.aq; <op>; sc.{w|d}.aqrl; bnez loop`
-|Fence |`fence rw,rw`
+!x86/TSO Operation !RVWMO Mapping
+!Load ! `l{b|h|w|d}; fence r,rw`
+!Store !`fence rw,w; s{b|h|w|d}`
+!Atomic RMW !`amo<op>.{w|d}.aqrl OR`
+! !`loop:lr.{w|d}.aq; <op>; sc.{w|d}.aqrl; bnez loop`
+!Fence !`fence rw,rw`
 |===
 
 <<somappings>> provides a mapping from TSO memory
@@ -1184,16 +1191,16 @@ reservation mechanism than was originally intended.
 
 [[powermappings]]
 .Mappings from Power operations to RISC-V operations
-[cols="<,<",options="header",]
+[cols="<,<",options="header",separator=!]
 |===
-|Power Operation |RVWMO Mapping
-|Load |`l{b|h|w|d}`
-|Load-Reserve |`lr.{w|d}`
-|Store |`s{b|h|w|d}`
-|Store-Conditional |`sc.{w|d}`
-|`lwsync` |`fence.tso`
-|`sync` |`fence rw,rw`
-|`isync` |`fence.i; fence r,r`
+!Power Operation !RVWMO Mapping
+!Load !`l{b|h|w|d}`
+!Load-Reserve !`lr.{w|d}`
+!Store !`s{b|h|w|d}`
+!Store-Conditional !`sc.{w|d}`
+!`lwsync` !`fence.tso`
+!`sync` !`fence rw,rw`
+!`isync` !`fence.i; fence r,r`
 |===
 
 <<powermappings>> provides a mapping from Power memory
@@ -1204,21 +1211,21 @@ not present in RVWMO.
 
 [[armmappings]]
 .Mappings from ARM operations to RISC-V operations
-[cols="<,<",options="header",]
+[cols="<,<",options="header",separator=!]
 |===
-|ARM Operation |RVWMO Mapping
-|Load |`l{b|h|w|d}`
-|Load-Acquire |`fence rw, rw; l{b|h|w|d}; fence r,rw`
-|Load-Exclusive |`lr.{w|d}`
-|Load-Acquire-Exclusive |`lr.{w|d}.aqrl`
-|Store |`s{b|h|w|d}`
-|Store-Release |`fence rw,w; s{b|h|w|d}`
-|Store-Exclusive |`sc.{w|d}`
-|Store-Release-Exclusive |`sc.{w|d}.rl`
-|`dmb` |`fence rw,rw`
-|`dmb.ld` |`fence r,rw`
-|`dmb.st` |`fence w,w`
-|`isb` |`fence.i; fence r,r`
+!ARM Operation !RVWMO Mapping
+!Load !`l{b|h|w|d}`
+!Load-Acquire !`fence rw, rw; l{b|h|w|d}; fence r,rw`
+!Load-Exclusive !`lr.{w|d}`
+!Load-Acquire-Exclusive !`lr.{w|d}.aqrl`
+!Store !`s{b|h|w|d}`
+!Store-Release !`fence rw,w; s{b|h|w|d}`
+!Store-Exclusive !`sc.{w|d}`
+!Store-Release-Exclusive !`sc.{w|d}.rl`
+!`dmb` !`fence rw,rw`
+!`dmb.ld` !`fence r,rw`
+!`dmb.st` !`fence w,w`
+!`isb` !`fence.i; fence r,r`
 |===
 
 <<armmappings>> provides a mapping from ARM memory
@@ -1337,6 +1344,7 @@ Memory Model evolves.
 
 [[lkmm_ll]]
 .Orderings between critical sections in Linux
+[source%linenums,asm]
 ....
 (a) int r0 = *x;
 (bc) spin_unlock(y, 0);
@@ -1364,128 +1372,126 @@ _aq_ and _rl_ set.
 
 [[c11mappings]]
 .Mappings from C/C++ primitives to RISC-V primitives.
-[cols="<,<",options="header",]
+[cols="<,<",options="header",separator=!]
 |===
-|C/C++ Construct | RVWMO Mapping
 
-|Non-atomic load | `l{b|h|w|d}`
+!C/C++ Construct ! RVWMO Mapping
+
+!Non-atomic load ! `l{b|h|w|d}`
 
-|`atomic_load(memory_order_relaxed)` |`l{b|h|w|d}`
+!`atomic_load(memory_order_relaxed)` !`l{b|h|w|d}`
 
-|`atomic_load(memory_order_acquire)` |`l{b|h|w|d}; fence r,rw`
+!`atomic_load(memory_order_acquire)` !`l{b|h|w|d}; fence r,rw`
 
-|`atomic_load(memory_order_seq_cst)` |`fence rw,rw; l{b|h|w|d}; fence r,rw`
+!`atomic_load(memory_order_seq_cst)` !`fence rw,rw; l{b|h|w|d}; fence r,rw`
 
-|Non-atomic store |`s{b|h|w|d}`
+!Non-atomic store !`s{b|h|w|d}`
 
-|`atomic_store(memory_order_relaxed)` |`s{b|h|w|d}`
+!`atomic_store(memory_order_relaxed)` !`s{b|h|w|d}`
 
-|`atomic_store(memory_order_release)` |`fence rw,w; s{b|h|w|d}`
+!`atomic_store(memory_order_release)` !`fence rw,w; s{b|h|w|d}`
 
-|`atomic_store(memory_order_seq_cst)` |`fence rw,w; s{b|h|w|d}`
+!`atomic_store(memory_order_seq_cst)` !`fence rw,w; s{b|h|w|d}`
 
-|`atomic_thread_fence(memory_order_acquire)` |`fence r,rw`
+!`atomic_thread_fence(memory_order_acquire)` !`fence r,rw`
 
-|`atomic_thread_fence(memory_order_release)` |`fence rw,w`
+!`atomic_thread_fence(memory_order_release)` !`fence rw,w`
 
-|`atomic_thread_fence(memory_order_acq_rel)` |`fence.tso`
+!`atomic_thread_fence(memory_order_acq_rel)` !`fence.tso`
 
-|`atomic_thread_fence(memory_order_seq_cst)` |`fence rw,rw`
+!`atomic_thread_fence(memory_order_seq_cst)` !`fence rw,rw`
 
-|C/C++ Construct |RVWMO AMO Mapping
+!C/C++ Construct !RVWMO AMO Mapping
 
-|`atomic_<op>(memory_order_relaxed)` |`amo<op>.{w|d}`
+!`atomic_<op>(memory_order_relaxed)` !`amo<op>.{w|d}`
 
-|`atomic_<op>(memory_order_acquire)` |`amo<op>.{w|d}.aq`
+!`atomic_<op>(memory_order_acquire)` !`amo<op>.{w|d}.aq`
 
-|`atomic_<op>(memory_order_release)` |`amo<op>.{w|d}.rl`
+!`atomic_<op>(memory_order_release)` !`amo<op>.{w|d}.rl`
 
-|`atomic_<op>(memory_order_acq_rel)` |`amo<op>.{w|d}.aqrl`
+!`atomic_<op>(memory_order_acq_rel)` !`amo<op>.{w|d}.aqrl`
 
-|`atomic_<op>(memory_order_seq_cst)` |`amo<op>.{w|d}.aqrl`
+!`atomic_<op>(memory_order_seq_cst)` !`amo<op>.{w|d}.aqrl`
 
-|C/C++ Construct |RVWMO LR/SC Mapping
+!C/C++ Construct !RVWMO LR/SC Mapping
 
-|`atomic_<op>(memory_order_relaxed)` |`loop:lr.{w|d}; <op>; sc.{w|d};`
+!`atomic_<op>(memory_order_relaxed)` !`loop:lr.{w|d}; <op>; sc.{w|d};`
 
-| |`bnez loop`
+! !`bnez loop`
 
-|`atomic_<op>(memory_order_acquire)`
-|`loop:lr.{w|d}.aq; <op>; sc.{w|d};`
+!`atomic_<op>(memory_order_acquire)` !`loop:lr.{w|d}.aq; <op>; sc.{w|d};`
 
-| |`bnez loop`
+! !`bnez loop`
 
-|`atomic_<op>(memory_order_release)`
-|`loop:lr.{w|d}; <op>; sc.{w|d}.rl;`
+!`atomic_<op>(memory_order_release)` !`loop:lr.{w|d}; <op>; sc.{w|d}.rl;`
 
-| |`bnez loop`
+! !`bnez loop`
 
-|`atomic_<op>(memory_order_acq_rel)`
-|`loop:lr.{w|d}.aq; <op>; sc.{w|d}.rl;`
+!`atomic_<op>(memory_order_acq_rel)` !`loop:lr.{w|d}.aq; <op>; sc.{w|d}.rl;`
 
-| |`bnez loop`
+! !`bnez loop`
 
-|`atomic_<op>(memory_order_seq_cst)` |`loop:lr.{w|d}.aqrl; <op>;`
+!`atomic_<op>(memory_order_seq_cst)` !`loop:lr.{w|d}.aqrl; <op>;`
 
-| |`sc.{w|d}.rl; bnez loop`
+! !`sc.{w|d}.rl; bnez loop`
 
 |===
 
 [[c11mappings_hypothetical]]
 .Hypothetical mappings from C/C++ primitives to RISC-V primitives, if native load-acquire and store-release opcodes are introduced.
-[cols="<,<",options="header",]
+[cols="<,<",options="header",separator=!]
 |===
-|C/C++ Construct |RVWMO Mapping
+!C/C++ Construct !RVWMO Mapping
 
-|Non-atomic load |`l{b|h|w|d}`
+!Non-atomic load !`l{b|h|w|d}`
 
-|`atomic_load(memory_order_relaxed)` |`l{b|h|w|d}`
+!`atomic_load(memory_order_relaxed)` !`l{b|h|w|d}`
 
-|`atomic_load(memory_order_acquire)` |`l{b|h|w|d}.aq`
+!`atomic_load(memory_order_acquire)` !`l{b|h|w|d}.aq`
 
-|`atomic_load(memory_order_seq_cst)` |`l{b|h|w|d}.aq`
+!`atomic_load(memory_order_seq_cst)` !`l{b|h|w|d}.aq`
 
-|Non-atomic store |`s{b|h|w|d}`
+!Non-atomic store !`s{b|h|w|d}`
 
-|`atomic_store(memory_order_relaxed)` |`s{b|h|w|d}`
+!`atomic_store(memory_order_relaxed)` !`s{b|h|w|d}`
 
-|`atomic_store(memory_order_release)` |`s{b|h|w|d}.rl`
+!`atomic_store(memory_order_release)` !`s{b|h|w|d}.rl`
 
-|`atomic_store(memory_order_seq_cst)` |`s{b|h|w|d}.rl`
+!`atomic_store(memory_order_seq_cst)` !`s{b|h|w|d}.rl`
 
-|`atomic_thread_fence(memory_order_acquire)` |`fence r,rw`
+!`atomic_thread_fence(memory_order_acquire)` !`fence r,rw`
 
-|`atomic_thread_fence(memory_order_release)` |`fence rw,w`
+!`atomic_thread_fence(memory_order_release)` !`fence rw,w`
 
-|`atomic_thread_fence(memory_order_acq_rel)` |`fence.tso`
+!`atomic_thread_fence(memory_order_acq_rel)` !`fence.tso`
 
-|`atomic_thread_fence(memory_order_seq_cst)` |`fence rw,rw`
+!`atomic_thread_fence(memory_order_seq_cst)` !`fence rw,rw`
 
-|C/C++ Construct |RVWMO AMO Mapping
+!C/C++ Construct !RVWMO AMO Mapping
 
-|`atomic_<op>(memory_order_relaxed)` |`amo<op>.{w|d}`
+!`atomic_<op>(memory_order_relaxed)` !`amo<op>.{w|d}`
 
-|`atomic_<op>(memory_order_acquire)` |`amo<op>.{w|d}.aq`
+!`atomic_<op>(memory_order_acquire)` !`amo<op>.{w|d}.aq`
 
-|`atomic_<op>(memory_order_release)` |`amo<op>.{w|d}.rl`
+!`atomic_<op>(memory_order_release)` !`amo<op>.{w|d}.rl`
 
-|`atomic_<op>(memory_order_acq_rel)` |`amo<op>.{w|d}.aqrl`
+!`atomic_<op>(memory_order_acq_rel)` !`amo<op>.{w|d}.aqrl`
 
-|`atomic_<op>(memory_order_seq_cst)` |`amo<op>.{w|d}.aqrl`
+!`atomic_<op>(memory_order_seq_cst)` !`amo<op>.{w|d}.aqrl`
 
-|C/C++ Construct |RVWMO LR/SC Mapping
+!C/C++ Construct !RVWMO LR/SC Mapping
 
-|`atomic_<op>(memory_order_relaxed)` |`lr.{w|d}; <op>; sc.{w|d}`
+!`atomic_<op>(memory_order_relaxed)` !`lr.{w|d}; <op>; sc.{w|d}`
 
-|`atomic_<op>(memory_order_acquire)` |`lr.{w|d}.aq; <op>; sc.{w|d}`
+!`atomic_<op>(memory_order_acquire)` !`lr.{w|d}.aq; <op>; sc.{w|d}`
 
-|`atomic_<op>(memory_order_release)` |`lr.{w|d}; <op>; sc.{w|d}.rl`
+!`atomic_<op>(memory_order_release)` !`lr.{w|d}; <op>; sc.{w|d}.rl`
 
-|`atomic_<op>(memory_order_acq_rel)` |`lr.{w|d}.aq; <op>; sc.{w|d}.rl`
+!`atomic_<op>(memory_order_acq_rel)` !`lr.{w|d}.aq; <op>; sc.{w|d}.rl`
 
-|`atomic_<op>(memory_order_seq_cst)` |`lr.{w|d}.aq^&#2731; <op>; sc.{w|d}.rl`
+!`atomic_<op>(memory_order_seq_cst)` !`lr.{w|d}.aq^&#2731; <op>; sc.{w|d}.rl`
 
-|`^&#2731;` must be `lr.{w|d}.aqrl` in order to interoperate with code mapped per <<c11mappings>> |
+!`^&#2731;` must be `lr.{w|d}.aqrl` in order to interoperate with code mapped per <<c11mappings>> !
 |===
 
 Any AMO can be emulated by an LR/SC pair, but care must be taken to
diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc
index feea627..e717e22 100644
--- a/src/mm-formal.adoc
+++ b/src/mm-formal.adoc
@@ -22,14 +22,12 @@ We present a formal specification of the RVWMO memory model in Alloy
 https://github.com/daniellustig/riscv-memory-model.
 
 The online material also contains some litmus tests and some examples of
-how Alloy can be used to model check some of the mappings in
-Section #sec:memory:porting[[sec:memory:porting]].
-
-`  `
+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 {
@@ -55,14 +53,13 @@ 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]
 ....
-////////////////////////////////////////////////////////////////////////////////
 // =RVWMO axioms=
 
 // Load Value Axiom
@@ -92,11 +89,11 @@ pred Atomicity {
 pred RISCV_mm { LoadValue and Atomicity /* and Progress */ }
 ....
 
-`  `
 
+.The RVWMO memory model formalized in Alloy (3/5: model of memory)
+[source%linenums,sml]
 ....
-////////////////////////////////////////////////////////////////////////////////
-// Basic model of memory
+//Basic model of memory
 
 sig Hart {  // hardware thread
   start : one Event
@@ -149,10 +146,9 @@ fact { acquireRCpc + acquireRCsc + releaseRCpc + releaseRCsc in iden }
 fact { no FenceTSO.(pr + pw + sr + sw) }
 ....
 
-`  `
-
+.The RVWMO memory model formalized in Alloy (4/5: Basic model rules)
+[source%linenums,scala]
 ....
-////////////////////////////////////////////////////////////////////////////////
 // =Basic model rules=
 
 // Ordering annotation groups
@@ -195,8 +191,8 @@ fact { all a: Address | one Init & a.~address } // one init store per address
 fact { no Init <: po and no po :> Init }
 ....
 
-`  `
-
+.The RVWMO memory model formalized in Alloy (5/5: Auxiliaries)
+[source%linenums,asm]
 ....
 // po
 fact { acyclic[po] }
@@ -228,7 +224,6 @@ fun rdw : Event->Event {
 fact { no gmo & gmo.gmo } // keep the visualization uncluttered
 fact { all a: Address | some a.~address }
 
-////////////////////////////////////////////////////////////////////////////////
 // =Optional: opcode encoding restrictions=
 
 // the list of blessed fences
@@ -245,7 +240,6 @@ pred restrict_to_current_encodings {
   no (LoadNormal + StoreNormal) & (Acquire + Release)
 }
 
-////////////////////////////////////////////////////////////////////////////////
 // =Alloy shortcuts=
 pred acyclic[rel: Event->Event] { no iden & ^rel }
 pred total[rel: Event->Event, bag: Event] {
@@ -269,11 +263,10 @@ partial order based RVWMO model.
 
 The simulator [.sans-serif]#herd# is part of the [.sans-serif]#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/.
-
-`  `
+models and more are available online at http://diy.inria.fr/cats7/riscv/.
 
+.riscv-defs.cat, a herd definition of preserved program order (1/3)
+[source%linenums,asm]
 ....
 (*************)
 (* Utilities *)
@@ -338,8 +331,8 @@ and r13 = [R];addr;[M];po;[W]
 let ppo = r1 | r2 | r3 | r4 | r5 | r6 | r7 | r8 | r9 | r10 | r11 | r12 | r13
 ....
 
-`  `
-
+.riscv.cat, a herd version of the RVWMO memory model (2/3)
+[source%linenums,asm]
 ....
 Total
 
@@ -381,8 +374,8 @@ let winside  = (infloc;rmw;inflocext) & (infloc;rf;rmw;inflocext) & [W]
 empty winside as Atomic
 ....
 
-`  `
-
+.`riscv.cat`, an alternative herd presentation of the RVWMO memory model (3/3)
+[source%linenums,asm]
 ....
 Partial
 
@@ -410,7 +403,7 @@ acyclic co|rfe|fr|ppo as Model
 empty rmw & (fre;coe) as Atomic
 ....
 
-[[sec:operational]]
+[[operational]]
 === An Operational Memory Model
 
 This is an alternative presentation of the RVWMO memory model in
@@ -438,7 +431,7 @@ sizes. Misaligned accesses are broken up into single-byte accesses.
 The operational model, together with a fragment of the RISC-V ISA
 semantics (RV64I and A), are integrated into the `rmem` exploration tool
 (https://github.com/rems-project/rmem). `rmem` can explore litmus tests
-(see #sec:litmustests[[sec:litmustests]]) and small ELF binaries
+(see <<litmustests>>) and small ELF binaries
 exhaustively, pseudo-randomly and interactively. In `rmem`, the ISA
 semantics is expressed explicitly in Sail (see
 https://github.com/rems-project/sail for the Sail language, and
@@ -449,7 +442,7 @@ https://github.com/rems-project/lem for the Lem language).
 `rmem` has a command-line interface and a web-interface. The
 web-interface runs entirely on the client side, and is provided online
 together with a library of litmus tests:
-http://www.cl.cam.ac.uk/~pes20/rmem. The command-line interface is
+http://www.cl.cam.ac.uk/. The command-line interface is
 faster than the web-interface, specially in exhaustive mode.
 
 Below is an informal introduction of the model states and transitions.
@@ -458,11 +451,11 @@ The description of the formal model starts in the next subsection.
 Terminology: In contrast to the axiomatic presentation, here every
 memory operation is either a load or a store. Hence, AMOs give rise to
 two distinct memory operations, a load and a store. When used in
-conjunction with ``instruction``, the terms ``load`` and ``store`` refer
+conjunction with `instruction`, the terms `load` and `store` refer
 to instructions that give rise to such memory operations. As such, both
-include AMO instructions. The term ``acquire`` refers to an instruction
+include AMO instructions. The term `acquire` refers to an instruction
 (or its memory operation) with the acquire-RCpc or acquire-RCsc
-annotation. The term ``release`` refers to an instruction (or its memory
+annotation. The term `release` refers to an instruction (or its memory
 operation) with the release-RCpc or release-RCsc annotation.
 
 ==== Model states
@@ -515,7 +508,7 @@ from a single instruction instance; it will change the state of that
 instance, and it may depend on or change the rest of its hart state and
 the shared memory state, but it does not depend on other hart states,
 and it will not change them. The transitions are introduced below and
-defined in Section #sec:omm:transitions[1.3.5], with a precondition and
+defined in <<transitions>>, with a precondition and
 a construction of the post-transition model state for each.
 
 Transitions for all instructions:
@@ -723,15 +716,15 @@ Data-flow dependencies (address and data) in the model emerge from the
 fact that each register read has to wait for the appropriate register
 write to be executed (as described above).
 
-[[sec:omm:inst_state]]
+[[inst_state]]
 ==== Instruction Instance State
 
-Each instruction instance latexmath:[$i$] has a state comprising:
+Each instruction instance __i_ has a state comprising:
 
 * _program_loc_, the memory address from which the instruction was
 fetched;
 * _instruction_kind_, identifying whether this is a load, store, AMO,
-fence, branch/jump or a `simple' instruction (this also includes a
+fence, branch/jump or a `simple` instruction (this also includes a
 _kind_ similar to the one described for the pseudocode execution
 states);
 * _src_regs_, the set of source _reg_name_s (including system
@@ -739,9 +732,10 @@ registers), as statically determined from the pseudocode of the
 instruction;
 * _dst_regs_, the destination _reg_name_s (including system registers),
 as statically determined from the pseudocode of the instruction;
-* _pseudocode_state_ (or sometimes just `state' for short), one of (this
-is a tagged union; tags in small-caps):
-+
+* _pseudocode_state_ (or sometimes just `state` for short), one of (this
+is a tagged union; tags in small-caps): +
+
+
 [cols="<,<",]
 |===
 |Plain(_isa_state_) |ready to make a pseudocode transition
@@ -914,7 +908,7 @@ latexmath:[$\textit{address}\ldots\textit{address}+\textit{size}-1$].
 . update the state of latexmath:[$i$] to
 Pending_mem_loads(_load_continuation_).
 
-In Section #sec:rvwmo:primitives[[sec:rvwmo:primitives]] it is said that
+In <<primitives>> it is said that
 misaligned memory accesses may be decomposed at any granularity. Here we
 decompose them to one-byte accesses as this granularity subsumes all
 others.
@@ -1022,7 +1016,7 @@ propagated memory store operations), and the condition above requires
 all program-order-previous store-releases-RCsc to be finished when the
 load is acquire-RCsc.
 
-[[omm:sat_from_mem]]
+[[sat_from_mem]]
 ===== Satisfy memory load operation from memory
 
 For an instruction instance latexmath:[$i$] of a non-AMO load
@@ -1134,7 +1128,7 @@ have initiated and so have non-empty _mem_stores_; and
 program-order-previous load instructions have initiated and so have
 non-empty _mem_loads_.
 
-Action: record that latexmath:[$i$] is committed.
+Action: record that _i_ is committed.
 
 Notice that if condition
 #omm:commit_store:prev_addrs[[omm:commit_store:prev_addrs]] is satisfied
@@ -1410,3 +1404,6 @@ transition does not generate memory load operations, and the shared
 memory is not involved in the transition. Instead, the model depends on
 an external oracle that provides an opcode when given a memory location.
 * The model does not cover exceptions, traps and interrupts.
+
+
+
diff --git a/src/riscv-isa-unpr-conv-review.adoc b/src/riscv-isa-unpr-conv-review.adoc
index 5603378..db8bd67 100644
--- a/src/riscv-isa-unpr-conv-review.adoc
+++ b/src/riscv-isa-unpr-conv-review.adoc
@@ -30,7 +30,7 @@
 :bibtex-style: apa
 :icons: font
 :lang: en
-:listing-caption: Listing
+:listing-caption: Example
 :sectnums:
 :toc: left
 :toclevels: 4
@@ -133,7 +133,7 @@ include::history.adoc[]
 //history.tex
 include::mm-eplan.adoc[]
 //memory.tex
-//include::mm-formal.adoc[]
+include::mm-formal.adoc[]
 //end of memory.tex, memory-model-alloy.tex, memory-model-herd.tex
 include::index.adoc[]
 // this is generated generated from index markers.
diff --git a/src/riscv-isa-unpr-conv-review.pdf b/src/riscv-isa-unpr-conv-review.pdf
index 07bc6f9..ce37973 100644
--- a/src/riscv-isa-unpr-conv-review.pdf
+++ b/src/riscv-isa-unpr-conv-review.pdf