Re: [PATCH] RISC-V: Add support for Ztso

[Andrea Parri <andrea@rivosinc.com>]

> > 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