lkml.org 
[lkml]   [2023]   [Jan]   [25]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
SubjectRe: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics
From


On 1/25/2023 9:21 PM, Alan Stern wrote:
> LKMM has long provided only approximate handling of SRCU read-side
> critical sections. This has not been a pressing problem because LKMM's
> traditional handling is correct for the common cases of non-overlapping
> and properly nested critical sections. However, LKMM's traditional
> handling of partially overlapping critical sections incorrectly fuses
> them into one large critical section.
>
> For example, consider the following litmus test:
>
> ------------------------------------------------------------------------
>
> C C-srcu-nest-5
>
> (*
> * Result: Sometimes
> *
> * This demonstrates non-nested overlapping of SRCU read-side critical
> * sections. Unlike RCU, SRCU critical sections do not unconditionally
> * nest.
> *)
>
> {}
>
> P0(int *x, int *y, struct srcu_struct *s1)
> {
> int r1;
> int r2;
> int r3;
> int r4;
>
> r3 = srcu_read_lock(s1);
> r2 = READ_ONCE(*y);
> r4 = srcu_read_lock(s1);
> srcu_read_unlock(s1, r3);
> r1 = READ_ONCE(*x);
> srcu_read_unlock(s1, r4);
> }
>
> P1(int *x, int *y, struct srcu_struct *s1)
> {
> WRITE_ONCE(*y, 1);
> synchronize_srcu(s1);
> WRITE_ONCE(*x, 1);
> }
>
> locations [0:r1]
> exists (0:r1=1 /\ 0:r2=0)
>
> ------------------------------------------------------------------------
>
> Current mainline incorrectly flattens the two critical sections into
> one larger critical section, giving "Never" instead of the correct
> "Sometimes":
>
> ------------------------------------------------------------------------
>
> $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus
> Test C-srcu-nest-5 Allowed
> States 3
> 0:r1=0; 0:r2=0;
> 0:r1=0; 0:r2=1;
> 0:r1=1; 0:r2=1;
> No
> Witnesses
> Positive: 0 Negative: 3
> Flag srcu-bad-nesting
> Condition exists (0:r1=1 /\ 0:r2=0)
> Observation C-srcu-nest-5 Never 0 3
> Time C-srcu-nest-5 0.01
> Hash=e692c106cf3e84e20f12991dc438ff1b
>
> ------------------------------------------------------------------------
>
> To its credit, it does complain about bad nesting. But with this
> commit we get the following result, which has the virtue of being
> correct:
>
> ------------------------------------------------------------------------
>
> $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus
> Test C-srcu-nest-5 Allowed
> States 4
> 0:r1=0; 0:r2=0;
> 0:r1=0; 0:r2=1;
> 0:r1=1; 0:r2=0;
> 0:r1=1; 0:r2=1;
> Ok
> Witnesses
> Positive: 1 Negative: 3
> Condition exists (0:r1=1 /\ 0:r2=0)
> Observation C-srcu-nest-5 Sometimes 1 3
> Time C-srcu-nest-5 0.05
> Hash=e692c106cf3e84e20f12991dc438ff1b
>
> ------------------------------------------------------------------------
>
> In addition, there are new srcu_down_read() and srcu_up_read()
> functions on their way to mainline. Roughly speaking, these are to
> srcu_read_lock() and srcu_read_unlock() as down() and up() are to
> mutex_lock() and mutex_unlock(). The key point is that
> srcu_down_read() can execute in one process and the matching
> srcu_up_read() in another, as shown in this litmus test:
>
> ------------------------------------------------------------------------
>
> C C-srcu-nest-6
>
> (*
> * Result: Never
> *
> * This would be valid for srcu_down_read() and srcu_up_read().
> *)
>
> {}
>
> P0(int *x, int *y, struct srcu_struct *s1, int *idx, int *f)
> {
> int r2;
> int r3;
>
> r3 = srcu_down_read(s1);
> WRITE_ONCE(*idx, r3);
> r2 = READ_ONCE(*y);
> smp_store_release(f, 1);
> }
>
> P1(int *x, int *y, struct srcu_struct *s1, int *idx, int *f)
> {
> int r1;
> int r3;
> int r4;
>
> r4 = smp_load_acquire(f);
> 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]
> filter (1:r4=1)
> exists (1:r1=1 /\ 0:r2=0)
>
> ------------------------------------------------------------------------
>
> When run on current mainline, this litmus test gets a complaint about
> an unknown macro srcu_down_read(). With this commit:
>
> ------------------------------------------------------------------------
>
> herd7 -conf linux-kernel.cfg C-srcu-nest-6.litmus
> 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.02
> Hash=c1f20257d052ca5e899be508bedcb2a1
>
> ------------------------------------------------------------------------
>
> Note that the user must supply the flag "f" and the "filter" clause,
> similar to what must be done to emulate call_rcu().
>
> The commit works by treating srcu_read_lock()/srcu_down_read() as
> loads and srcu_read_unlock()/srcu_up_read() as stores. This allows us
> to determine which unlock matches which lock by looking for a data
> dependency between them. In order for this to work properly, the data
> dependencies have to be tracked through stores to intermediate
> variables such as "idx" in the litmus test above; this is handled by
> the new carry-srcu-data relation. But it's important here (and in the
> existing carry-dep relation) to avoid tracking the dependencies
> through SRCU unlock stores. Otherwise, in situations resembling:
>
> A: r1 = srcu_read_lock(s);
> B: srcu_read_unlock(s, r1);
> C: r2 = srcu_read_lock(s);
> D: srcu_read_unlock(s, r2);
>
> it would look as if D was dependent on both A and C, because "s" would
> appear to be an intermediate variable written by B and read by C.
> This explains the complications in the definitions of carry-srcu-dep
> and carry-dep.
>
> As a debugging aid, the commit adds a check for errors in which the
> value returned by one call to srcu_read_lock()/srcu_down_read() is
> passed to more than one instance of srcu_read_unlock()/srcu_up_read().
>
> Finally, since these SRCU-related primitives are now treated as
> ordinary reads and writes, we have to add them into the lists of
> marked accesses (i.e., not subject to data races) and lock-related
> accesses (i.e., one shouldn't try to access an srcu_struct with a
> non-lock-related primitive such as READ_ONCE() or a plain write).
>
> [ paulmck: Fix space-before-tab whitespace nit. ]
>
> TBD-contributions-from: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

