[PATCH 02/13] litmus: Add SRCU fastpath scan-before-anchor test

[Kunwu Chan]

From: Kunwu Chan <kunwu.chan@xxxxxxxxx>

If the synchronize_srcu_atomic() fastpath instead places its lock scan
before the grace-period anchor, the scan can miss a reader whose
increment was already visible before the anchor.  That reader already
existed when the grace period started, so completing the grace period
without waiting for it would violate the SRCU grace-period guarantee.

This litmus test models the reversed ordering, with the lock scan placed
before the grace-period anchor.  "seq" models the grace-period anchor in
->srcu_gp_seq and "ctr" models the per-CPU ->srcu_ctrs[].srcu_locks
counter.  P0 scans the lock counter before writing the anchor, with an
smp_mb() between them.  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 same outcome is allowed with this ordering, and herd7 reports
"Sometimes".  The litmus-tests README is also updated to describe both
SRCU fastpath tests.

Tested with herd7 7.58 using linux-kernel.cfg.

Signed-off-by: Kunwu Chan <kunwu.chan@xxxxxxxxx>
---
 tools/memory-model/litmus-tests/README        | 16 ++++++
 .../SRCU-fastpath-scan-before-anchor.litmus   | 53 +++++++++++++++++++
 2 files changed, 69 insertions(+)
 create mode 100644 tools/memory-model/litmus-tests/SRCU-fastpath-scan-before-anchor.litmus

diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index d311a0ff1ae6..449747c6db9e 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -137,6 +137,22 @@ S+fencewmbonceonce+poacquireonce.litmus
 	Can a smp_wmb(), instead of a release, and an acquire order
 	a prior store against a subsequent store?
 
+SRCU-fastpath-anchor-before-scan.litmus
+	This models the synchronize_srcu_atomic() fastpath with the
+	grace-period anchor ordered before the lock-counter scan.  This
+	ordering prevents readers that existed before the grace period
+	from being missed by the scan.  See
+	SRCU-fastpath-scan-before-anchor.litmus for the reversed
+	ordering.
+
+SRCU-fastpath-scan-before-anchor.litmus
+	This models the synchronize_srcu_atomic() fastpath with the
+	lock-counter scan ordered before the grace-period anchor.  This
+	permits the scan to miss readers that existed before the grace
+	period, violating the SRCU grace-period guarantee.  See
+	SRCU-fastpath-anchor-before-scan.litmus for the opposite
+	ordering.
+
 WRC+poonceonces+Once.litmus
 WRC+pooncerelease+fencermbonceonce+Once.litmus
 	These two are members of an extension of the MP litmus-test
diff --git a/tools/memory-model/litmus-tests/SRCU-fastpath-scan-before-anchor.litmus b/tools/memory-model/litmus-tests/SRCU-fastpath-scan-before-anchor.litmus
new file mode 100644
index 000000000000..931a41014de7
--- /dev/null
+++ b/tools/memory-model/litmus-tests/SRCU-fastpath-scan-before-anchor.litmus
@@ -0,0 +1,53 @@
+C SRCU-fastpath-scan-before-anchor
+
+(*
+ * Result: Sometimes
+ *
+ * If the synchronize_srcu_atomic() fastpath instead places its lock
+ * scan before the grace-period anchor, the scan can miss a reader whose
+ * increment was already visible before the anchor.  That reader already
+ * existed when the grace period started, so completing the grace period
+ * without waiting for it would violate the SRCU grace-period guarantee.
+ *
+ * This litmus test models the reversed ordering, with the lock scan
+ * placed before the grace-period anchor.  "seq" models the grace-period
+ * anchor in ->srcu_gp_seq and "ctr" models the per-CPU
+ * ->srcu_ctrs[].srcu_locks counter.  P0 scans the lock counter before
+ * writing the anchor, with an smp_mb() between them.  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 same outcome is allowed with this ordering, and herd7 reports
+ * "Sometimes".  See SRCU-fastpath-anchor-before-scan.litmus for the
+ * opposite ordering, which forbids this outcome.
+ *)
+
+{}
+
+P0(int *seq, int *ctr)
+{
+	int r2;
+
+	r2 = READ_ONCE(*ctr);
+	smp_mb();
+	WRITE_ONCE(*seq, 1);
+}
+
+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