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

[Alan Stern]

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.

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

The operational model doesn't specify exactly how synchronize_srcu() 
manages to do these things, though.

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.

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

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.

Does this answer your question satisfactorily?

> > > So if there is an srcu_down() that produces a cookie that is read by some
> > > read R, and R doesn't then pass that value into an srcu_up(), the
> > > srcu-warranty is voided.
> > No, it isn't.
> I quote Paul:
> "If you do anything else at all with it, anything at all, you just voided
> your SRCU warranty. For that matter, if you just throw that value on the
> floor and don't pass it to an srcu_up_read() execution, you also just voided
> your SRCU warranty."

I suspect Paul did not express himself very precisely, and what he 
really meant was more like this:

	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.

Alan