[RFC/WIP PATCH 4/4] Documentation/litmus-tests: add hazptr acquire-before-scan test

[Kunwu Chan <kunwu.chan@gmail.com>]

Add an LKMM test for the hazard-pointer publication protocol used
by the lockdep conversion.

The test checks that the reclaimer cannot miss a reader hazard
pointer publication while the reader still observes the
pre-unpublish pointer.  The smp_mb() pair provides the required
ordering.

Models the resolved-publication case; the in-flight wildcard window
is covered by the two-phase wildcard scan of the v3 implementation.

Verified with herd7: Never 0 6.

Signed-off-by: Kunwu Chan <kunwu.chan@gmail.com>
---
 .../hazptr/hazptr-acquire-before-scan.litmus  | 49 +++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus

diff --git a/Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus b/Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus
new file mode 100644
index 000000000000..19df97f1c3b2
--- /dev/null
+++ b/Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus
@@ -0,0 +1,49 @@
+C hazptr-acquire-before-scan
+
+(*
+ * Result: Never
+ *
+ * The reclaimer unpublishes the pointer, executes smp_mb(), then
+ * scans the hazard-pointer slot.  The reader publishes the
+ * protected address, executes smp_mb(), then loads the pointer.
+ *
+ * The smp_mb() pair forbids the reclaimer from missing the
+ * publication while the reader still observes the pre-unpublish
+ * pointer.
+ *
+ * This is the publication protocol used by the lockdep
+ * is_dynamic_key()/lockdep_unregister_key() conversion.
+ *
+ * Models the resolved-publication case; the in-flight wildcard
+ * window is covered by the two-phase wildcard scan of the v3
+ * implementation.
+ *)
+
+{
+int ptr = 1;	(* 1: points to the object, 0: unpublished. *)
+int hp = 0;	(* Hazard-pointer slot: 0: empty, 1: holds the addr. *)
+int data = 1;	(* Object payload; 0: reclaimed. *)
+}
+
+P0(int *ptr, int *hp, int *data)
+{
+	int r0;
+
+	WRITE_ONCE(*ptr, 0);	/* Store A: unpublish. */
+	smp_mb();
+	r0 = READ_ONCE(*hp);	/* Load B: scan. */
+	WRITE_ONCE(*data, 0);	/* Reclaim. */
+}
+
+P1(int *ptr, int *hp, int *data)
+{
+	int r0;
+	int r1;
+
+	WRITE_ONCE(*hp, 1);	/* Store B: publish. */
+	smp_mb();
+	r0 = READ_ONCE(*ptr);	/* Load A: load pointer. */
+	r1 = READ_ONCE(*data);	/* Access object. */
+}
+
+exists (0:r0=0 /\ 1:r0=1)
-- 
2.43.0