Re: [RFC] tools/memory-model: Rule out OOTA

On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote:
> The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following
> example shared on this list a few years ago:

Apologies for being slow, but I have finally added the litmus tests in
this email thread to the https://github.com/paulmckrcu/litmus repo.

It is quite likely that I have incorrectly intuited the missing portions
of the litmus tests, especially the two called out in the commit log
below.  If you have time, please do double-check.

And the updated (and condensed!) version of the C++ OOTA paper may be
found here, this time with a proposed change to the standard:

https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2025/p3692r1.pdf

							Thanx, Paul

------------------------------------------------------------------------

commit fd17e8fceb75326e159ba3aa6fdb344f74f5c7a5
Author: Paul E. McKenney <[email protected]>
Date:   Tue Jul 22 17:21:19 2025 -0700

    manual/oota:  Add Jonas and Alan OOTA examples
    
    Each of these new litmus tests contains the URL of the email message
    that I took it from.
    
    Please note that I had to tweak the example leading up to
    C-JO-OOTA-4.litmus, and I might well have misinterpreted Jonas's "~"
    operator.
    
    Also, C-JO-OOTA-7.litmus includes a "*r2 = a" statement that makes herd7
    very unhappy.  On the other hand, initializing registers to the address
    of a variable is straight forward, as shown in the resulting litmus test.
    
    Signed-off-by: Paul E. McKenney <[email protected]>

