Messages in this thread | | | Date | Fri, 20 Jan 2023 07:47:09 -0800 | From | "Paul E. McKenney" <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
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
| |