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

Andrea Parri
2023-01-17T11:46:41Z

On Mon, Jan 16, 2023 at 02:13:57PM -0800, Paul E. McKenney wrote:
> On Mon, Jan 16, 2023 at 02:20:57PM -0500, Alan Stern wrote:
> > On Mon, Jan 16, 2023 at 11:06:52AM -0800, Paul E. McKenney wrote:
> > > On Mon, Jan 16, 2023 at 01:11:41PM -0500, Alan Stern wrote:
> >
> > > > Why do you want to prohibit nesting? Why would that be a better
> > > > approximation?
> > >
> > > Because the current LKMM gives wrong answers for nested critical
> > > sections.
> >
> > I don't agree. Or at least, it depends on whose definition of "nested
> > critical sections" you adopt.
>
> Fair point, and I have therefore updated the test's header comment
> to read as follows:
>
> (*
> * Result: Sometimes
> *
> * This demonstrates non-nested overlapping of SRCU read-side critical
> * sections. Unlike RCU, SRCU critical sections do not unconditionally
> * nest.
> *)
>
> > > For example, for the litmus test shown below, mainline
> > > LKMM will incorrectly report "Never". The two SRCU read-side critical
> > > sections are independent, so the fact that P1()'s synchronize_srcu() is
> > > guaranteed to wait for the first on to complete says nothing about the
> > > second having completed. Therefore, in Linux-kernel SRCU, the "exists"
> > > clause could be satisfied.
> > >
> > > In contrast, the proposed change flags this as having nesting.
> >
> > In fact, this litmus test has overlapping critical sections, not nested
> > ones. But the current LKML incorrectly _thinks_ they are nested,
> > because it matches each lock with the first unmatched unlock.
> >
> > If you write a litmus test that has properly nested (not overlapping!)
> > read-side critical sections, the current LKMM will match the locks and
> > unlocks correctly and will give the right answer.
> >
> > So what you really want to do is rule out overlapping, not nesting. But
> > I guess there's no way to do one without the other.
>
> None that I could see!

This was reminiscent of old discussions, in fact, we do have:

[tools/memory-model/Documentation/litmus-tests.txt]

e. Although sleepable RCU (SRCU) is now modeled, there
are some subtle differences between its semantics and
those in the Linux kernel. For example, the kernel
might interpret the following sequence as two partially
overlapping SRCU read-side critical sections:

1 r1 = srcu_read_lock(&my_srcu);
2 do_something_1();
3 r2 = srcu_read_lock(&my_srcu);
4 do_something_2();
5 srcu_read_unlock(&my_srcu, r1);
6 do_something_3();
7 srcu_read_unlock(&my_srcu, r2);

In contrast, LKMM will interpret this as a nested pair of
SRCU read-side critical sections, with the outer critical
section spanning lines 1-7 and the inner critical section
spanning lines 3-5.

This difference would be more of a concern had anyone
identified a reasonable use case for partially overlapping
SRCU read-side critical sections. For more information
on the trickiness of such overlapping, please see:
https://paulmck.livejournal.com/40593.html

More recently/related,

https://lore.kernel.org/lkml/20220421230848.GA194034@paulmck-ThinkPad-P17-Gen-1/T/#m2a8701c7c377ccb27190a6679e58b0929b0b0ad9

Thanks,
Andrea

>
> Thanx, Paul
>
> > Alan
> >
> > > Thaxn, Paul
> > >
> > > ------------------------------------------------------------------------
> > >
> > > C C-srcu-nest-5
> > >
> > > (*
> > > * Result: Sometimes
> > > *
> > > * This demonstrates non-nesting of SRCU read-side critical sections.
> > > * Unlike RCU, SRCU critical sections do not nest.
> > > *)
> > >
> > > {}
> > >
> > > P0(int *x, int *y, struct srcu_struct *s1)
> > > {
> > > int r1;
> > > int r2;
> > > int r3;
> > > int r4;
> > >
> > > r3 = srcu_read_lock(s1);
> > > r2 = READ_ONCE(*y);
> > > r4 = srcu_read_lock(s1);
> > > srcu_read_unlock(s1, r3);
> > > r1 = READ_ONCE(*x);
> > > srcu_read_unlock(s1, r4);
> > > }
> > >
> > > P1(int *x, int *y, struct srcu_struct *s1)
> > > {
> > > WRITE_ONCE(*y, 1);
> > > synchronize_srcu(s1);
> > > WRITE_ONCE(*x, 1);
> > > }
> > >
> > > locations [0:r1]
> > > exists (0:r1=1 /\ 0:r2=0)