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

[Andrea Parri]

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)