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

Paul E. McKenney
2023-01-21T20:10:33Z

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