feat(runtime-include): support std::atomic_ref in C++ programs

CHANGELOG.md

@@ -9,6 +9,21 @@ released.
 
 - Merge of MIXER [POPL'25] into mainline GenMC
 
+### Added
+
+- Support for `std::atomic_ref`
+- Support for `std::atomic_flag::test`
+- Support for `wait`/`notify_one`/`notify_all` on `std::atomic`,
+  `std::atomic_flag` and `std::atomic_ref`
+
+### Fixes
+
+- The bundled `<atomic>` no longer exposes only its C++11 subset when compiling
+  with `-std=c++17` or later, which also restores
+  `std::atomic<T>::is_always_lock_free`
+- The bundled C++ headers (`atomic`, `thread`, ...) are now installed; only the
+  `.h` ones were
+
 
 ## [0.18.0] - 2026.09.02
 

CMakeLists.txt

@@ -27,7 +27,9 @@ add_library(genmc_config_includes INTERFACE)
 target_compile_features(genmc_config_includes INTERFACE cxx_std_23)
 target_include_directories(genmc_config_includes INTERFACE ${CMAKE_BINARY_DIR}/include)
 
-install(DIRECTORY lli/runtime-include/c/ DESTINATION "${PKG_INCLUDE_DIR}" FILES_MATCHING PATTERN "*.h")
+# Every file here is a header, and the C++ ones (atomic, thread, cassert, ...)
+# carry no extension, so matching on one would leave them behind.
+install(DIRECTORY lli/runtime-include/c/ DESTINATION "${PKG_INCLUDE_DIR}")
 
 ### Whether to build lli-based binary
 option(BUILD_LLI "Build lli-based executable (requires LLVM)" ON)

tests/correct/infr/cpp-atomic-flag-test/args.rc11.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-flag-test/args.rc11.wb.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-flag-test/args.sc.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-flag-test/expected.rc11.mo.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-flag-test/expected.rc11.wb.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-flag-test/expected.sc.mo.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-flag-test/variants/cpp-atomic-flag-test.cpp

@@ -0,0 +1,45 @@
+#include <pthread.h>
+#include <atomic>
+#include <cassert>
+
+/* atomic_flag::test observes the flag without setting it, so the setter's
+ * release must be what makes `data` visible. */
+std::atomic_flag f = ATOMIC_FLAG_INIT;
+int data = 0;
+
+void t0()
+{
+	data = 42;
+	f.test_and_set(std::memory_order_release);
+}
+
+void t1()
+{
+	if (f.test(std::memory_order_acquire))
+		assert(data == 42);
+}
+
+int main()
+{
+	pthread_t threads[2];
+
+	assert(!f.test());
+
+	pthread_create(
+		&threads[0],
+		nullptr,
+		[](void *) -> void * {t0(); return nullptr;},
+		nullptr);
+	pthread_create(
+		&threads[1],
+		nullptr,
+		[](void *) -> void * {t1(); return nullptr;},
+		nullptr);
+	for (auto i = 0; i < 2; ++i) {
+		pthread_join(threads[i], nullptr);
+	}
+
+	assert(std::atomic_flag_test(&f));
+
+	return 0;
+}

tests/correct/infr/cpp-atomic-ref-mp/args.rc11.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-mp/args.rc11.wb.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-mp/args.sc.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.mo.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.wb.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-ref-mp/expected.sc.mo.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-ref-mp/variants/cpp-atomic-ref-mp.cpp

@@ -0,0 +1,47 @@
+#include <pthread.h>
+#include <atomic>
+#include <cassert>
+#include <cstdint>
+
+/* `data` and `flag` stay plain objects with the layout of their own types;
+ * only the accesses through atomic_ref are atomic. The release/acquire pair
+ * on `flag` must order the plain accesses to `data`. */
+std::uint32_t data = 0;
+std::uint32_t flag = 0;
+
+void t0()
+{
+	std::atomic_ref<std::uint32_t> f{flag};
+
+	data = 42;
+	f.store(1, std::memory_order_release);
+}
+
+void t1()
+{
+	std::atomic_ref<std::uint32_t> f{flag};
+
+	if (f.load(std::memory_order_acquire) == 1)
+		assert(data == 42);
+}
+
+int main()
+{
+	pthread_t threads[2];
+
+	pthread_create(
+		&threads[0],
+		nullptr,
+		[](void *) -> void * {t0(); return nullptr;},
+		nullptr);
+	pthread_create(
+		&threads[1],
+		nullptr,
+		[](void *) -> void * {t1(); return nullptr;},
+		nullptr);
+	for (auto i = 0; i < 2; ++i) {
+		pthread_join(threads[i], nullptr);
+	}
+
+	return 0;
+}

tests/correct/infr/cpp-atomic-ref-repr/args.rc11.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-repr/args.rc11.wb.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-repr/args.sc.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.mo.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.wb.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-repr/expected.sc.mo.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-repr/variants/cpp-atomic-ref-repr.cpp

@@ -0,0 +1,55 @@
+#include <atomic>
+#include <cassert>
+#include <cstddef>
+#include <cstdint>
+
+/* A type whose size is a power of two must be naturally aligned to be operated
+ * on atomically, however weak its own alignment requirement is. */
+struct Unaligned {
+	char b[8];
+};
+
+/* char followed by int leaves padding bits, which a compare-exchange has to
+ * ignore. */
+struct Padded {
+	char c;
+	int i;
+};
+
+static_assert(alignof(Unaligned) < 8, "expected a weakly aligned type");
+static_assert(std::atomic_ref<Unaligned>::required_alignment == 8, "");
+static_assert(std::atomic_ref<std::uint32_t>::required_alignment == 4, "");
+static_assert(alignof(Padded) == 4 && sizeof(Padded) == 8, "expected padding and weak alignment");
+static_assert(std::atomic_ref<Padded>::required_alignment == 8, "");
+
+/* Padded asks for more alignment than the type itself declares, so say so
+ * rather than relying on where the linker happens to put it. */
+alignas(std::atomic_ref<Padded>::required_alignment) Padded obj = {1, 2};
+
+int main()
+{
+	std::atomic_ref<Padded> r{obj};
+	Padded expected;
+	unsigned char *bytes = reinterpret_cast<unsigned char *>(&expected);
+
+	r.store(Padded{3, 4});
+
+	/* Give `expected` padding that differs from the object's. */
+	for (unsigned k = 0; k < sizeof(Padded); ++k)
+		bytes[k] = 0xFF;
+	expected.c = 3;
+	expected.i = 4;
+
+	assert(r.compare_exchange_strong(expected, Padded{5, 6}));
+
+	Padded got = r.load();
+	assert(got.c == 5 && got.i == 6);
+
+	/* On failure the caller's expected takes the value that was read. */
+	expected.c = 0;
+	expected.i = 0;
+	assert(!r.compare_exchange_strong(expected, Padded{7, 8}));
+	assert(expected.c == 5 && expected.i == 6);
+
+	return 0;
+}

tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.wb.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-rmw/args.sc.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.mo.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.wb.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-ref-rmw/expected.sc.mo.in

@@ -0,0 +1 @@
+2

tests/correct/infr/cpp-atomic-ref-rmw/variants/cpp-atomic-ref-rmw.cpp

@@ -0,0 +1,36 @@
+#include <pthread.h>
+#include <atomic>
+#include <cassert>
+#include <cstdint>
+
+/* Read-modify-write through atomic_ref on a plain object: both increments
+ * must be observed, whichever order they land in. */
+std::uint32_t counter = 0;
+
+void incr()
+{
+	std::atomic_ref<std::uint32_t> c{counter};
+
+	c.fetch_add(1, std::memory_order_relaxed);
+}
+
+int main()
+{
+	pthread_t threads[2];
+
+	for (auto i = 0; i < 2; ++i) {
+		pthread_create(
+			&threads[i],
+			nullptr,
+			[](void *) -> void * {incr(); return nullptr;},
+			nullptr);
+	}
+	for (auto i = 0; i < 2; ++i) {
+		pthread_join(threads[i], nullptr);
+	}
+
+	std::atomic_ref<std::uint32_t> c{counter};
+	assert(c.load(std::memory_order_relaxed) == 2);
+
+	return 0;
+}

tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.wb.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-wait-repr/args.sc.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.mo.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.wb.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-wait-repr/expected.sc.mo.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-wait-repr/variants/cpp-atomic-ref-wait-repr.cpp

@@ -0,0 +1,21 @@
+#include <atomic>
+#include <cassert>
+
+/* wait() compares value representations, which for floating point is not what
+ * operator== would say. 0.0 and -0.0 compare equal but are represented
+ * differently, so a wait on 0.0 over a -0.0 referent has nothing to wait for
+ * and must return. */
+double negzero = -0.0;
+int reached = 0;
+
+int main()
+{
+	std::atomic_ref<double> r{negzero};
+
+	r.wait(0.0, std::memory_order_relaxed);
+	reached = 1;
+
+	assert(reached == 1);
+	assert(r.load(std::memory_order_relaxed) == 0.0); /* still -0.0 */
+	return 0;
+}

tests/correct/infr/cpp-atomic-ref-wait/args.rc11.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-wait/args.rc11.wb.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-wait/args.sc.mo.in

@@ -0,0 +1 @@
+ | -std=c++20

tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.mo.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.wb.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-wait/expected.sc.mo.in

@@ -0,0 +1 @@
+1

tests/correct/infr/cpp-atomic-ref-wait/variants/cpp-atomic-ref-wait.cpp

@@ -0,0 +1,48 @@
+#include <pthread.h>
+#include <atomic>
+#include <cassert>
+#include <cstdint>
+
+/* wait() must not return until `flag` moves off the awaited value, and the
+ * acquire ordering it is given must make the released `data` visible.
+ * notify_one() is a no-op under the polling implementation. */
+std::uint32_t data = 0;
+std::uint32_t flag = 0;
+
+void t0()
+{
+	std::atomic_ref<std::uint32_t> f{flag};
+
+	data = 42;
+	f.store(1, std::memory_order_release);
+	f.notify_one();
+}
+
+void t1()
+{
+	std::atomic_ref<std::uint32_t> f{flag};
+
+	f.wait(0, std::memory_order_acquire);
+	assert(data == 42);
+}
+
+int main()
+{
+	pthread_t threads[2];
+
+	pthread_create(
+		&threads[0],
+		nullptr,
+		[](void *) -> void * {t0(); return nullptr;},
+		nullptr);
+	pthread_create(
+		&threads[1],
+		nullptr,
+		[](void *) -> void * {t1(); return nullptr;},
+		nullptr);
+	for (auto i = 0; i < 2; ++i) {
+		pthread_join(threads[i], nullptr);
+	}
+
+	return 0;
+}

tests/wrong/racy/cpp-atomic-ref-mp-rlx/args.rc11.wb.in

@@ -0,0 +1 @@
+-std=c++20