Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

[Paul E. McKenney]

On Wed, Jan 04, 2023 at 11:13:05AM +0000, Jonas Oberhauser wrote:
> 
> 
> -----Original Message-----
> From: Alan Stern [mailto:stern@xxxxxxxxxxxxxxxxxxx] 
> Sent: Tuesday, January 3, 2023 7:56 PM
> > [Added LKML to the CC: list so there will be a permanent record of this part of the discussion, and changed the Subject: to something more descriptive of the topic at hand.]
> 
> Aha, so it's the same discussion but now with 64% improved chance of immortalizing any mistakes I make.

Welcome to our world of open-source software development!  ;-)

> > > To be more explicit, in the current LKMM, mb includes some cases of po;[UL];co;[LKW];po which also relates events between threads, and this trickles up to the ppo:
> > > 
> > >   let mb = ([M] ; fencerel(Mb) ; [M]) |
> > > 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> > > 	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
> > > 	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> > > 	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> > > 		fencerel(After-unlock-lock) ; [M])
> > >   let gp = po ; [Sync-rcu | Sync-srcu] ; po?
> > >   let strong-fence = mb | gp
> > >   ...
> > >   let ppo = to-r | to-w | (... | strong-fence | ...) | 
> > > (po-unlock-lock-po & int) // expanded for readability
> > > 
> > > Because of this, not every preserved program order edge is actually a program order edge that is being preserved.
> 
> > Indeed, one can argue that neither the fence nor the (po-unlock-lock-po & int) sub-relations should be included in ppo, since they don't reflect dataflow constraints.  They could instead be added separately to the definition of hb, which is the only place that uses ppo.
> 
> One can, but one can also argue instead that fences and lock/unlock sequences preserve program order. At least for fences this is the view e.g. RISC-V takes and I prefer this view.
> 
> > > My suggestion for a fix would be to move this part out of mb and strong-fence, and instead introduce a new relation strong-sync that covers synchronization also between threads.
> > > 
> > >   let mb = ([M] ; fencerel(Mb) ; [M]) |
> > > 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> > > 	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
> > > 	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> > > - 	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> > > -		fencerel(After-unlock-lock) ; [M])
> > >   let gp = po ; [Sync-rcu | Sync-srcu] ; po?
> > >   let strong-fence = mb | gp
> > > +  let strong-sync = strong-fence | ([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> > > +		fencerel(After-unlock-lock) ; [M])
> > > ...
> > >   let ppo = to-r | to-w | (... | strong-fence | ...) | 
> > > (po-unlock-lock-po & int)
> > > 
> > > and then use strong-sync instead of strong-fence everywhere else, e.g.
> > > - let pb = prop ; strong-fence ; hb* ; [Marked]
> > > + let pb = prop ; strong-sync ; hb* ; [Marked]
> > > and similarly where strong-fence is being redefined and used in various later lines.
> > > (In general I would prefer renaming also other *-fence relations into *-sync when they include edges between threads).
> > > The definition of strong-sync could also be slightly simplified to 
> > >   let strong-sync = strong-fence | ([M]; po-unlock-lock-po ; 
> > > [After-unlock-lock] ; po ; [M]) which is kind of pretty because the after-unlock-lock is now after po-unlock-lock-po.
> > > 
> > > What do you think?
> 
> > That all sounds good to me.  However, I wonder if it might be better to use "strong-order" (and similar) for the new relation name instead of "strong-sync".  The idea being that fences are about ordering, not (or not directly) about synchronization.
> 
> I think that is indeed better, thanks. I suppose *-sync might be more appropriate if it *only* included edges between threads.

There are quite a few ways to group the relations.  As long as we
don't end up oscillating back and forth with too short a frequency,
I am good.  ;-)

> I'll wait a few days for other suggestions and then prepare a patch.

Looking forward to seeing what you come up with!

							Thanx, Paul