From 6662706aa5cebbf89d59b2f98c96b8a15e6e231d Mon Sep 17 00:00:00 2001 From: Kersten Richter Date: Tue, 26 Mar 2024 12:13:18 -0500 Subject: [PATCH] Update from old PR Adding left over stuff from this PR - https://github.com/riscv/riscv-isa-manual/pull/529/files Signed-off-by: Kersten Richter --- src/mm-eplan.adoc | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/mm-eplan.adoc b/src/mm-eplan.adoc index 470a3ab4d..d7bb8704e 100644 --- a/src/mm-eplan.adoc +++ b/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