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

[Alan Stern <stern@rowland.harvard.edu>]

[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.]

On Tue, Jan 03, 2023 at 04:57:56PM +0000, Jonas Oberhauser wrote:
> Happy new year everyone!
> 
> I'd like to circle back to the brief discussion we had about ppo \subseteq po.
> 
> Here's some context:
> 
> > > > > the preserved program order not always being a 
> > > > > program order, lack of
> > > 
> > > > Where does the LKMM allow a ppo relation not to be in program order?
> > >
> > > When one thread releases a lock and another one takes the lock, you 
> > > can get an mb relation between the two threads
> > >
> > > https://github.com/torvalds/linux/blob/master/tools/memory-model/linux
> > > -kernel.cat#L40
> > > 
> > > this then turns into a ppo edge.
> 
> > Ah.  I suppose we should have been a little more careful about internal vs. external full barriers.  RCU barriers are also external, but the model didn't try to include them in the definition of mb; we should have done the same with unlock-lock.
> 
> 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.

> 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).
> 
> 
> Note that no ordering is changed by this move.
> Firstly, the case [M];po;[UL];po;[LKW]; fencerel(After-unlock-lock) ; [M] which is also eliminated from mb by this change  is still present in ppo through the definition ppo = ... | (po-unlock-lock-po & int).
> Secondly, for the ordering of [M];po;[UL];co;[LKW]; fencerel(After-unlock-lock) ; [M] we can focus on the case [M];po;[UL];coe;[LKW]; fencerel(After-unlock-lock) ; [M] because the other case (coi) is covered by the previous case.
> Ordering imposed by this case is also not lost, since every [M];po;[UL];coe;[LKW]; fencerel(After-unlock-lock) ; [M] edge also imposes a
>     [M];po;[UL];rfe;[LKR]; fencerel(After-unlock-lock) ; [M]
> edge which is a po-rel ; [Marked] ; rfe ; [Marked] ; acq-po edge and hence hb;hb;hb.
> Thirdly, no new ordering is imposed by this change since every place we now order by strong-sync was previously ordered by the old strong-fence which is identical to the new strong-sync, and in all other places we changed we just (potentially) removed ordering.
> 
> 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.

Alan