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

[Alan Stern]

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.

>  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.

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)