diff options
Diffstat (limited to 'src/mm-eplan.adoc')
| -rw-r--r-- | src/mm-eplan.adoc | 33 |
1 files changed, 16 insertions, 17 deletions
diff --git a/src/mm-eplan.adoc b/src/mm-eplan.adoc index d7bb870..7071b19 100644 --- a/src/mm-eplan.adoc +++ b/src/mm-eplan.adoc @@ -75,7 +75,7 @@ particular valid or invalid execution on the right. [.left] [%autowidth,float="center",align="center",cols="^,<,^,<",options="header"] !=== -2+!Hart 0 2+!Hart 1 +2+!Hart 0 2+!Hart 1 ! !⋮ ! !⋮ ! !li t1,1 ! !li t4,4 !(a) !sw t1,0(s0) !(e) !sw t4,0(s0) @@ -239,7 +239,7 @@ visible memory). Any other hart will therefore observe the load as performing before the store. Consider the <<litms_sb_forward>>. When running this program on an implementation with -store buffers, it is possible to arrive at the final outcome a0=1, `a1=0, a2=1, a3=0` as follows: +store buffers, it is possible to arrive at the final outcome `a0=1, a1=0, a2=1, a3=0` as follows: [[litms_sb_forward]] .A store buffer forwarding litmus test (outcome permitted) @@ -295,7 +295,7 @@ Call this "Rule X". Then we get the following: preceded (d), then (d) would be required to return the value 1. (This is a perfectly legal execution; it's just not the one in question) * (e) precedes (f): by rule X -* (f) precedes (h): by rule <<overlapping-ordering, 4]>> +* (f) precedes (h): by rule <<overlapping-ordering, 4>> * (h) precedes (a): by the load value axiom, as above. The global memory order must be a total order and cannot be cyclic, @@ -400,9 +400,9 @@ original hart holds the reservation. |(b) sd t1, 0(s0) |(b) sw t1, 4(s0) |(b) sw t1, 4(s0) |(b) sw t1, 4(s0) -|(c) sc.d t3, t2, 0(s0) |(c) sc.d t3, t2, 0(s0) |(c) sc.w t3, t2, 0(s0) |(c) addi s0, s0, 8 +|(c) sc.d t3, t2, 0(s0) |(c) sc.d t3, t2, 0(s0) |(c) sc.w t3, t2, 0(s0) |(c) addi s0, s0, 8 -|(d) sc.w t3, t2, 8(s0)||| +||||(d) sc.w t3, t2, 0(s0) |==== [[litmus_lrsdsc]] <<litmus_lrsdsc, Figure 4>>: In all four (independent) instances, the final store-conditional instruction is permitted but not guaranteed to succeed. @@ -608,7 +608,7 @@ balance between enforcing CoRR in all cases while simultaneously being weak enough to permit "RSW" and "fri-rfi" patterns that commonly appear in real microarchitectures. -There is one more overlapping-address rule: <<overlapping-ordering, +There is one more overlapping-address rule: <<overlapping-ordering, rule 3>> simply states that a value cannot be returned from an AMO or SC to a subsequent load until the AMO or SC has (in the case of the SC, successfully) performed globally. This @@ -671,8 +671,8 @@ memory model. Finally, we note that since RISC-V uses a multi-copy atomic memory model, programmers can reason about fences bits in a thread-local -manner. There is no complex notion of "fence cumulativity" as found in -memory models that are not multi-copy atomic. +manner. Fences in RISC-V are not cumulative, as they are in some +non-multi-copy-atomic memory models. [[sec:memory:acqrel]] ==== Explicit Synchronization (<<overlapping-ordering, Rules 5-8>>) @@ -786,8 +786,8 @@ operation due to the inherent data dependency. However, PPO rule 8 also applies even when the value being stored does not syntactically depend on the value returned by the paired LR. -Lastly, we note that just as with fences, programmers need not worry -about "cumulativity" when analyzing ordering annotations. +Lastly, we note that, as with fences, ordering annotations are +not cumulative. [[sec:memory:dependencies]] ==== Syntactic Dependencies (<<overlapping-ordering, Rules 9-11>>) @@ -941,7 +941,7 @@ no effect on the global memory order. !=== 4+!Initial values: 0(s0)=1; 0(s2)=1 4+! -2+^!Hart 0 2+^!Hart 1 +2+^!Hart 0 2+^!Hart 1 !(a) !ld a0,0(s0) !(e) !ld a3,0(s2) !(b) !lr a1,0(s1) !(f) !sd a3,0(s0) !(c) !sc a2,a0,0(s1) ! ! @@ -1023,7 +1023,7 @@ data for that store are known. Consider <<litmus_datarfi>> (f) cannot be executed until the data for (e) has been resolved, because (f) must return the value written by (e) (or by something even later in the global memory order), and the old value must not be clobbered by the -writeback of (e) before (d) has had a chance to perform. Therefore, (f) +write-back of (e) before (d) has had a chance to perform. Therefore, (f) will never perform before (d) has performed. @@ -1058,7 +1058,7 @@ then (f) would no longer be dependent on the data of (e) being resolved, and hence the dependency of (f) on (d), which produces the data for (e), would be broken. -Rule<<overlapping-ordering, 13>> makes a similar observation to the +Rule <<overlapping-ordering, 13>> makes a similar observation to the previous rule: a store cannot be performed at memory until all previous loads that might access the same address have themselves been performed. Such a load must appear to execute before the store, but it cannot do so @@ -1176,7 +1176,7 @@ I/O write to a device register, a FENCE W,O or stronger is needed. [.text-center,source%linenums,asm] ---- sd t0, 0(a0) -fence w,o +fence w,o sd a0, 0(a1) ---- @@ -1775,7 +1775,7 @@ would be compatible with the RVWMO memory model: * "J" JIT extension * Native encodings for load and store opcodes with _aq_ and _rl_ set * Fences limited to certain addresses -* Cache writeback/flush/invalidate/etc.instructions +* Cache write-back/flush/invalidate/etc.instructions [[discrepancies]] === Known Issues @@ -1803,7 +1803,7 @@ would be compatible with the RVWMO memory model: .Mixed-size discrepancy (permitted by axiomatic models, forbidden by operational model) [%autowidth,float="center",align="center",cols="^,<,^,<",options="header"] |=== -2+|Hart 0 2+^|Hart 1 +2+|Hart 0 2+^|Hart 1 2+|li t1, 1 2+^|li t1, 1 |(a) |lw a0,0(s0) |(d) |ld a1,0(s1) |(b) |fence rw,rw |(e) |lw a2,4(s1) @@ -1848,4 +1848,3 @@ enforce this ordering naturally. As such, even though this rule is not official, we recommend that implementers enforce it nevertheless in order to ensure forwards compatibility with the possible future addition of this rule to RVWMO. - |