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

["Paul E. McKenney" <paulmck@kernel.org>]

On Sat, Jan 21, 2023 at 02:56:57PM -0500, Alan Stern wrote:
> On Sat, Jan 21, 2023 at 10:40:32AM -0800, Paul E. McKenney wrote:
> > On Sat, Jan 21, 2023 at 12:36:26PM -0500, Alan Stern wrote:
> > > On Fri, Jan 20, 2023 at 10:41:14PM +0100, Jonas Oberhauser wrote:
> > > > 
> > > > 
> > > > On 1/20/2023 5:18 PM, Alan Stern wrote:
> > > > > On Fri, Jan 20, 2023 at 11:13:00AM +0100, Jonas Oberhauser wrote:
> > > > > > Perhaps we could say that reading an index without using it later is
> > > > > > forbidden?
> > > > > > 
> > > > > > flag ~empty [Srcu-lock];data;rf;[~ domain(data;[Srcu-unlock])] as
> > > > > > thrown-srcu-cookie-on-floor
> > > > > We already flag locks that don't have a matching unlock.
> > > > 
> > > > Of course, but as you know this is completely orthogonal.
> > > 
> > > Yeah, okay.  It doesn't hurt to add this check, but the check isn't 
> > > complete.  For example, it won't catch the invalid usage here:
> > > 
> > > P0(srcu_struct *ss)
> > > {
> > > 	int r1, r2;
> > > 
> > > 	r1 = srcu_read_lock(ss);
> > > 	srcu_read_unlock(&ss, r1);
> > > 	r2 = srcu_read_lock(ss);
> > > 	srcu_read_unlock(&ss, r2);
> > > }
> > > 
> > > exists (~0:r1=0:r2)
> > > 
> > > On the other hand, how often will people make this sort of mistake in 
> > > their litmus tests?  My guess is not very.
> > 
> > I must be blind this morning.  I see a well-formed pair of back-to-back
> > SRCU read-side critical sections.  A rather useless pair, given that
> > both are empty,
> 
> And there are no synchronize_srcu() calls.

Agreed, an additional level of uselessness, though not invalidity.  After
all, the more advantageous SRCU use cases execute lots of srcu_read_lock()
and srcu_read_unlock() calls and very few synchronize_srcu() calls.

> >  but valid nonetheless.
> > 
> > Or is the bug the use of 0:r1 and 0:r2 in the "exists" clause?  If so,
> > then I agree that this is not at all a high-priority bug to flag.
> 
> Yes, that is the bug.  The patched version of LKMM and the 
> implementation you described say the exist clause will never be 
> satisfied, the current version of LKMM says it will always be 
> satisfied, and the theoretical model for SRCU says it will sometimes 
> be satisfied -- which is the answer we want.

Got it, thank you.

