Messages in this thread | | | Date | Tue, 24 Jan 2023 18:20:19 -0800 | From | "Paul E. McKenney" <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
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
| |