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

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

On 1/17/2023 7:55 PM, Paul E. McKenney wrote:

> On Tue, Jan 17, 2023 at 07:27:29PM +0100, Jonas Oberhauser wrote:
>> On 1/17/2023 6:43 PM, Paul E. McKenney wrote:
>>> Just to see if I understand, different-values yields true if the set
>>> contains multiple elements with the same value mapping to different
>>> values.  Or, to put it another way, if the relation does not correspond
>>> to a function.
>> based on https://lkml.org/lkml/2019/1/10/155:
> Ah, thank you for the pointer!

What troubles me is that this is the only reference I could find as to 
what the meaning of different-values is. Herd7 is a great tool for 
specifying memory models, but the documentation could be heavily improved.

>> I think different-values(r) is the same as r \ same-values, where
>> same-values links all reads and writes that have the same value (e.g.,
>> "write 5 to x" and "read 5 from y").
>>
>> With this in mind, I think the idea is to 1) forbid partial overlap, and
>> using the different-values to 2) force them to provide the appropriate
>> value.
>> This works because apparently srcu-lock is a read and srcu-unlock is a
>> write, so in case of
>> int r1 = srcu-lock(&ss);   ==>  Read(&ss, x), r1 := x
>> ...
>> srcu-unlock(&ss, r1);  ==> Write(&ss, r1), which is Write(&ss, x)
>>
>> This guarantees that the read and write have the same value, hence
>> different-values(...) will be the empty relation, and so no flag.
> Might it instead match the entire event?

Which event?

Btw, if you want to state that a relation is functional (e.g., that 
srcu-rscs only matches each lock event to at most one unlock event), one 
way to do so is to state

flag ~empty ((srcu-rscs ; srcu-rscs^-1) \ id) as srcu-use-multiple-lock

I visualize this as two different locks pointing via srcu-rscs to the 
same unlock.
Analogously,

flag ~empty ((srcu-rscs^-1 ; srcu-rscs) \ id) as srcu-reuse-lock-idx

should flag if a single lock points to two different unlocks (note: in a 
single execution! this does not flag `int idx = srcu_lock(&ss); if { 
...; srcu_unlock(&ss,idx); } else { ... ; srcu_unlock(&ss,idx) ;... } `).

[snipping in here a part written by Alan:]

> I think what you want would be:
>
> let srcu-rscs = ([Srcu-lock] ; data ; [Srcu-unlock]) & loc
>

I think it makes more sense to define
     let srcu-rscs = ([Srcu-lock] ; (whatever relation says "I'm using 
the return value as the second input") ; [Srcu-unlock])
and then to do
     flag ~empty srcu-rscs\loc as srcu-passing-idx-to-wrong-unlock
to flag cases where you try to pass an index from one srcu_struct to 
another.

>>> Agreed, changes must wait for SRCU support in herd7.
>>>
>> I would like instead to be able to give names to the arguments of events
>> that become dependency relations, like
>>     event srcu_unlock(struct srcu_struct *srcu_addr, struct srcu_token
>> *srcu_data)
>> and then
>>      let srcu-rscs = [Srcu-lock] ; srcu_data ; (data; rfi)*
>>
>> Personally I would also like to not have Linux-specific primitives in
>> herd7/cat, that means that to understand LKMM you also need to understand
>> the herd7 tool, and sounds quite brittle.
>>
>> I would prefer if herd7 had some means to define custom events/instructions
>> and uninterpreted relations between them, like
>>
>> relation rf : [write] x [read]
>> [read] <= range(rf)
>> empty rf ;rf^-1 \ id
>>
>> and some way to say
>> [read] ; .return <= rf^-1 ; .data
>> (where .return is a functional relation relating every event to the value it
>> returns, and .xyz is the functional relation relating every event to the
>> value of its argument xyz).
> I am glad that I asked rather than kneejerk filing a bug report.  ;-)

Please send me a link if you open a thread, then I'll voice my wishes as well.
Maybe Luc is in a wish-fulfilling mood?

best wishes,
jonas

PS:

> Other thoughts?

Other than that I added too many [] in my example? :) :( :) I meant

relation rf : write x read
read <= range(rf)
empty rf ;rf^-1 \ id