diff options
| author | Kersten Richter <kersten@riscv.org> | 2024-03-26 12:13:18 -0500 |
|---|---|---|
| committer | Andrew Waterman <andrew@sifive.com> | 2024-03-26 13:13:15 -0700 |
| commit | 6662706aa5cebbf89d59b2f98c96b8a15e6e231d (patch) | |
| tree | 45e65d60f2a59abbeedf68d41f4be4ebf55c50aa /src/mm-eplan.adoc | |
| parent | b3ee62f3e9c15ff50df8438c43e0c474f6d22b8e (diff) | |
| download | riscv-isa-manual-6662706aa5cebbf89d59b2f98c96b8a15e6e231d.zip riscv-isa-manual-6662706aa5cebbf89d59b2f98c96b8a15e6e231d.tar.gz riscv-isa-manual-6662706aa5cebbf89d59b2f98c96b8a15e6e231d.tar.bz2 | |
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 <kersten@riscv.org>
Diffstat (limited to 'src/mm-eplan.adoc')
| -rw-r--r-- | src/mm-eplan.adoc | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/mm-eplan.adoc b/src/mm-eplan.adoc index 470a3ab..d7bb870 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 |