Messages in this thread | | | Date | Wed, 25 Jan 2023 14:10:08 +0100 | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) | From | Jonas Oberhauser <> |
| |
On 1/25/2023 3:20 AM, Paul E. McKenney wrote: > 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
FWIW, I currently don't see a need for either RCU nor "base" LKMM to have this kind of guarantee. But I'm curious for why it doesn't exist in LKMM -- is it because of Alpha or some other issues that make it hard to guarantee (like a compiler merging two threads and optimizing or something?), or is it simply that it seemed like a complicated guarantee with no discernible upside, or something else?
Best wishes, jonas
| |