[RFC PATCH v25 10/14] tools/testing/hpcc: add litmus tests of the memory ordering

[Mathieu Desnoyers <mathieu.desnoyers@efficios.com>]

The limit counters rely on memory ordering. So do the carries and the
publication of the tree by lazy activation. A test on real hardware
cannot show that an ordering is needed: a missing barrier may never
fail in practice. The userspace test runs on one thread only.

Check each of these orderings with the Linux kernel memory model
instead. The litmus tests cover:

- The publication of the tree: the update fast path, the carry slow
  path, the precise sum and the approximate sum.
- The carries of percpu_counter_tree_add(), against the precise sum.
- The limit counters: the carries of the additions, an addition undone,
  an amount freed on another CPU, and two concurrent checks.

herd7 reports "Never" for the 12 tests of the code as it is. 9 variants
drop one ordering each, and herd7 reports "Sometimes" for them. This
shows that these orderings are needed. The README explains how to run
the tests, and the comments of the library now point at them.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
---
 lib/percpu_counter_tree.c                     |  8 ++-
 tools/testing/hpcc/litmus/README              | 61 +++++++++++++++++++
 .../leave-first-precise-sum-relaxed.litmus    | 37 +++++++++++
 .../litmus/leave-first-precise-sum.litmus     | 41 +++++++++++++
 .../litmus/limit-arrive-first-acquire.litmus  | 38 ++++++++++++
 .../limit-arrive-first-unordered.litmus       | 37 +++++++++++
 .../hpcc/litmus/limit-arrive-first.litmus     | 41 +++++++++++++
 .../hpcc/litmus/limit-free-level0-nomb.litmus | 40 ++++++++++++
 .../hpcc/litmus/limit-free-level0.litmus      | 43 +++++++++++++
 .../hpcc/litmus/limit-free-root.litmus        | 42 +++++++++++++
 .../litmus/limit-last-checker-nomb.litmus     | 28 +++++++++
 .../hpcc/litmus/limit-last-checker.litmus     | 33 ++++++++++
 .../hpcc/litmus/limit-undo-level0.litmus      | 35 +++++++++++
 .../hpcc/litmus/limit-undo-root-rmb.litmus    | 30 +++++++++
 .../litmus/limit-undo-root-unordered.litmus   | 29 +++++++++
 .../hpcc/litmus/limit-undo-root.litmus        | 32 ++++++++++
 .../litmus/publish-approximate-sum.litmus     | 40 ++++++++++++
 .../hpcc/litmus/publish-carry-normb.litmus    | 36 +++++++++++
 .../testing/hpcc/litmus/publish-carry.litmus  | 43 +++++++++++++
 .../publish-precise-sum-noacquire.litmus      | 38 ++++++++++++
 .../hpcc/litmus/publish-precise-sum.litmus    | 44 +++++++++++++
 .../litmus/publish-update-norelease.litmus    | 34 +++++++++++
 .../testing/hpcc/litmus/publish-update.litmus | 40 ++++++++++++
 23 files changed, 848 insertions(+), 2 deletions(-)
 create mode 100644 tools/testing/hpcc/litmus/README
 create mode 100644 tools/testing/hpcc/litmus/leave-first-precise-sum-relaxed.litmus
 create mode 100644 tools/testing/hpcc/litmus/leave-first-precise-sum.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-arrive-first-acquire.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-arrive-first-unordered.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-arrive-first.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-free-level0-nomb.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-free-level0.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-free-root.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-last-checker-nomb.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-last-checker.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-undo-level0.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-undo-root-rmb.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-undo-root-unordered.litmus
 create mode 100644 tools/testing/hpcc/litmus/limit-undo-root.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-approximate-sum.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-carry-normb.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-carry.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-precise-sum-noacquire.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-precise-sum.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-update-norelease.litmus
 create mode 100644 tools/testing/hpcc/litmus/publish-update.litmus

