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

Jonas Oberhauser
2023-01-20T22:22:15Z

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