> > > > Can you briefly explain how the operational model you have in mind for
> > > > srcu's up and down allows x==1 (and y==0 and idx1==idx2) in the example I
> > > > sent before (copied with minor edit below for convenience)?
> > > > 
> > > > P0{
> > > >     idx1 = srcu_down(&ss);
> > > >     store_rel(p1, true);
> > > > 
> > > > 
> > > >     shared cs
> > > > 
> > > >     R x == 1
> > > > 
> > > >     while (! load_acq(p2));
> > > >     R idx2 == idx1 // for some reason, we got lucky!
> > > >     srcu_up(&ss,idx1);
> > > > }
> > > > 
> > > > P1{
> > > >     idx2 = srcu_down(&ss);
> > > >     store_rel(p2, true);
> > > > 
> > > >     shared cs
> > > > 
> > > >     R y == 0
> > > > 
> > > >     while (! load_acq(p1));
> > > >     srcu_up(&ss,idx2);
> > > > }
> > > > 
> > > > P2 {
> > > >     W y = 1
> > > >     srcu_sync(&ss);
> > > >     W x = 1
> > > > }
> > > > 
> > > > 
> > > > I can imagine models that allow this but they aren't pretty. Maybe you have
> > > > a better operational model?
> > > 
> > > The operational model is not very detailed as far as SRCU is concerned.  
> > > It merely says that synchronize_srcu() executing on CPU C waits until:
> > > 
> > > 	All writes received by C prior to the start of the function have 
> > > 	propagated to all CPUs (call this time t1).  This could be 
> > > 	arranged by having synchronize_srcu() start with an smp_mb().
> > > 
> > > 	For every srcu_down_read() that executed prior to t1, the 
> > > 	matching srcu_up_read() has finished and all writes received 
> > > 	by the unlocking CPU prior to the unlock have propagated to all 
> > > 	CPUs.  This could be arranged by having the srcu_up_read() 
> > > 	call include a release write which has been received by C and 
> > > 	having synchronize_srcu() end with an smp_mb().
> > 
> > Agreed.  It took me a few reads to see that this prohibited later writes
> > by other CPUs affecting reads in the prior critical section, but the "all
> > writes received by the unlocking CPU" does seem to me to prohibit this.
> > 
> > > The operational model doesn't specify exactly how synchronize_srcu() 
> > > manages to do these things, though.
> > 
> > Which is a good thing, given the wide variety of possible implementations.
> > 
> > > Oh yes, it also says that the value returned by srcu_down_read() is an 
> > > unpredictable int.  This differs from the code in the patched herd 
> > > model, which says that the value will always be 0.
> > 
> > As noted earlier, I believe that this is fine.  If significant problems
> > arise, then we might need to do something.  However, there is some
> > cost to complexity, so we should avoid getting too speculative about
> > possible probems.
> > 
> > > Anyway, the operational model says the litmus test can succeed as 
> > > follows:
> > > 
> > > P0                    P1                     P2
> > > --------------------- ---------------------- -------------------------
> > >                       Widx2=srcu_down_read()
> > >                       Wrel p2=1
> > >                       Ry=0
> > >                                              Wy=1
> > >                                              synchronize_srcu() starts
> > > 	... idx2, p2, and y propagate to all CPUs ...
> > >                                              Time t1
> > > Widx1=srcu_down_read()
> > > Wrel p1=1
> > > 	,,, idx1 and p1 propagate to all CPUs ...
> > >                       Racq p1=1
> > >                       srcu_up_read(idx2)
> > >                                              synchronize_srcu() ends
> > >                                              Wx=1
> > > Rx=1
> > > Racq p2=1
> > > Ridx2=idx1
> > > srcu_up_read(idx1)
> > > 
> > > (The final equality in P0 is allowed because idx1 and idx2 are both 
> > > random numbers, so they might be equal.)
> > 
> > This all makes sense to me.
> > 
> > > Incidentally, it's worth pointing out that the algorithm Paul described 
> > > will forbid this litmus test even if you remove the while loop and the 
> > > read of idx2 from P0.
> > 
> > Given that the values returned by those two srcu_down_read() calls must
> > be the same, then, yes, the current Linux-kernel Tree RCU implementation
> > would forbid this.
> > 
> > On the other hand, if the two indexes differ, then P2's synchronize_srcu()
> > can see that there are no really old readers on !Widx2, then flip
> > the index.  This would mean that P0's Widx1 would be equal to !Widx2,
> > which has already been waited on.  Then P2's synchronize_srcu() can
> > return as soon as it sees P1's srcu_up_read().
> 
> Sorry, what I said may not have been clear.  I meant that even if you 
> remove the while loop and read of idx2 from P0, your algorithm will 
> still not allow idx1 = idx2 provided everything else is as written.

If synchronize_srcu() has flipped ->srcu_idx by the time that P0's
srcu_down_read() executes, agreed.  Otherwise, Widx1 and Widx2 might
well be equal.

> > > 	If you don't pass the value to exactly one srcu_up_read() call, 
> > > 	you void the SRCU warranty.  In addition, if you do anything 
> > > 	else with the value that might affect the outcome of the litmus 
> > > 	test, you incur the risk that herd7 might compute an incorrect 
> > > 	result [as in the litmus test I gave near the start of this
> > > 	email].
> > > 
> > > Merely storing the value in a shared variable which then doesn't get 
> > > used or is used only for something inconsequential would not cause any 
> > > problems.
> > 
> > That is consistent with my understanding, but please let me try again
> > in list form:
> 
> ...
> 
> > 4.	If a value returned from a given srcu_read_lock() is passed to
> > 	exactly one srcu_read_unlock(), and then that value is later
> > 	manipulated, that is bad practice (exactly what are you trying
> > 	to accomplish by so doing?), but SRCU won't know the difference.
> > 
> > 	In particular, the Linux-kernel SRCU implementation doesn't know
> > 	about the herd7 "exists" clause, but kudos to Jonas for casting
> > 	his conceptual net widely indeed!
> 
> In addition, herd7 might give an answer different from what would 
> actually happen in the kernel, depending on what the manipulation does.

True, given that the kernel's srcu_read_unlock() can return a
non-zero value.

> Yes, that is more or less what I was trying to express.

Sounds good!

							Thanx, Paul