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

[Paul E. McKenney]

On Tue, Jan 24, 2023 at 08:54:56PM -0500, Alan Stern wrote:
> On Tue, Jan 24, 2023 at 02:54:49PM -0800, Paul E. McKenney wrote:
> > On Tue, Jan 24, 2023 at 05:35:33PM -0500, Alan Stern wrote:
> > > Can you be more explicit?  Exactly what guarantees does the kernel 
> > > implementation make that can't be expressed in LKMM?
> > 
> > I doubt that I will be able to articulate it very well, but here goes.
> > 
> > Within the Linux kernel, the rule for a given RCU "domain" is that if
> > an event follows a grace period in pretty much any sense of the word,
> > then that event sees the effects of all events in all read-side critical
> > sections that began prior to the start of that grace period.
> > 
> > Here the senses of the word "follow" include combinations of rf, fr,
> > and co, combined with the various acyclic and irreflexive relations
> > defined in LKMM.
> 
> The LKMM says pretty much the same thing.  In fact, it says the event 
> sees the effects of all events po-before the unlock of (not just inside) 
> any read-side critical section that began prior to the start of the 
> grace period.
> 
> > > And are these anything the memory model needs to worry about?
> > 
> > Given that several people, yourself included, are starting to use LKMM
> > to analyze the Linux-kernel RCU implementations, maybe it does.
> > 
> > Me, I am happy either way.
> 
> Judging from your description, I don't think we have anything to worry 
> about.

Sounds good, and let's proceed on that assumption then.  We can always
revisit later if need be.

							Thanx, Paul