From 2937c004646103b0bd57a6a94d7dacca070cfcd4 Mon Sep 17 00:00:00 2001
From: lukeg101 <6547672+lukeg101@users.noreply.github.com>
Date: Fri, 12 Jun 2026 04:41:04 -0700
Subject: [PATCH] cpp2w: exclude NORETURN from tecotsb target endpoint

Models the non-returning atomic reduction atomic_store_add_explicit from
P3111R0 (Atomic Reduction Operations):
https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3111r0.html

A non-returning RMW (tagged NORETURN) should not anchor the tecotsb
ordering edge the way a value-returning RMW does. Excluding NORETURN from the
target [A] endpoint lets a release store_add not establish message-passing
synchronization, so the stale-read outcome {r0=0, y=2} becomes observable.

Adds tests/mp/mp-store-add.litmus and mp-fetch-add.litmus: under the
patched cpp2w, store_add -> 4 states (incl. {r0=0,y=2}); fetch_add -> 3 states
(forbids it).

The other models (cpp11, cpp17, rc11, rc17) already support store_add
(same 4-state weak behaviour); they have no tecotsb relation, so a non-returning
RMW never over-synchronizes there. cpp2w was the sole outlier.

herd7 does not support store_add (its CSem is a stub), so no
.litmus.expected can be generated; reproduced/validated with dartagnan (Dat3M
exploration_mode branch, commit b360545), see
https://github.com/hernanponcedeleon/Dat3M/issues/984.

Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 model/cpp2w.cat              |  2 +-
 tests/mp/mp-fetch-add.litmus | 16 ++++++++++++++++
 tests/mp/mp-store-add.litmus | 16 ++++++++++++++++
 3 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 tests/mp/mp-fetch-add.litmus
 create mode 100644 tests/mp/mp-store-add.litmus

diff --git a/model/cpp2w.cat b/model/cpp2w.cat
index e010e3a8..1fb23883 100644
--- a/model/cpp2w.cat
+++ b/model/cpp2w.cat
@@ -27,7 +27,7 @@ let pscb = ([SC] | [F & SC]; hb?); scb; ([SC] | hb? ; [F & SC])
 let pscf = [F & SC]; (hb | hb; eco; hb); [F & SC]
 let psc = pscb | pscf
 
-let tecotsb = ([A]; (eco); [A])+; sb
+let tecotsb = ([A]; (eco); [A \ NORETURN])+; sb
 
 let cnf = ((W * _) | (_ * W)) & loc \ ((IW * _) | (_ * IW))
 let dr = (cnf & ext) \ (hb | hb^-1 | A * A | tecotsb | tecotsb^-1)
diff --git a/tests/mp/mp-fetch-add.litmus b/tests/mp/mp-fetch-add.litmus
new file mode 100644
index 00000000..666193cc
--- /dev/null
+++ b/tests/mp/mp-fetch-add.litmus
@@ -0,0 +1,16 @@
+C mp-fetch-add
+{ [x] = 0; [y] = 0; }
+
+P0 (int* x, int* y) {
+  atomic_store_explicit(x, 1, memory_order_relaxed);
+  atomic_thread_fence(memory_order_release);
+  atomic_store_explicit(y, 1, memory_order_relaxed);
+}
+
+P1 (int* x, int* y) {
+  int r1 = atomic_fetch_add_explicit(y, 1, memory_order_release);
+  atomic_thread_fence(memory_order_acquire);
+  int r0 = atomic_load_explicit(x, memory_order_relaxed);
+}
+
+exists (1:r0=0 /\ y=2)
diff --git a/tests/mp/mp-store-add.litmus b/tests/mp/mp-store-add.litmus
new file mode 100644
index 00000000..64c6bad8
--- /dev/null
+++ b/tests/mp/mp-store-add.litmus
@@ -0,0 +1,16 @@
+C mp-store-add
+{ [x] = 0; [y] = 0; }
+
+P0 (int* x, int* y) {
+  atomic_store_explicit(x, 1, memory_order_relaxed);
+  atomic_thread_fence(memory_order_release);
+  atomic_store_explicit(y, 1, memory_order_relaxed);
+}
+
+P1 (int* x, int* y) {
+  atomic_store_add_explicit(y, 1, memory_order_release);
+  atomic_thread_fence(memory_order_acquire);
+  int r0 = atomic_load_explicit(x, memory_order_relaxed);
+}
+
+exists (1:r0=0 /\ y=2)