Messages in this thread | | | Date | Tue, 17 Jan 2023 21:20:54 +0100 | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) | From | Jonas Oberhauser <> |
| |
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
| |