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

Paul E. McKenney
2023-01-25T02:20:25Z

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