Messages in this thread | ![/](/images/icornerl.gif) | | Date | Tue, 24 Jan 2023 20:54:56 -0500 | From | Alan Stern <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
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.
Alan
| ![\](/images/icornerr.gif) |