diff options
-rw-r--r-- | src/mm-eplan.adoc | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/src/mm-eplan.adoc b/src/mm-eplan.adoc index 528168f..6d653de 100644 --- a/src/mm-eplan.adoc +++ b/src/mm-eplan.adoc @@ -214,12 +214,12 @@ is determined by the load value axiom, not just strictly by determining the most recent store to the same address in the global memory order, as described below. -[[loadvalueaxiom]] +[[loadvalueaxiom, Load value axiom]] ==== Load value axiom [IMPORTANT] ==== -<<ax-load, Load Value Axiom>>: Each byte of each load _i_ returns the value written +<<ax-load>>: Each byte of each load _i_ returns the value written to that byte by the store that is the latest in global memory order among the following stores: @@ -241,19 +241,26 @@ Consider the <<litms_sb_forward>>. When running this program on an implementatio 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) -graphviz::images/graphviz/litmus_sb_fwd.txt[align="center",width=80] -[%autowidth,float="center",cols="^,<,^,<",options="header",align="center"] +[float="center",align="center",cols="1a,.^1a",frame="none",grid="none",options="noheader"] |=== -2+^|Hart 0 2+^|Hart 1 -2+^|li t1, 1 2+^|li t1, 1 -2+<|(a) sw t1,0(s0) 2+|(e) sw t1,0(s1) -2+<|(b) lw a0,0(s0) 2+|(f) lw a2,0(s1) -2+<|(c) fence r,r 2+|(g) fence r,r -2+<|(d) lw a1,0(s1) 2+|(h) lw a3,0(s0) -4+^|Outcome: `a0=1`, `a1=0`, `a2=1`, `a3=0` +| +[%autowidth,float="center",align="center",cols="^,<,^,<",options="header",align="center"] +!=== +2+^!Hart 0 2+^!Hart 1 +2+^!li t1, 1 2+^!li t1, 1 +2+<!(a) sw t1,0(s0) 2+!(e) sw t1,0(s1) +2+<!(b) lw a0,0(s0) 2+!(f) lw a2,0(s1) +2+<!(c) fence r,r 2+!(g) fence r,r +2+<!(d) lw a1,0(s1) 2+!(h) lw a3,0(s0) +4+^!Outcome: `a0=1`, `a1=0`, `a2=1`, `a3=0` +!=== +| +!=== +a! graphviz::images/graphviz/litmus_sb_fwd.txt[] +!=== |=== + * (a) executes and enters the first hart's private store buffer * (b) executes and forwards its return value 1 from (a) in the store buffer |