Messages in this thread | | | Date | Tue, 17 Jan 2023 15:15:06 -0500 | From | Alan Stern <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
On Tue, Jan 17, 2023 at 09:43:08AM -0800, Paul E. McKenney wrote: > On Tue, Jan 17, 2023 at 10:56:34AM -0500, Alan Stern wrote: > > Isn't it true that the current code will flag srcu-bad-nesting if a > > litmus test has non-nested overlapping SRCU read-side critical sections? > > Now that you mention it, it does indeed, flagging srcu-bad-nesting. > > 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.
As I understand it, given a relation r (i.e., a set of pairs of events), different-values(r) returns the sub-relation consisting of those pairs in r for which the value associated with the first event of the pair is different from the value associated with the second event of the pair.
For srcu_read_lock() and loads in general, the associated value is the value returned by the function call. For srcu_read_unlock() and stores in general, the associated value is the value (i.e., the second argument) passed to the function call.
> Or am I still missing something? > > > And if it is true, is there any need to change the memory model at this > > point? > > > > (And if it's not true, that's most likely due to a bug in herd7.) > > Agreed, changes must wait for SRCU support in herd7.
Apparently the only change necessary is to make the srcu_read_lock and srcu_read_unlock events act like loads and stores. In particular, they need to be subject to the standard rules for calculating dependencies.
Right now the behavior is kind of strange. The following simple litmus test:
C test {} P0(int *x) { int r1; r1 = srcu_read_lock(x); srcu_read_unlock(x, r1); } exists (~0:r1=0)
produces the following output from herd7:
Test test Allowed States 1 0:r1=906; Ok Witnesses Positive: 1 Negative: 0 Condition exists (not (0:r1=0)) Observation test Always 1 0 Time test 0.01 Hash=2f42c87ae9c1d267f4e80c66f646b9bb
Don't ask me where that 906 value comes from or why it is't 0. Also, herd7's graphical output shows there is no data dependency from the lock to the unlock, but we need to have one.
> At which point something roughly similar to this might work? > > let srcu-rscs = return_value(Srcu-lock) ; (dep | rfi)* ; > parameter(Srcu-unlock, 2)
I can't tell what that's supposed to mean. In any case, I think what you want would be:
let srcu-rscs = ([Srcu-lock] ; data ; [Srcu-unlock]) & loc
> Given an Srcu-down and an Srcu-up: > > let srcu-rscs = ( return_value(Srcu-lock) ; (dep | rfi)* ; > parameter(Srcu-unlock, 2) ) | > ( return_value(Srcu-down) ; (dep | rf)* ; > parameter(Srcu-up, 2) ) > > Seem reasonable, or am I missing yet something else?
Not at all reasonable.
For one thing, consider this question: Which statements lie inside a read-side critical section?
With srcu_read_lock() and a matching srcu_read_unlock(), the answer is clear: All statements po-between the two. With srcu_down_read() and srcu_up_read(), the answer is cloudy in the extreme.
Also, bear in mind that the Fundamental Law of RCU is formulated in terms of stores propagating to a critical section's CPU. What are we to make of this when a single critical section can belong to more than one CPU?
Indeed, given:
P0(int *x) { srcu_down_read(x); }
P1(int *x) { srcu_up_read(x); }
what are we to make of executions in which P1 executes before P0?
Alan
| |