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

[Paul E. McKenney]

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

I suspect that you guys are talking past one another.  My guess is that
one of you is saying "we could check" and the other "we are not required
to check", which are not necessarily in disagreement.

But that is just a guess.  You guys tell me!  ;-)

							Thanx, Paul