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

[Jonas Oberhauser]

On 1/19/2023 7:41 PM, Paul E. McKenney wrote:
> On Thu, Jan 19, 2023 at 02:39:01PM +0100, Jonas Oberhauser wrote:
> > On 1/19/2023 1:11 AM, Paul E. McKenney wrote:
> > > On Wed, Jan 18, 2023 at 10:24:50PM +0100, Jonas Oberhauser wrote:
> > > > What I was thinking of is more something like this:
> > > >
> > > > P0{
> > > >      idx1 = srcu_down(&ss);
> > > >      srcu_up(&ss,idx1);
> > > > }
> > > >
> > > > P1{
> > > >       idx2 = srcu_down(&ss);
> > > >       srcu_up(&ss,idx2)
> > > > }
> > > And srcu_read_lock() and srcu_read_unlock() already do this.
> > I think I left out too much from my example.
> > And filling in the details led me down a bit of a rabbit hole of confusion
> > for a while.
> > But here's what I ended up with:
> >
> >
> > P0{
> >      idx1 = srcu_down(&ss);
> >      store_rel(p1, true);
> >
> >
> >      shared cs
> >
> >      R x == ?
> >
> >      while (! load_acq(p2));
> >      R idx2 == idx1 // for some reason, we got lucky!
> >      srcu_up(&ss,idx1);
> Although the current Linux-kernel implementation happens to be fine with
> this sort of abuse, I am quite happy to tell people "Don't do that!"
> And you can do this with srcu_read_lock() and srcu_read_unlock().
> In contrast, this actually needs srcu_down_read() and srcu_up_read():

My point/clarification request wasn't about whether you could write that 
code with read_lock() and read_unlock(), but what it would/should mean 
for the operational and axiomatic models.
As I wrote later in the mail, for the operational model it is quite 
clear that x==1 should be allowed for lock() and unlock(), but would 
probably be forbidden for down() and up().
My clarification request is whether that difference in the probable 
operational model should be reflected in the axiomatic model (as I first 
suspected based on the word "semaphore" being dropped a lot), or whether 
it's just due to abuse (i.e., yes the axiomatic model and operational 
model might be different here, but you're not allowed to look).
Which brings us to the next point:

> Could you please review the remainder to see what remains given the
> usage restrictions that I called out above?

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

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.

Perhaps it would also be good to add special tags for Srcu-down and 
Srcu-up to avoid collisions.

always have fun, jonas