diff --git a/manual/oota/C-AS-OOTA-1.litmus b/manual/oota/C-AS-OOTA-1.litmus
new file mode 100644
index 00000000..81a873a7
--- /dev/null
+++ b/manual/oota/C-AS-OOTA-1.litmus
@@ -0,0 +1,40 @@
+C C-AS-OOTA-1
+
+(*
+ * Result: Sometimes
+ *
+ * Because smp_rmb() combined with smp_wmb() does not order earlier
+ * reads against later writes.
+ *
+ * https://lore.kernel.org/all/[email protected]
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		*a = *b;
+	}
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		*b = *a;
+	}
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r1=1)
diff --git a/manual/oota/C-AS-OOTA-2.litmus b/manual/oota/C-AS-OOTA-2.litmus
new file mode 100644
index 00000000..c672b0e7
--- /dev/null
+++ b/manual/oota/C-AS-OOTA-2.litmus
@@ -0,0 +1,33 @@
+C C-AS-OOTA-2
+
+(*
+ * Result: Always
+ *
+ * If we were using C-language relaxed atomics instead of volatiles,
+ * the compiler *could* eliminate the first WRITE_ONCE() in each process,
+ * then also each process's local variable, thus having an undefined value
+ * for each of those local variables.  But this cannot happen given that
+ * we are using Linux-kernel _ONCE() primitives.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b)
+{
+	int r0 = READ_ONCE(*a);
+
+	WRITE_ONCE(*b, r0);
+	WRITE_ONCE(*b, 2);
+}
+
+P1(int *a, int *b)
+{
+	int r1 = READ_ONCE(*b);
+
+	WRITE_ONCE(*a, r0);
+	WRITE_ONCE(*a, 2);
+}
+
+exists ((0:r0=0 \/ 0:r0=2) /\ (1:r1=0 \/ 1:r1=2))
diff --git a/manual/oota/C-JO-OOTA-1.litmus b/manual/oota/C-JO-OOTA-1.litmus
new file mode 100644
index 00000000..6ab437b4
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-1.litmus
@@ -0,0 +1,40 @@
+C C-JO-OOTA-1
+
+(*
+ * Result: Never
+ *
+ * But Sometimes in LKMM as of early 2025, given that 42 is a possible
+ * value for things like S19..
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		*a = *b;
+	}
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		*b = *a;
+	}
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+exists (b=42)
diff --git a/manual/oota/C-JO-OOTA-2.litmus b/manual/oota/C-JO-OOTA-2.litmus
new file mode 100644
index 00000000..ad708c60
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-2.litmus
@@ -0,0 +1,44 @@
+C C-JO-OOTA-2
+
+(*
+ * Result: Never
+ *
+ * But Sometimes in LKMM as of early 2025, given that 42 is a possible
+ * value for things like S23.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2 = 0;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = *b;
+	}
+	WRITE_ONCE(*a, r2);
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2 = 0;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = *a;
+	}
+	WRITE_ONCE(*b, r2);
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+exists (b=42)
diff --git a/manual/oota/C-JO-OOTA-3.litmus b/manual/oota/C-JO-OOTA-3.litmus
new file mode 100644
index 00000000..633b8334
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-3.litmus
@@ -0,0 +1,46 @@
+C C-JO-OOTA-3
+
+(*
+ * Result: Never
+ *
+ * But LKMM finds the all-ones result, perhaps due to not tracking
+ * control dependencies out of the "if" statement.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	r2 = READ_ONCE(*b);
+	if (r1 == 1) {
+		r2 = *b;
+	}
+	WRITE_ONCE(*a, r2);
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	r2 = READ_ONCE(*a);
+	if (r1 == 1) {
+		r2 = *a;
+	}
+	WRITE_ONCE(*b, r2);
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r1=1)
diff --git a/manual/oota/C-JO-OOTA-4.litmus b/manual/oota/C-JO-OOTA-4.litmus
new file mode 100644
index 00000000..cab7ebb6
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-4.litmus
@@ -0,0 +1,43 @@
+C C-JO-OOTA-4
+
+(*
+ * Result: Never
+ *
+ * And LKMM agrees, which might be a surprise.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+	int r3;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	r2 = *b;
+	r3 = r1 == 0;
+	WRITE_ONCE(*a, (r3 + 1) & r2);
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+	int r3;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	r2 = *a;
+	r3 = r1 == 0;
+	WRITE_ONCE(*b, (r3 + 1) & r2);
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r1=1)
diff --git a/manual/oota/C-JO-OOTA-5.litmus b/manual/oota/C-JO-OOTA-5.litmus
new file mode 100644
index 00000000..145c8378
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-5.litmus
@@ -0,0 +1,44 @@
+C C-JO-OOTA-5
+
+(*
+ * Result: Never
+ *
+ * But LKMM finds the all-ones result, perhaps due r2 being unused.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = READ_ONCE(*a);
+	}
+	*b = 1;
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = READ_ONCE(*b);
+	}
+	*a = 1;
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+locations [0:r2;1:r2]
+exists (0:r1=1 /\ 1:r1=1)
diff --git a/manual/oota/C-JO-OOTA-6.litmus b/manual/oota/C-JO-OOTA-6.litmus
new file mode 100644
index 00000000..942e6c82
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-6.litmus
@@ -0,0 +1,44 @@
+C C-JO-OOTA-6
+
+(*
+ * Result: Never
+ *
+ * But LKMM finds the all-ones result, due to OOTA on r2.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = READ_ONCE(*a);
+	}
+	*b = r2;
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = READ_ONCE(*b);
+	}
+	*a = r2;
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+locations [0:r2;1:r2]
+exists (0:r1=1 /\ 1:r1=1)
diff --git a/manual/oota/C-JO-OOTA-7.litmus b/manual/oota/C-JO-OOTA-7.litmus
new file mode 100644
index 00000000..31c0b8ae
--- /dev/null
+++ b/manual/oota/C-JO-OOTA-7.litmus
@@ -0,0 +1,47 @@
+C C-JO-OOTA-7
+
+(*
+ * Result: Never
+ *
+ * But LKMM finds the all-ones result, due to OOTA on r2.
+ *
+ * https://lore.kernel.org/all/[email protected]/
+ *)
+
+{
+	0:r2=a;
+	1:r2=b;
+}
+
+P0(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = READ_ONCE(*a);
+	}
+	*r2 = a;
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		r2 = READ_ONCE(*b);
+	}
+	*r2 = b;
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+locations [0:r2;1:r2]
+exists (0:r1=1 /\ 1:r1=1)
diff --git a/manual/oota/C-PM-OOTA-1.litmus b/manual/oota/C-PM-OOTA-1.litmus
new file mode 100644
index 00000000..e771e3c9
--- /dev/null
+++ b/manual/oota/C-PM-OOTA-1.litmus
@@ -0,0 +1,37 @@
+C C-PM-OOTA-1
+
+(*
+ * Result: Never
+ *
+ * LKMM agrees.
+ *
+ * https://lore.kernel.org/all/9a0dccbb-bfa7-4b33-ac1a-daa9841b609a@paulmck-laptop/
+ *)
+
+{}
+
+P0(int *a, int *b, int *x, int *y) {
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_rmb();
+	if (r1 == 1) {
+		WRITE_ONCE(*a, *b);
+	}
+	smp_wmb();
+	WRITE_ONCE(*y, 1);
+}
+
+P1(int *a, int *b, int *x, int *y) {
+	int r1;
+
+	r1 = READ_ONCE(*y);
+	smp_rmb();
+	if (r1 == 1) {
+		WRITE_ONCE(*b, *a);
+	}
+	smp_wmb();
+	WRITE_ONCE(*x, 1);
+}
+
+exists b=42