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

[Jonas Oberhauser]

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.

> I don't see any point in worrying about whatever else happens to the index.

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?

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

Best wishes,
jonas