From: Kunwu Chan <[email protected]> synchronize_srcu_atomic() may end its grace period immediately when its scan of the per-CPU lock counters finds no readers. Correctness requires the grace-period anchor written by srcu_gp_start() to precede the smp_mb() ordering the lock scan. This ordering ensures that any reader whose lock increment is missed by the scan cannot have incremented its lock counter before the grace-period anchor, and therefore cannot be a pre-existing reader of this grace period.
This litmus test models the key ordering between the grace-period anchor and the lock counter scan, where "seq" models the grace-period anchor in ->srcu_gp_seq and "ctr" models the per-CPU ->srcu_ctrs[].srcu_locks counter. P0 writes the anchor before the smp_mb() and the lock scan. P1 models the reader-side counter increment, with the smp_mb() of __srcu_read_lock() following the increment. P2 models an observer that sees the reader's increment before seeing the anchor. The outcome is forbidden by LKMM, and herd7 reports "Never". See SRCU-fastpath-scan-before-anchor.litmus for the reversed ordering, which permits this outcome. Tested with herd7 7.58 using linux-kernel.cfg. Signed-off-by: Kunwu Chan <[email protected]> --- .../SRCU-fastpath-anchor-before-scan.litmus | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus diff --git a/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus b/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus new file mode 100644 index 000000000000..8200a75e15ef --- /dev/null +++ b/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus @@ -0,0 +1,56 @@ +C SRCU-fastpath-anchor-before-scan + +(* + * Result: Never + * + * The synchronize_srcu_atomic() fastpath may end its grace period + * immediately when its scan of the per-CPU lock counters finds no + * readers. Correctness requires the grace-period anchor written by + * srcu_gp_start() to precede the smp_mb() ordering the lock scan. + * This ordering ensures that any reader whose lock increment is missed + * by the scan cannot have incremented its lock counter before the + * grace-period anchor, and therefore cannot be a pre-existing reader + * of this grace period. + * + * This litmus test models the key ordering between the grace-period + * anchor and the lock counter scan, where "seq" models the + * grace-period anchor in ->srcu_gp_seq and "ctr" models the per-CPU + * ->srcu_ctrs[].srcu_locks counter. P0 writes the anchor before the + * smp_mb() and the lock scan. P1 models the reader-side counter + * increment, with the smp_mb() of __srcu_read_lock() following the + * increment. P2 models an observer that sees the reader's increment + * before seeing the anchor. + * + * The outcome is forbidden by LKMM, and herd7 reports "Never". See + * SRCU-fastpath-scan-before-anchor.litmus for the reversed ordering, + * which permits this outcome. + *) + +{} + +P0(int *seq, int *ctr) +{ + int r2; + + WRITE_ONCE(*seq, 1); + smp_mb(); + r2 = READ_ONCE(*ctr); +} + +P1(int *ctr) +{ + WRITE_ONCE(*ctr, 1); + smp_mb(); +} + +P2(int *seq, int *ctr) +{ + int r3; + int r4; + + r3 = READ_ONCE(*ctr); + smp_mb(); + r4 = READ_ONCE(*seq); +} + +exists (0:r2 = 0 /\ 2:r3 = 1 /\ 2:r4 = 0) -- 2.43.0
