[lkml]   [2023]   [Jan]   [21]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
SubjectRe: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
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

P0 P1 P2
--------------------- ---------------------- -------------------------
Wrel p2=1
synchronize_srcu() starts
... idx2, p2, and y propagate to all CPUs ...
Time t1
Wrel p1=1
,,, idx1 and p1 propagate to all CPUs ...
Racq p1=1
synchronize_srcu() ends
Racq p2=1

(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

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


 \ /
  Last update: 2023-03-26 23:51    [W:0.291 / U:0.396 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site