diff --git a/lib/percpu_counter_tree.c b/lib/percpu_counter_tree.c
index 9c172fc3e4d7..fcffc3d073ca 100644
--- a/lib/percpu_counter_tree.c
+++ b/lib/percpu_counter_tree.c
@@ -552,7 +552,9 @@ EXPORT_SYMBOL_GPL(percpu_counter_tree_init_many_lazy);
  * The read barriers between the levels of the precise sum are unrelated
  * to the publication: they order carries, see
  * percpu_counter_tree_precise_sum_unbiased().
-
+ *
+ * The litmus tests in tools/testing/hpcc/litmus check these orderings
+ * with the Linux kernel memory model, and those of the carries.
  */
 
 /**
@@ -1261,7 +1263,9 @@ EXPORT_SYMBOL_GPL(percpu_counter_tree_batch_for_accuracy);
  * retries once when the value leaves room for it.
  *
  * Both counters wrap around: all the arithmetic is modular.
-
+ *
+ * The litmus tests in tools/testing/hpcc/litmus check these orderings
+ * with the Linux kernel memory model.
  */
 
 /*
diff --git a/tools/testing/hpcc/litmus/README b/tools/testing/hpcc/litmus/README
new file mode 100644
index 000000000000..16c234a76786
--- /dev/null
+++ b/tools/testing/hpcc/litmus/README
@@ -0,0 +1,61 @@
+Litmus tests of lib/percpu_counter_tree.c. They check its memory
+ordering arguments with the Linux kernel memory model. Each test models
+one argument. A test with the result "Sometimes" drops one ordering of
+the code, to show that the argument needs it.
+
+The model has no atomic_long_t: the tests use atomic_t, with the same
+ordering. The per-CPU counters are plain int.
+
+Run them from tools/memory-model, with herd7 installed:
+
+  cd tools/memory-model
+  for f in ../testing/hpcc/litmus/*.litmus; do
+	herd7 -conf linux-kernel.cfg $f | grep Observation
+  done
+
+Each observation must match the "Result" in the comment of its test.
+
+Publication of the tree, see "Publication of the tree":
+
+  publish-update.litmus, publish-update-norelease.litmus
+    The update fast path reads level0, then its per-CPU counter.
+
+  publish-carry.litmus, publish-carry-normb.litmus
+    The carry slow path reads approx_sum after a read barrier.
+
+  publish-precise-sum.litmus, publish-precise-sum-noacquire.litmus
+    The precise sum reads level0 with an acquire.
+
+  publish-approximate-sum.litmus
+    The approximate sum reads the root through approx_sum.
+
+Carries of percpu_counter_tree_add(), see
+percpu_counter_tree_precise_sum_unbiased():
+
+  leave-first-precise-sum.litmus, leave-first-precise-sum-relaxed.litmus
+    A carry leaves each level before it arrives at the next one. The
+    precise sum, read from the root down, never counts it twice.
+
+Limit counters, see "Limit counters":
+
+  limit-arrive-first.litmus, limit-arrive-first-acquire.litmus,
+  limit-arrive-first-unordered.litmus
+    A carry of the additions arrives at each level before it leaves the
+    level below. The precise sum, read from level 0 up, never misses it.
+    The root update must be fully ordered.
+
+  limit-undo-root.litmus, limit-undo-root-rmb.litmus,
+  limit-undo-root-unordered.litmus, limit-undo-level0.litmus
+    An addition undone on the same CPU. The check reads the
+    subtractions, then the additions. It never sees the subtraction
+    without the addition.
+
+  limit-free-root.litmus, limit-free-level0.litmus,
+  limit-free-level0-nomb.litmus
+    An amount added on one CPU and subtracted on another one, which
+    found it through a release and an acquire. The full barrier after
+    the addition orders it before a subtraction which stays in level 0.
+
+  limit-last-checker.litmus, limit-last-checker-nomb.litmus
+    Two concurrent additions, each checked after a full barrier. At
+    least one check sees the other addition.
diff --git a/tools/testing/hpcc/litmus/leave-first-precise-sum-relaxed.litmus b/tools/testing/hpcc/litmus/leave-first-precise-sum-relaxed.litmus
new file mode 100644
index 000000000000..951b7c39bbbc
--- /dev/null
+++ b/tools/testing/hpcc/litmus/leave-first-precise-sum-relaxed.litmus
@@ -0,0 +1,37 @@
+C leave-first-precise-sum-relaxed
+
+(*
+ * Result: Sometimes
+ *
+ * Like leave-first-precise-sum, with a relaxed arrival at the middle
+ * item. The precise sum can then count the carry twice.
+ *)
+
+{
+	l0=1;
+}
+
+P0(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r;
+
+	r = cmpxchg_relaxed(l0, 1, 0);
+	r = atomic_add_return_relaxed(1, item);
+	r = atomic_cmpxchg_relaxed(item, 1, 0);
+	r = atomic_add_return_release(1, root);
+}
+
+P1(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r0;
+	int r1;
+	int r2;
+
+	r2 = atomic_read(root);
+	smp_rmb();
+	r1 = atomic_read(item);
+	smp_rmb();
+	r0 = READ_ONCE(*l0);
+}
+
+exists ((1:r2=1 /\ 1:r1=1) \/ (1:r2=1 /\ 1:r0=1) \/ (1:r1=1 /\ 1:r0=1))
diff --git a/tools/testing/hpcc/litmus/leave-first-precise-sum.litmus b/tools/testing/hpcc/litmus/leave-first-precise-sum.litmus
new file mode 100644
index 000000000000..a80ddb605d4e
--- /dev/null
+++ b/tools/testing/hpcc/litmus/leave-first-precise-sum.litmus
@@ -0,0 +1,41 @@
+C leave-first-precise-sum
+
+(*
+ * Result: Never
+ *
+ * A carry of percpu_counter_tree_add(), from the level 0 counter l0 to
+ * the root through a middle item. It leaves each level before it
+ * arrives at the next one, with a release. The precise sum reads the
+ * root, the item and level 0, with read barriers. It never counts the
+ * carry twice. This also keeps the sum of the subtractions of a limit
+ * counter from being above their value.
+ *)
+
+{
+	l0=1;
+}
+
+P0(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r;
+
+	r = cmpxchg_relaxed(l0, 1, 0);
+	r = atomic_add_return_release(1, item);
+	r = atomic_cmpxchg_relaxed(item, 1, 0);
+	r = atomic_add_return_release(1, root);
+}
+
+P1(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r0;
+	int r1;
+	int r2;
+
+	r2 = atomic_read(root);
+	smp_rmb();
+	r1 = atomic_read(item);
+	smp_rmb();
+	r0 = READ_ONCE(*l0);
+}
+
+exists ((1:r2=1 /\ 1:r1=1) \/ (1:r2=1 /\ 1:r0=1) \/ (1:r1=1 /\ 1:r0=1))
diff --git a/tools/testing/hpcc/litmus/limit-arrive-first-acquire.litmus b/tools/testing/hpcc/litmus/limit-arrive-first-acquire.litmus
new file mode 100644
index 000000000000..f5f06dd0ff08
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-arrive-first-acquire.litmus
@@ -0,0 +1,38 @@
+C limit-arrive-first-acquire
+
+(*
+ * Result: Sometimes
+ *
+ * Like limit-arrive-first, with an acquire add at the root. The acquire
+ * only orders the read of the add. The departures can then be seen
+ * before the arrival at the root, and the sum misses the carry.
+ *)
+
+{
+	l0 = 1;
+}
+
+P0(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r;
+
+	r = atomic_cmpxchg(item, 0, 1);
+	r = atomic_add_return_acquire(1, root);
+	atomic_sub(1, item);
+	WRITE_ONCE(*l0, 0);
+}
+
+P1(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r0;
+	int r1;
+	int r2;
+
+	r0 = READ_ONCE(*l0);
+	smp_rmb();
+	r1 = atomic_read(item);
+	smp_rmb();
+	r2 = atomic_read(root);
+}
+
+exists (1:r0=0 /\ 1:r1=0 /\ 1:r2=0)
diff --git a/tools/testing/hpcc/litmus/limit-arrive-first-unordered.litmus b/tools/testing/hpcc/litmus/limit-arrive-first-unordered.litmus
new file mode 100644
index 000000000000..9d870c2e0aa2
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-arrive-first-unordered.litmus
@@ -0,0 +1,37 @@
+C limit-arrive-first-unordered
+
+(*
+ * Result: Sometimes
+ *
+ * Like limit-arrive-first, with an unordered add at the root. The sum
+ * can miss the carry.
+ *)
+
+{
+	l0 = 1;
+}
+
+P0(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r;
+
+	r = atomic_cmpxchg(item, 0, 1);
+	atomic_add(1, root);
+	atomic_sub(1, item);
+	WRITE_ONCE(*l0, 0);
+}
+
+P1(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r0;
+	int r1;
+	int r2;
+
+	r0 = READ_ONCE(*l0);
+	smp_rmb();
+	r1 = atomic_read(item);
+	smp_rmb();
+	r2 = atomic_read(root);
+}
+
+exists (1:r0=0 /\ 1:r1=0 /\ 1:r2=0)
diff --git a/tools/testing/hpcc/litmus/limit-arrive-first.litmus b/tools/testing/hpcc/litmus/limit-arrive-first.litmus
new file mode 100644
index 000000000000..9d9f6efdf0aa
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-arrive-first.litmus
@@ -0,0 +1,41 @@
+C limit-arrive-first
+
+(*
+ * Result: Never
+ *
+ * A carry of the additions of a limit counter, from the level 0 counter
+ * l0 to the root through a middle item, as in
+ * percpu_counter_tree_add_arrive_first(). It arrives at the item with a
+ * fully ordered cmpxchg, and at the root with a fully ordered add. Then
+ * it leaves the item and level 0. The precise sum reads level 0, the
+ * item and the root, with read barriers. It never misses the carry.
+ *)
+
+{
+	l0 = 1;
+}
+
+P0(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r;
+
+	r = atomic_cmpxchg(item, 0, 1);
+	r = atomic_add_return(1, root);
+	atomic_sub(1, item);
+	WRITE_ONCE(*l0, 0);
+}
+
+P1(int *l0, atomic_t *item, atomic_t *root)
+{
+	int r0;
+	int r1;
+	int r2;
+
+	r0 = READ_ONCE(*l0);
+	smp_rmb();
+	r1 = atomic_read(item);
+	smp_rmb();
+	r2 = atomic_read(root);
+}
+
+exists (1:r0=0 /\ 1:r1=0 /\ 1:r2=0)
diff --git a/tools/testing/hpcc/litmus/limit-free-level0-nomb.litmus b/tools/testing/hpcc/litmus/limit-free-level0-nomb.litmus
new file mode 100644
index 000000000000..d220bab401ac
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-free-level0-nomb.litmus
@@ -0,0 +1,40 @@
+C limit-free-level0-nomb
+
+(*
+ * Result: Sometimes
+ *
+ * Like limit-free-level0, without the full barrier after the addition.
+ * The release of the page does not order the addition before the
+ * unordered subtraction of CPU 1, for CPU 2. The precise sum can then
+ * see the subtraction without the addition.
+ *)
+
+{}
+
+P0(int *l0p, int *page)
+{
+	WRITE_ONCE(*l0p, 1);
+	smp_store_release(page, 1);
+}
+
+P1(int *l0n, int *page)
+{
+	int r0;
+	int r;
+
+	r0 = smp_load_acquire(page);
+	if (r0 == 1)
+		r = cmpxchg_relaxed(l0n, 0, 1);
+}
+
+P2(int *l0p, int *l0n)
+{
+	int r0;
+	int r1;
+
+	r0 = READ_ONCE(*l0n);
+	smp_rmb();
+	r1 = READ_ONCE(*l0p);
+}
+
+exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
diff --git a/tools/testing/hpcc/litmus/limit-free-level0.litmus b/tools/testing/hpcc/litmus/limit-free-level0.litmus
new file mode 100644
index 000000000000..cb5d6b083ecf
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-free-level0.litmus
@@ -0,0 +1,43 @@
+C limit-free-level0
+
+(*
+ * Result: Never
+ *
+ * CPU 0 adds to its level 0 counter of the additions l0p. The full
+ * barrier of percpu_counter_tree_limit_add() follows. Then CPU 0
+ * publishes the page it charged. CPU 1 finds the page and frees it: the
+ * subtraction stays in its level 0 counter of the subtractions l0n,
+ * without ordering. The precise sum of CPU 2 reads l0n, then l0p after a
+ * read barrier. It never sees the subtraction without the addition.
+ *)
+
+{}
+
+P0(int *l0p, int *page)
+{
+	WRITE_ONCE(*l0p, 1);
+	smp_mb();
+	smp_store_release(page, 1);
+}
+
+P1(int *l0n, int *page)
+{
+	int r0;
+	int r;
+
+	r0 = smp_load_acquire(page);
+	if (r0 == 1)
+		r = cmpxchg_relaxed(l0n, 0, 1);
+}
+
+P2(int *l0p, int *l0n)
+{
+	int r0;
+	int r1;
+
+	r0 = READ_ONCE(*l0n);
+	smp_rmb();
+	r1 = READ_ONCE(*l0p);
+}
+
+exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
diff --git a/tools/testing/hpcc/litmus/limit-free-root.litmus b/tools/testing/hpcc/litmus/limit-free-root.litmus
new file mode 100644
index 000000000000..d3f267311411
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-free-root.litmus
@@ -0,0 +1,42 @@
+C limit-free-root
+
+(*
+ * Result: Never
+ *
+ * CPU 0 adds to the root of the additions p, then publishes the page it
+ * charged. CPU 1 finds the page and frees it: its carry reaches the root
+ * of the subtractions n with a release. CPU 2 checks: it reads n with an
+ * acquire, then p. It never sees the subtraction without the
+ * addition.
+ *)
+
+{}
+
+P0(atomic_t *p, int *page)
+{
+	int r;
+
+	r = atomic_add_return(1, p);
+	smp_store_release(page, 1);
+}
+
+P1(atomic_t *n, int *page)
+{
+	int r0;
+	int r;
+
+	r0 = smp_load_acquire(page);
+	if (r0 == 1)
+		r = atomic_add_return_release(1, n);
+}
+
+P2(atomic_t *p, atomic_t *n)
+{
+	int r0;
+	int r1;
+
+	r0 = atomic_read_acquire(n);
+	r1 = atomic_read(p);
+}
+
+exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
diff --git a/tools/testing/hpcc/litmus/limit-last-checker-nomb.litmus b/tools/testing/hpcc/litmus/limit-last-checker-nomb.litmus
new file mode 100644
index 000000000000..2690fdf6e868
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-last-checker-nomb.litmus
@@ -0,0 +1,28 @@
+C limit-last-checker-nomb
+
+(*
+ * Result: Sometimes
+ *
+ * Like limit-last-checker, without the full barrier. Both checks can
+ * miss the other addition, and both pass.
+ *)
+
+{}
+
+P0(int *a, int *b)
+{
+	int r0;
+
+	WRITE_ONCE(*a, 1);
+	r0 = READ_ONCE(*b);
+}
+
+P1(int *a, int *b)
+{
+	int r0;
+
+	WRITE_ONCE(*b, 1);
+	r0 = READ_ONCE(*a);
+}
+
+exists (0:r0=0 /\ 1:r0=0)
diff --git a/tools/testing/hpcc/litmus/limit-last-checker.litmus b/tools/testing/hpcc/litmus/limit-last-checker.litmus
new file mode 100644
index 000000000000..891f20ec86a0
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-last-checker.litmus
@@ -0,0 +1,33 @@
+C limit-last-checker
+
+(*
+ * Result: Never
+ *
+ * Two CPUs add to their level 0 counters a and b, then check with a
+ * precise sum, which reads the other counter. With a full barrier
+ * between the addition and the check, at least one of them sees the
+ * other addition. Of the additions which pass their check, the one
+ * checked last thus sees all of them.
+ *)
+
+{}
+
+P0(int *a, int *b)
+{
+	int r0;
+
+	WRITE_ONCE(*a, 1);
+	smp_mb();
+	r0 = READ_ONCE(*b);
+}
+
+P1(int *a, int *b)
+{
+	int r0;
+
+	WRITE_ONCE(*b, 1);
+	smp_mb();
+	r0 = READ_ONCE(*a);
+}
+
+exists (0:r0=0 /\ 1:r0=0)
diff --git a/tools/testing/hpcc/litmus/limit-undo-level0.litmus b/tools/testing/hpcc/litmus/limit-undo-level0.litmus
new file mode 100644
index 000000000000..1bda7b3835de
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-undo-level0.litmus
@@ -0,0 +1,35 @@
+C limit-undo-level0
+
+(*
+ * Result: Never
+ *
+ * An addition which does not fit is undone on the same CPU. Both stay
+ * in the level 0 counters, l0p for the additions and l0n for the
+ * subtractions. The full barrier of percpu_counter_tree_limit_add()
+ * comes between them. The precise sum of the limit counter reads l0n,
+ * then l0p after a read barrier. It never sees the subtraction without
+ * the addition.
+ *)
+
+{}
+
+P0(int *l0p, int *l0n)
+{
+	int r;
+
+	WRITE_ONCE(*l0p, 1);
+	smp_mb();
+	r = cmpxchg_relaxed(l0n, 0, 1);
+}
+
+P1(int *l0p, int *l0n)
+{
+	int r0;
+	int r1;
+
+	r0 = READ_ONCE(*l0n);
+	smp_rmb();
+	r1 = READ_ONCE(*l0p);
+}
+
+exists (0:r=0 /\ 1:r0=1 /\ 1:r1=0)
diff --git a/tools/testing/hpcc/litmus/limit-undo-root-rmb.litmus b/tools/testing/hpcc/litmus/limit-undo-root-rmb.litmus
new file mode 100644
index 000000000000..3b43afbeb8e9
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-undo-root-rmb.litmus
@@ -0,0 +1,30 @@
+C limit-undo-root-rmb
+
+(*
+ * Result: Never
+ *
+ * Like limit-undo-root, with a read barrier between the two reads
+ * instead of the acquire.
+ *)
+
+{}
+
+P0(atomic_t *p, atomic_t *n)
+{
+	int r;
+
+	r = atomic_add_return(1, p);
+	r = atomic_add_return_release(1, n);
+}
+
+P1(atomic_t *p, atomic_t *n)
+{
+	int r0;
+	int r1;
+
+	r0 = atomic_read(n);
+	smp_rmb();
+	r1 = atomic_read(p);
+}
+
+exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/testing/hpcc/litmus/limit-undo-root-unordered.litmus b/tools/testing/hpcc/litmus/limit-undo-root-unordered.litmus
new file mode 100644
index 000000000000..65bc0f2900b2
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-undo-root-unordered.litmus
@@ -0,0 +1,29 @@
+C limit-undo-root-unordered
+
+(*
+ * Result: Sometimes
+ *
+ * Like limit-undo-root, without ordering between the two reads. The
+ * check can then see the subtraction without the addition.
+ *)
+
+{}
+
+P0(atomic_t *p, atomic_t *n)
+{
+	int r;
+
+	r = atomic_add_return(1, p);
+	r = atomic_add_return_release(1, n);
+}
+
+P1(atomic_t *p, atomic_t *n)
+{
+	int r0;
+	int r1;
+
+	r0 = atomic_read(n);
+	r1 = atomic_read(p);
+}
+
+exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/testing/hpcc/litmus/limit-undo-root.litmus b/tools/testing/hpcc/litmus/limit-undo-root.litmus
new file mode 100644
index 000000000000..72335ee2ee6c
--- /dev/null
+++ b/tools/testing/hpcc/litmus/limit-undo-root.litmus
@@ -0,0 +1,32 @@
+C limit-undo-root
+
+(*
+ * Result: Never
+ *
+ * An addition which does not fit is undone on the same CPU. Its carry
+ * reaches the root of the additions p. Then the undo reaches the root of
+ * the subtractions n, with a release. The check reads n with an acquire,
+ * then p. It never sees the subtraction without the addition, which
+ * would take the difference below the value.
+ *)
+
+{}
+
+P0(atomic_t *p, atomic_t *n)
+{
+	int r;
+
+	r = atomic_add_return(1, p);
+	r = atomic_add_return_release(1, n);
+}
+
+P1(atomic_t *p, atomic_t *n)
+{
+	int r0;
+	int r1;
+
+	r0 = atomic_read_acquire(n);
+	r1 = atomic_read(p);
+}
+
+exists (1:r0=1 /\ 1:r1=0)
diff --git a/tools/testing/hpcc/litmus/publish-approximate-sum.litmus b/tools/testing/hpcc/litmus/publish-approximate-sum.litmus
new file mode 100644
index 000000000000..be4396a96ebc
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-approximate-sum.litmus
@@ -0,0 +1,40 @@
+C publish-approximate-sum
+
+(*
+ * Result: Never
+ *
+ * percpu_counter_tree_activate_many() zeroes the per-CPU counter l0mem
+ * and the root rootmem, which held stale values, then publishes approx_sum
+ * and level0 with releases. See "Publication of the tree" in
+ * lib/percpu_counter_tree.c.
+ *
+ * The approximate sum reads approx_sum, then the root through it. The
+ * address dependency orders the two reads. It never sees the stale
+ * root.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	smp_store_release(approx_sum, rootmem);
+	smp_store_release(level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int r1;
+
+	r0 = READ_ONCE(*approx_sum);
+	r1 = READ_ONCE(*r0);
+}
+
+exists (1:r0=rootmem /\ 1:r1=1)
diff --git a/tools/testing/hpcc/litmus/publish-carry-normb.litmus b/tools/testing/hpcc/litmus/publish-carry-normb.litmus
new file mode 100644
index 000000000000..bc5fa4a6aaad
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-carry-normb.litmus
@@ -0,0 +1,36 @@
+C publish-carry-normb
+
+(*
+ * Result: Sometimes
+ *
+ * Like publish-carry, without the read barrier. The carry slow path can
+ * then see approx_sum unpublished.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	smp_store_release(approx_sum, rootmem);
+	smp_store_release(level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int *r1;
+	int r2;
+
+	r0 = READ_ONCE(*level0);
+	r1 = READ_ONCE(*approx_sum);
+	r2 = READ_ONCE(*r1);
+}
+
+exists (1:r0=l0mem /\ (1:r1=noroot \/ 1:r2=1))
diff --git a/tools/testing/hpcc/litmus/publish-carry.litmus b/tools/testing/hpcc/litmus/publish-carry.litmus
new file mode 100644
index 000000000000..b316ade6d647
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-carry.litmus
@@ -0,0 +1,43 @@
+C publish-carry
+
+(*
+ * Result: Never
+ *
+ * percpu_counter_tree_activate_many() zeroes the per-CPU counter l0mem
+ * and the root rootmem, which held stale values, then publishes approx_sum
+ * and level0 with releases. See "Publication of the tree" in
+ * lib/percpu_counter_tree.c.
+ *
+ * The carry slow path has read level0. Then it reads approx_sum after a
+ * read barrier, and the root through it. It never sees approx_sum
+ * unpublished or the stale root.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	smp_store_release(approx_sum, rootmem);
+	smp_store_release(level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int *r1;
+	int r2;
+
+	r0 = READ_ONCE(*level0);
+	smp_rmb();
+	r1 = READ_ONCE(*approx_sum);
+	r2 = READ_ONCE(*r1);
+}
+
+exists (1:r0=l0mem /\ (1:r1=noroot \/ 1:r2=1))
diff --git a/tools/testing/hpcc/litmus/publish-precise-sum-noacquire.litmus b/tools/testing/hpcc/litmus/publish-precise-sum-noacquire.litmus
new file mode 100644
index 000000000000..b3fcfad22a61
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-precise-sum-noacquire.litmus
@@ -0,0 +1,38 @@
+C publish-precise-sum-noacquire
+
+(*
+ * Result: Sometimes
+ *
+ * Like publish-precise-sum, with a plain read of level0. The precise sum
+ * can then see approx_sum unpublished.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	smp_store_release(approx_sum, rootmem);
+	smp_store_release(level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int *r1;
+	int r2;
+	int r3;
+
+	r0 = READ_ONCE(*level0);
+	r1 = READ_ONCE(*approx_sum);
+	r2 = READ_ONCE(*r1);
+	r3 = READ_ONCE(*r0);
+}
+
+exists (1:r0=l0mem /\ (1:r1=noroot \/ 1:r2=1 \/ 1:r3=1))
diff --git a/tools/testing/hpcc/litmus/publish-precise-sum.litmus b/tools/testing/hpcc/litmus/publish-precise-sum.litmus
new file mode 100644
index 000000000000..0649b75b0bdc
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-precise-sum.litmus
@@ -0,0 +1,44 @@
+C publish-precise-sum
+
+(*
+ * Result: Never
+ *
+ * percpu_counter_tree_activate_many() zeroes the per-CPU counter l0mem
+ * and the root rootmem, which held stale values, then publishes approx_sum
+ * and level0 with releases. See "Publication of the tree" in
+ * lib/percpu_counter_tree.c.
+ *
+ * The precise sum reads level0 with an acquire, then approx_sum, the
+ * root and the per-CPU counter. It never sees approx_sum unpublished or
+ * a stale value.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	smp_store_release(approx_sum, rootmem);
+	smp_store_release(level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int *r1;
+	int r2;
+	int r3;
+
+	r0 = smp_load_acquire(level0);
+	r1 = READ_ONCE(*approx_sum);
+	r2 = READ_ONCE(*r1);
+	r3 = READ_ONCE(*r0);
+}
+
+exists (1:r0=l0mem /\ (1:r1=noroot \/ 1:r2=1 \/ 1:r3=1))
diff --git a/tools/testing/hpcc/litmus/publish-update-norelease.litmus b/tools/testing/hpcc/litmus/publish-update-norelease.litmus
new file mode 100644
index 000000000000..44a3d387b760
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-update-norelease.litmus
@@ -0,0 +1,34 @@
+C publish-update-norelease
+
+(*
+ * Result: Sometimes
+ *
+ * Like publish-update, with plain stores instead of the releases. The
+ * update fast path can then see the stale per-CPU counter.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	WRITE_ONCE(*approx_sum, rootmem);
+	WRITE_ONCE(*level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int r1;
+
+	r0 = READ_ONCE(*level0);
+	r1 = READ_ONCE(*r0);
+}
+
+exists (1:r0=l0mem /\ 1:r1=1)
diff --git a/tools/testing/hpcc/litmus/publish-update.litmus b/tools/testing/hpcc/litmus/publish-update.litmus
new file mode 100644
index 000000000000..55603a274b28
--- /dev/null
+++ b/tools/testing/hpcc/litmus/publish-update.litmus
@@ -0,0 +1,40 @@
+C publish-update
+
+(*
+ * Result: Never
+ *
+ * percpu_counter_tree_activate_many() zeroes the per-CPU counter l0mem
+ * and the root rootmem, which held stale values, then publishes approx_sum
+ * and level0 with releases. See "Publication of the tree" in
+ * lib/percpu_counter_tree.c.
+ *
+ * The update fast path reads level0, then its per-CPU counter through
+ * it. The address dependency orders the two reads. It never sees the
+ * stale per-CPU counter.
+ *)
+
+{
+	level0=nolevel0;
+	approx_sum=noroot;
+	l0mem=1;
+	rootmem=1;
+}
+
+P0(int **level0, int **approx_sum, int *l0mem, int *rootmem)
+{
+	WRITE_ONCE(*l0mem, 0);
+	WRITE_ONCE(*rootmem, 0);
+	smp_store_release(approx_sum, rootmem);
+	smp_store_release(level0, l0mem);
+}
+
+P1(int **level0, int **approx_sum)
+{
+	int *r0;
+	int r1;
+
+	r0 = READ_ONCE(*level0);
+	r1 = READ_ONCE(*r0);
+}
+
+exists (1:r0=l0mem /\ 1:r1=1)
-- 
2.47.3