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

Jonas Oberhauser
2023-01-20T10:13:42Z

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