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

From: Jonas Oberhauser
Date: Fri Jan 20 2023 - 17:22:15 EST



On 1/20/2023 4:47 PM, Paul E. McKenney wrote:
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.

I think at the very least it would be nice if the convention was written down somewhere.

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

Luckily, I currently don't have a stake in this :D
I currently don't think it's necessary to take a peek at cookies before deciding whether it should be used or not, since the decision can't depend on the value of the cookie anyways.


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.

Too bad, I was aiming for dazed and amazed. Ah well, I'll take what I can get.

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

Let me use up/down names and also fix the statement a little bit in analogy to the other issue we had with the rf from the other subthread.

let  use-cookie = (data|[~(Srcu-up|Srcu-unlock)] ; rfe)* ; data

flag ~empty [Srcu-down] ; use-cookie; [~Srcu-up] ; rf ; [~ domain(use-cookie;[Srcu-up])] as thrown-srcu-cookie-on-floor

Here use-cookie is essentially just a name for the relation we used before to see where the cookie is being used in the end when defining how to match srcu events: it links (among other things) an srcu-down to every store that stores the cookie produced by that srcu-down,
and every read that reads such a cookie to the srcu_up() that uses the cookie returned by that read. (Because of how srcu's up() and down() are currently formalized, those two happen to be the same thing, but maybe it helps thinking of them as seperate for now).

Then the relation

[Srcu-down] ; use-cookie ; [~Srcu-up] ; rf ; [~ domain(use-cookie;[Srcu-up])]

links an event X to an event R exactly in the following case:

X ->use-cookie W ->rf R
and X \in Srcu-down, W \not\in Srcu-up, and R \not\in domain(use-cookie;[Srcu-up])

meaning X is an srcu_down(), and its cookie is stored by the write W, and R is a read that looks at the cookie (it reads from W), but(!) the cookie read by R is never used by any srcu_up().

More precisely, imagine that in contrast to what I just claimed, the cookie read by R would actually be used in some srcu_up() event U.
Then R would be linked by use-cookie to U; we would have
  R ->use-cookie U
  and U \in Srcu-up
which we could rewrite as
  R ->use-cookie;[Srcu-up] U

Now because R appears on the left-hand-side of the relation with some event (here U), R is in the domain(*) of this relation :
  R \in domain(use-cookie;[Srcu-up])
which is a contradiction.

In other words, the relation would be non-empty (= the flag is raised) exactly when there is a read R that reads a cookie produced by some srcu_down() event X, but the return value of that read is never used as input to srcu_up().
This seems to be exactly the "drop on the floor" metaphor you mentioned (and from my own experience I know it's bad to drop cookies on the floor).

does that make it more clear why it might be a reasonable formalization of that principle?
jonas

(*anyways I hope so, I always mix up domain and range, but I think domain is the left side and range the right side. I can also barely keep apart reft and light though, so...)