Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po

[Jonas Oberhauser]

On 2/26/2023 5:23 PM, Joel Fernandes wrote:
> On Fri, Feb 24, 2023 at 02:52:51PM +0100, Jonas Oberhauser wrote:
> > As stated in the documentation and implied by its name, the ppo
> > (preserved program order) relation is intended to link po-earlier
> > to po-later instructions under certain conditions.  However, a
> > corner case currently allows instructions to be linked by ppo that
> > are not executed by the same thread, i.e., instructions are being
> > linked that have no po relation.
> >
> > This happens due to the mb/strong-fence/fence relations, which (as
> > one case) provide order when locks are passed between threads
> > followed by an smp_mb__after_unlock_lock() fence.  This is
> > illustrated in the following litmus test (as can be seen when using
> > herd7 with `doshow ppo`):
> >
> > P0(int *x, int *y)
> > {
> >      spin_lock(x);
> >      spin_unlock(x);
> > }
> >
> > P1(int *x, int *y)
> > {
> >      spin_lock(x);
> >      smp_mb__after_unlock_lock();
> >      *y = 1;
> > }
> >
> > The ppo relation will link P0's spin_lock(x) and P1's *y=1, because
> > P0 passes a lock to P1 which then uses this fence.
> >
> > The patch makes ppo a subrelation of po by letting fence contribute
> > to ppo only in case the fence links events of the same thread.
> >
> > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx>
> > ---
> >   tools/memory-model/linux-kernel.cat | 2 +-
> >   1 file changed, 1 insertion(+), 1 deletion(-)
> >
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index cfc1b8fd46da..adf3c4f41229 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -82,7 +82,7 @@ let rwdep = (dep | ctrl) ; [W]
> >   let overwrite = co | fr
> >   let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
> >   let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi)
> > -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int)
> > +let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int)
> Alternatively can be the following appended diff? Requires only single 'int'
> in ->ppo then and prevents future similar issues caused by sub relations.
> Also makes clear that ->ppo can only be CPU-internal.

I had thought about going in that direction, but it doesn't prevent 
future similar issues, at best makes them less likely.
For example, you could have an xfence that somehow goes back to the 
original thread, but to a po-earlier event (e.g., like prop).

Given that to-r and to-w are unlikely to ever become become inconsistent 
with po, I am not sure it even really helps much.

Personally I'm not too happy with the ad-hoc '& int' because it's like 
adding some unused stuff (via ... | unused-stuff) and then cutting it 
back out with &int, unlike prop & int which has a real semantic meaning 
(propagate back to the thread). The fastest move is the move we avoid 
doing, so I rather wouldn't add those parts in the first place.

However fixing the fence relation turned out to be a lot trickier, both 
because of the missed data race and also rmw-sequences, essentially I 
would have had to disambiguate between xfences and fences already in 
this patch. So I did this minimal local fix for now and we can discuss 
whether it makes sense to get rid of the '& int' once/if we have xfence etc.

Best wishes,
jonas

PS:
> ---8<-----------------------

haha that's so clever :D

> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 07f884f9b2bf..63052d1628e9 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -70,7 +70,7 @@ let rwdep = (dep | ctrl) ; [W]
>   let overwrite = co | fr
>   let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
>   let to-r = addr | (dep ; [Marked] ; rfi)
> -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int)
> +let ppo = (to-r | to-w | fence | po-unlock-lock-po) & int
>   
>   (* Propagation: Ordering from release operations and strong fences. *)
>   let A-cumul(r) = (rfe ; [Marked])? ; r