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

[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