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

[Paul E. McKenney]

On Fri, Jan 20, 2023 at 11:13:00AM +0100, Jonas Oberhauser wrote:
> 
> 
> 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().

Agreed, the math might say something or another about doing something
with the srcu_read_lock() or srcu_down_read() return values (other than
passing them to srcu_read_unlock() or srcu_up_read(), respectively),
but such somethings are excluded by convention.

So it would be nice for LKMM to complain about such abuse, but not
at all mandatory.

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

For the moment, I am taking the door labeled "abuse".

Maybe someday someone will come up with a valid use case, but they have
to prove it first.  ;-)

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

I like the general idea, but I am dazed and confused by this "flag"
statement.

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

Ah, separate down/up tags could make this "flag" statement at least
somewhat less dazing and confusing.

> always have fun, jonas

Always do!  ;-)

							Thanx, Paul