In general this seems like a good solution for the time being.
I do have a few minor questions.

> ---
>
> tools/memory-model/linux-kernel.bell | 17 +++++------------
> tools/memory-model/linux-kernel.def | 6 ++++--
> tools/memory-model/lock.cat | 6 +++---
> 3 files changed, 12 insertions(+), 17 deletions(-)
>
> 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
> @@ -57,20 +57,13 @@ flag ~empty Rcu-lock \ domain(rcu-rscs)
> flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-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 carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
> +let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) & loc
>
> (* Validate nesting *)
> flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock
> flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock
> +flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches

Have you considered adding
flag ~empty (srcu-rscs ; srcu-rscs^-1) \ id as mixed-srcu-cookie

Although I think one has to be intentionally trying to trick herd
to be violating this. If herd could produce different cookies, this would be
easy to detect just by the different-values flag you already have.


>
> (* Check for use of synchronize_srcu() inside an RCU critical section *)
> flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
> @@ -80,11 +73,11 @@ flag ~empty different-values(srcu-rscs)
>
> (* 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

Good catch! But why wasn't this necessary before? Is it only necessary
now because the accesses became loads and stores (maybe to avoid data
races?)

> 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); }

How do you feel about introducing Srcu-up and Srcu-down with this patch?

> synchronize_srcu(X) { __srcu{sync-srcu}(X); }
> synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); }
>
> Index: usb-devel/tools/memory-model/lock.cat
> ===================================================================
> --- usb-devel.orig/tools/memory-model/lock.cat
> +++ usb-devel/tools/memory-model/lock.cat
> @@ -36,9 +36,9 @@ let RU = try RU with emptyset
> (* Treat RL as a kind of LF: a read with no ordering properties *)
> let LF = LF | RL
>
> -(* There should be no ordinary R or W accesses to spinlocks *)
> -let ALL-LOCKS = LKR | LKW | UL | LF | RU
> -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
> +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *)
> +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu
> +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses

Since this was pointed out by Boqun, would it be appropriate to mention
him in the patch somehow?

> (* Link Lock-Reads to their RMW-partner Lock-Writes *)
> let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)

Thanks for your patience,
jonas

\
 
 \ /
  Last update: 2023-03-26 23:55    [W:0.155 / U:0.856 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site