> > > Is x86's brand of memory ordering strong enough for Ztso?
> > > I thought x86 had an optimisation where it was allowed to store forward
> > > within the current CPU causing stores not to be quite strictly ordered.
[...]
> then a bit further down, '8.2.3.5 Intra-Processor Forwarding Is Allowed'
> has an example and says
>
> 'The memory-ordering model allows concurrent stores by two processors to
> be seen in
> different orders by those two processors; specifically, each processor
> may perceive
> its own store occurring before that of the other.'
>
> Having said that, I remember it's realyl difficult to trigger; it's ~10
> years since I saw an example to trigger it, and can't remember it.
AFAICT, Ztso allows the forwarding in question too. Simulations with
the axiomatic formalization confirm such expectation:
RISCV intra-processor-forwarding
{
0:x5=1; 0:x6=x; 0:x8=y;
1:x5=1; 1:x6=y; 1:x8=x;
}
P0 | P1 ;
sw x5,0(x6) | sw x5,0(x6) ;
lw x9,0(x6) | lw x9,0(x6) ;
lw x7,0(x8) | lw x7,0(x8) ;
exists
(0:x7=0 /\ 1:x7=0 /\ 0:x9=1 /\ 1:x9=1)
Test intra-processor-forwarding Allowed
States 4
0:x7=0; 0:x9=1; 1:x7=0; 1:x9=1;
0:x7=0; 0:x9=1; 1:x7=1; 1:x9=1;
0:x7=1; 0:x9=1; 1:x7=0; 1:x9=1;
0:x7=1; 0:x9=1; 1:x7=1; 1:x9=1;
Ok
Witnesses
Positive: 1 Negative: 3
Condition exists (0:x7=0 /\ 1:x7=0 /\ 0:x9=1 /\ 1:x9=1)
Observation intra-processor-forwarding Sometimes 1 3
Time intra-processor-forwarding 0.00
Hash=518e4b9b2f0770c94918ac5d7e311ba5
Andrea
