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

[Alan Stern]

On Mon, Jan 23, 2023 at 09:06:54PM +0100, Jonas Oberhauser wrote:
> 
> 
> On 1/23/2023 8:58 PM, Alan Stern wrote:
> > On Mon, Jan 23, 2023 at 05:16:27PM +0100, Jonas Oberhauser wrote:
> > > On 1/19/2023 5:41 PM, Alan Stern wrote:
> > > 
> > > > But when you're comparing grace periods or critical sections to each other,
> > > > things get a little ambiguous.  Should G1 be considered to come before
> > > > G2 when t1(G1) < t1(G2), when t2(G1) < t2(G2), or when t2(G1) < t1(G2)?
> > > > Springing for (po ; rcu-order ; po?) amounts to choosing the second
> > > > alternative.
> > > Aha, I see! Powerful notation indeed.
> > > Keeping that in mind, wouldn't it make sense for pb also be changed to
> > > `...;po?` ?
> > You mean changing the definition of pb to either:
> > 
> > 	prop ; strong-fence ; hb* ; po? ; [Marked]
> > 
> > or
> > 
> > 	prop ; strong-fence ; hb* ; [Marked] ; po? ; [Marked]
> 
> Oh no, not at all!
> 
> I mean that
>     pb = prop ; po ; {strong ordering-operation} ; po ; hb* ; [Marked]
> could instead be
>     pb = prop ; po ; {strong ordering-operation} ; po? ; hb* ; [Marked]
> 
> (note that the po ; ... ; po part is actually folded inside the actual
> definition of strong fence).

This goes back to the original herd models, before the LKMM came about: 
The fencerel() macro uses po on both sides.  I believe the motivating 
idea back then was that ordering should apply only to memory accesses 
(which can in practice be observed), not to other types of events such 
as memory barriers.

> > rcu-fence is different because rcu-order has to begin and end with
> > either a grace period or a critical section, and both of these restrict
> > the execution order of surrounding events:
> > 
> > 	If X is a synchronize_rcu() or rcu_read_unlock() then events
> > 	po-before X must execute before X;
> > 
> > 	If X is a synchronize_rcu() or rcu_read_lock() then events
> > 	po-after X must execute after X.
> > 
> I believe so do the strong ordering-operations in pb.

But the beginning and end of a pb link (for example, overwrite and hb) 
don't need to be strong-ordering operations.

Alan