> > AFAICT, Ztso allows the forwarding in question too. Simulations with
> > the axiomatic formalization confirm such expectation:
>
> OK that seems to be what it says in:
> https://five-embeddev.com/riscv-isa-manual/latest/ztso.html
> 'In both of these memory models, it is the that allows a hart to
> forward a value from its store buffer to a subsequent (in program order)
> load—that is to say that stores can be forwarded locally before they are
> visible to other harts'
Indeed, thanks for the remark.
> > 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)
>
> (I'm a bit fuzzy reading this...)
> So is that the interesting case - where x7 is saying neither processor
> saw the other processors write yet, but they did see their own?
Right, it was inspired by the homonymous test in the Intel's specs.
Andrea
