Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
From: Jonas Oberhauser
Date: Fri Jan 20 2023 - 07:51:46 EST
I'm not going to get it right today, am I?
+let srcu-rscs = ([Srcu-lock] ; (data ; [~ Srcu-unlock] ; rfe) * ; data
; [Srcu-unlock]) & loc
I see now that I copied the format from your message but without
realizing the original had a `|` where I have a `;`.
I hope this version is finally right and perhaps more natural than the
(data | rf) version, considering rf can't actually appear in most places
and this more closely matches carry-dep;data.
But of course feel free to use
+let srcu-rscs = ([Srcu-lock] ; (data | [~ Srcu-unlock] ; rf)+ ;
[Srcu-unlock]) & loc
instead if you prefer.
have fun, jonas
On 1/20/2023 1:34 PM, Jonas Oberhauser wrote:
I just realized I made a mistake in my earlier response to this
message; you still need the rf for passing the cookie across threads.
Perhaps it's better to just also exclude srcu_unlock type events
explicitly here.
+let srcu-rscs = ([Srcu-lock] ; (data ; [~ Srcu-unlock] ; rf) + ;
[Srcu-unlock]) & loc
best wishes,
jonas
On 1/20/2023 4:55 AM, Paul E. McKenney wrote:
On Thu, Jan 19, 2023 at 02:51:53PM -0500, Alan Stern wrote:
On Thu, Jan 19, 2023 at 10:41:07AM -0800, Paul E. McKenney wrote:
In contrast, this actually needs srcu_down_read() and srcu_up_read():
------------------------------------------------------------------------
C C-srcu-nest-6
(*
* Result: Never
*
* Flag unbalanced-srcu-locking
* This would be valid for srcu_down_read() and srcu_up_read().
*)
{}
P0(int *x, int *y, struct srcu_struct *s1, int *idx)
{
int r2;
int r3;
r3 = srcu_down_read(s1);
WRITE_ONCE(*idx, r3);
r2 = READ_ONCE(*y);
}
P1(int *x, int *y, struct srcu_struct *s1, int *idx)
{
int r1;
int r3;
r1 = READ_ONCE(*x);
r3 = READ_ONCE(*idx);
srcu_up_read(s1, r3);
}
P2(int *x, int *y, struct srcu_struct *s1)
{
WRITE_ONCE(*y, 1);
synchronize_srcu(s1);
WRITE_ONCE(*x, 1);
}
locations [0:r1]
exists (1:r1=1 /\ 0:r2=0)
I modified this litmus test by adding a flag variable with an
smp_store_release in P0, an smp_load_acquire in P1, and a filter clause
to ensure that P1 reads the flag and idx from P1.
With the patch below, the results were as expected:
Test C-srcu-nest-6 Allowed
States 3
0:r1=0; 0:r2=0; 1:r1=0;
0:r1=0; 0:r2=1; 1:r1=0;
0:r1=0; 0:r2=1; 1:r1=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (1:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-6 Never 0 3
Time C-srcu-nest-6 0.04
Hash=2b010cf3446879fb84752a6016ff88c5
It turns out that the idea of removing rf edges from Srcu-unlock events
doesn't work well. The missing edges mess up herd's calculation of the
fr relation and the coherence axiom. So I've gone back to filtering
those edges out of carry-dep.
Also, Boqun's suggestion for flagging ordinary accesses to SRCU
structures no longer works, because the lock and unlock operations now
_are_ normal accesses. I removed that check too, but it shouldn't hurt
much because I don't expect to encounter litmus tests that try to read
or write srcu_structs directly.
Alan
Index: usb-devel/tools/memory-model/linux-kernel.bell
===================================================================
--- usb-devel.orig/tools/memory-model/linux-kernel.bell
+++ usb-devel/tools/memory-model/linux-kernel.bell
@@ -53,38 +53,30 @@ let rcu-rscs = let rec
in matched
(* Validate nesting *)
-flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
-flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
+flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-lock
+flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-unlock
(* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
-let srcu-rscs = let rec
- unmatched-locks = Srcu-lock \ domain(matched)
- and unmatched-unlocks = Srcu-unlock \ range(matched)
- and unmatched = unmatched-locks | unmatched-unlocks
- and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
- and unmatched-locks-to-unlocks =
- ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
- and matched = matched | (unmatched-locks-to-unlocks \
- (unmatched-po ; unmatched-po))
- in matched
+let srcu-rscs = ([Srcu-lock] ; (data | rf)+ ; [Srcu-unlock]) & loc
(* Validate nesting *)
-flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
-flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
+flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-lock
+flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-unlock
+flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches
(* Check for use of synchronize_srcu() inside an RCU critical
section *)
flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
(* Validate SRCU dynamic match *)
-flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
+flag ~empty different-values(srcu-rscs) as bad-srcu-value-match
(* Compute marked and plain memory accesses *)
let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) |
range(rmw) |
- LKR | LKW | UL | LF | RL | RU
+ LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
let Plain = M \ Marked
(* Redefine dependencies to include those carried through plain
accesses *)
-let carry-dep = (data ; rfi)*
+let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
let addr = carry-dep ; addr
let ctrl = carry-dep ; ctrl
let data = carry-dep ; data
Index: usb-devel/tools/memory-model/linux-kernel.def
===================================================================
--- usb-devel.orig/tools/memory-model/linux-kernel.def
+++ usb-devel/tools/memory-model/linux-kernel.def
@@ -49,8 +49,10 @@ synchronize_rcu() { __fence{sync-rcu}; }
synchronize_rcu_expedited() { __fence{sync-rcu}; }
// SRCU
-srcu_read_lock(X) __srcu{srcu-lock}(X)
-srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
+srcu_read_lock(X) __load{srcu-lock}(*X)
+srcu_read_unlock(X,Y) { __store{srcu-unlock}(*X,Y); }
+srcu_down_read(X) __load{srcu-lock}(*X)
+srcu_up_read(X,Y) { __store{srcu-unlock}(*X,Y); }
synchronize_srcu(X) { __srcu{sync-srcu}(X); }
synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); }
And for some initial tests:
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-1.litmus
"Flag multiple-srcu-matches" but otherwise OK.
As a "hail Mary" exercise, I used r4 for the second SRCU
read-side critical section, but this had no effect.
(This flag is expected and seen for #4 below.)
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-2.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-3.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-4.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-5.litmus
All as expected.
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-6.litmus
Get "Flag unbalanced-srcu-lock" and "Flag unbalanced-srcu-unlock",
but this is srcu_down_read() and srcu_up_read(), where this should
be OK. Ah, but I need to do the release/acquire/filter trick.
Once
I did that, it works as expected.
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-7.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/kernel/C-srcu-nest-8.litmus
Both as expected.
Getting there!!!
I also started a regression test, hopefully without pilot error. :-/
Thanx, Paul