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

Jonas Oberhauser
2023-01-25T13:10:59Z

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