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

[Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>]

On 1/20/2023 4:39 PM, Paul E. McKenney wrote:
> On Fri, Jan 20, 2023 at 10:43:10AM +0100, Jonas Oberhauser wrote:
>
>> I don't think Boqun's patch is hard to repair.
>> Besides the issue you mention, I think it's also missing Sync-srcu, which
>> seems to be linked by loc based on its first argument.
>>
>> How about something like this?
>>
>> let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock |
>> Sync-srcu   flag ~empty ~[ALL_LOCKS | IW] ; loc ; [ALL-LOCKS] as
>> mixed-lock-accesses
>>
>> If you're using something that isn't a lock or intial write on the same location as a lock, you get the flag.
> Wouldn't that unconditionally complain about the first srcu_read_lock()
> in a given process?  Or am I misreading those statements?
> 							

I unfolded the definition step by step and it seems I was careless when 
distributing the ~ over the [] operator.
I should have written:

flag ~empty [~(ALL_LOCKS | IW)] ; loc ; [ALL-LOCKS] as mixed-lock-accesses

but somehow I thought I can save the parentheses by putting the ~ on the 
outside.
Now on the off-chance that this is kind of how you already read the 
relation, let me unfold it step-by-step.

Let's assume that the sequence s of operations on this location is
   s = initial write , (perhaps some gps) , first read lock , read 
lock&unlock&gp ...
then the flag would appear if the specified relation isn't empty. That 
would be the case if there are a and b that are linked by

   a ->[~(ALL_LOCKS | IW)] ; loc ; [ALL-LOCKS] b

This means a is neither in ALL_LOCKS nor in IW, while b is ALL-LOCKS; and furthermore, they are equal to a' and b' resp. that are related by loc, i.e., appear in this sequence s. Thus both a and b are actually appearing both in the sequence s.
However, every event in the sequence s is either in ALL_LOCKS or in IW, which contradicts the assumption that a is in the sequence and in neither of the sets. Because of this contradiction, the flag doesn't appear if the sequence looks like this.

More generally, if every event in the sequence is either the initial write or one of (srcu-) lock,unlock,up,down,sync, there won't be a flag.

In contrast, if the sequence has the form
  s' = initial write, (normal srcu events), some other acces x, (normal srcu events)
and y is one of the srcu events in this sequence, then
  x ->[~(ALL_LOCKS | IW)] ; loc ; [ALL_LOCKS] y
and you get a flag.

Best wishes,
jonas