Merge pull request #1293 from riscv/kersten1-patch-2

Old PR - Add initial value of Figure A.13

src/mm-eplan.adoc

@@ -939,7 +939,7 @@ no effect on the global memory order.
 |
 [%autowidth,cols="^,<,^,<",float="center",align="center"]
 !===
-4+!Initial values: 0(s0)=1; 0(s1)=1
+4+!Initial values: 0(s0)=1; 0(s2)=1
 4+!
 2+^!Hart 0 2+^!Hart 1 
 !(a) !ld a0,0(s0) !(e) !ld a3,0(s2)
@@ -1438,7 +1438,9 @@ RVWMO Mapping:
 (c) sd x0,0(s1)
 ....
 loop:
-(d) amoswap.d.aq a1,t1,0(s1)
+(d) lr.d.aq a1,(s1)
+bnez a1,loop
+sc.d a1,t1,(s1)
 bnez a1,loop
 (e) lw a2,0(s2)
 ----
@@ -1746,10 +1748,10 @@ a! image::graphviz/litmus_subsumption.png[]
 As written, if the load  (d) reads value _1_, then (a) must
 precede (f) in the global memory order:
 
-* (a) precedes (c) in the global memory order because of rule 2
+* (a) precedes (c) in the global memory order because of rule 4
 * (c) precedes (d) in the global memory order because of the Load
 Value axiom
-* (d) precedes (e) in the global memory order because of rule 7
+* (d) precedes (e) in the global memory order because of rule 10
 * (e) precedes (f) in the global memory order because of rule 1
 
 In other words the final value of the memory location whose address is