diff --git a/CHANGELOG.md b/CHANGELOG.md
index 93d729e3..4241574e 100644
--- a/CHANGELOG.md
+++ b/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
 
diff --git a/CMakeLists.txt b/CMakeLists.txt
index a96e2302..f0d24b0d 100644
--- a/CMakeLists.txt
+++ b/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)
diff --git a/lli/runtime-include/c/atomic b/lli/runtime-include/c/atomic
index 54c68056..c2d41694 100644
--- a/lli/runtime-include/c/atomic
+++ b/lli/runtime-include/c/atomic
@@ -587,10 +587,34 @@ void atomic_signal_fence(memory_order m) noexcept;
 // #error C++ standard library is incompatible with <stdatomic.h>
 // #endif
 
+// Upstream libc++ has its build system supply _LIBCPP_STD_VER; this bundled
+// copy is included directly by the compiler driver, so derive it here.
+// Without it every dialect check below reads as C++11 and the post-C++11
+// parts of the library silently disappear.
+#ifndef _LIBCPP_STD_VER
+# if __cplusplus <= 201103L
+#  define _LIBCPP_STD_VER 11
+# elif __cplusplus <= 201402L
+#  define _LIBCPP_STD_VER 14
+# elif __cplusplus <= 201703L
+#  define _LIBCPP_STD_VER 17
+# elif __cplusplus <= 202002L
+#  define _LIBCPP_STD_VER 20
+# else
+#  define _LIBCPP_STD_VER 23
+# endif
+#endif
+
 #if _LIBCPP_STD_VER > 14
 # define __cpp_lib_atomic_is_always_lock_free 201603L
 #endif
 
+#if _LIBCPP_STD_VER > 17
+# define __cpp_lib_atomic_ref 201806L
+# define __cpp_lib_atomic_flag_test 201907L
+# define __cpp_lib_atomic_wait 201907L
+#endif
+
 #define _LIBCPP_CHECK_STORE_MEMORY_ORDER(__m) \
   _LIBCPP_DIAGNOSE_WARNING(__m == memory_order_consume || \
                            __m == memory_order_acquire || \
@@ -615,6 +639,34 @@ typedef enum memory_order
     memory_order_release, memory_order_acq_rel, memory_order_seq_cst
 } memory_order;
 
+// Order translation is needed whenever the GCC-style builtins are used, which
+// atomic_ref does unconditionally, so it sits outside the guard below.
+namespace __gcc_atomic {
+
+static inline _LIBCPP_CONSTEXPR int __to_gcc_order(memory_order __order) {
+  // Avoid switch statement to make this a constexpr.
+  return __order == memory_order_relaxed ? __ATOMIC_RELAXED:
+         (__order == memory_order_acquire ? __ATOMIC_ACQUIRE:
+          (__order == memory_order_release ? __ATOMIC_RELEASE:
+           (__order == memory_order_seq_cst ? __ATOMIC_SEQ_CST:
+            (__order == memory_order_acq_rel ? __ATOMIC_ACQ_REL:
+              __ATOMIC_CONSUME))));
+}
+
+// A compare-exchange may not fail with a release order, so acq_rel and release
+// degrade to their load-only counterparts.
+static inline _LIBCPP_CONSTEXPR int __to_gcc_failure_order(memory_order __order) {
+  // Avoid switch statement to make this a constexpr.
+  return __order == memory_order_relaxed ? __ATOMIC_RELAXED:
+         (__order == memory_order_acquire ? __ATOMIC_ACQUIRE:
+          (__order == memory_order_release ? __ATOMIC_RELAXED:
+           (__order == memory_order_seq_cst ? __ATOMIC_SEQ_CST:
+            (__order == memory_order_acq_rel ? __ATOMIC_ACQUIRE:
+              __ATOMIC_CONSUME))));
+}
+
+} // namespace __gcc_atomic
+
 #if defined(_LIBCPP_HAS_GCC_ATOMIC_IMP)
 namespace __gcc_atomic {
 template <typename _Tp>
@@ -651,26 +703,6 @@ struct __can_assign {
       sizeof(__test_atomic_assignable<_Tp, _Td>(1)) == sizeof(char);
 };
 
-static inline _LIBCPP_CONSTEXPR int __to_gcc_order(memory_order __order) {
-  // Avoid switch statement to make this a constexpr.
-  return __order == memory_order_relaxed ? __ATOMIC_RELAXED:
-         (__order == memory_order_acquire ? __ATOMIC_ACQUIRE:
-          (__order == memory_order_release ? __ATOMIC_RELEASE:
-           (__order == memory_order_seq_cst ? __ATOMIC_SEQ_CST:
-            (__order == memory_order_acq_rel ? __ATOMIC_ACQ_REL:
-              __ATOMIC_CONSUME))));
-}
-
-static inline _LIBCPP_CONSTEXPR int __to_gcc_failure_order(memory_order __order) {
-  // Avoid switch statement to make this a constexpr.
-  return __order == memory_order_relaxed ? __ATOMIC_RELAXED:
-         (__order == memory_order_acquire ? __ATOMIC_ACQUIRE:
-          (__order == memory_order_release ? __ATOMIC_RELAXED:
-           (__order == memory_order_seq_cst ? __ATOMIC_SEQ_CST:
-            (__order == memory_order_acq_rel ? __ATOMIC_ACQUIRE:
-              __ATOMIC_CONSUME))));
-}
-
 } // namespace __gcc_atomic
 
 template <typename _Tp>
@@ -916,11 +948,61 @@ kill_dependency(_Tp __y) _NOEXCEPT
 # define ATOMIC_POINTER_LOCK_FREE   __GCC_ATOMIC_POINTER_LOCK_FREE
 #endif
 
+// Notes on wait()/notify_one()/notify_all(), defined below for atomic<T>,
+// atomic_flag and atomic_ref<T>.
+//
+// wait() polls instead of blocking, which GenMC's spin-assume transformation
+// turns into an assume: an execution whose awaited value never arrives is
+// pruned rather than reported as a deadlock. That in turn makes notify_one()
+// and notify_all() no-ops, since a waiter re-reads the object rather than
+// being woken. Polling is a conforming implementation because wait() is
+// permitted to return spuriously.
+//
+// Waiting compares value representations, which is what the standard asks for
+// and what floating point needs: 0.0 and -0.0 are one value held two ways, so
+// comparing values waits on a value that has already arrived, and the
+// spin-assume prunes that execution rather than failing it. Two identical NaNs
+// go the other way, one representation that compares unequal.
+//
+// The comparison has to stay a single one, because the transformation does not
+// recognise a loop nested inside the spin loop. Reinterpreting the
+// representation as an integer of the same width buys that; the widths without
+// such an integer are the ones no target holds atomically, and wait() is
+// unavailable for them. atomic_flag waits on a bool, which holds one value one
+// way, and compares it directly.
+template <size_t _Sz>
+struct __atomic_repr_type {};
+template <>
+struct __atomic_repr_type<1> { typedef uint8_t type; };
+template <>
+struct __atomic_repr_type<2> { typedef uint16_t type; };
+template <>
+struct __atomic_repr_type<4> { typedef uint32_t type; };
+template <>
+struct __atomic_repr_type<8> { typedef uint64_t type; };
+#ifdef __SIZEOF_INT128__
+template <>
+struct __atomic_repr_type<16> { typedef __uint128_t type; };
+#endif
+
+// Callers take the awaited value's representation once, above the loop: left
+// in the condition it folds to a cast of a constant, which an assume cannot
+// hold.
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+typename __atomic_repr_type<sizeof(_Tp)>::type __atomic_repr(const _Tp& __v) _NOEXCEPT
+{
+    typedef typename __atomic_repr_type<sizeof(_Tp)>::type _Ur;
+    return __builtin_bit_cast(_Ur, __v);
+}
+
 // general atomic<T>
 
 template <class _Tp, bool = is_integral<_Tp>::value && !is_same<_Tp, bool>::value>
 struct __atomic_base  // false
 {
+    typedef _Tp value_type;
+
     mutable _Atomic(_Tp) __a_;
 
 #if defined(__cpp_lib_atomic_is_always_lock_free)
@@ -1002,6 +1084,25 @@ struct __atomic_base  // false
                                  memory_order __m = memory_order_seq_cst) _NOEXCEPT
         {return __c11_atomic_compare_exchange_strong(&__a_, &__e, __d, __m, __m);}
 
+#if _LIBCPP_STD_VER > 17
+    _LIBCPP_INLINE_VISIBILITY
+    void wait(_Tp __v, memory_order __m = memory_order_seq_cst) const volatile _NOEXCEPT
+        {const typename __atomic_repr_type<sizeof(_Tp)>::type __want = __atomic_repr(__v);
+         while (__atomic_repr(load(__m)) == __want) ;}
+    _LIBCPP_INLINE_VISIBILITY
+    void wait(_Tp __v, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {const typename __atomic_repr_type<sizeof(_Tp)>::type __want = __atomic_repr(__v);
+         while (__atomic_repr(load(__m)) == __want) ;}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_one() volatile _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_one() _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_all() volatile _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_all() _NOEXCEPT {}
+#endif
+
     _LIBCPP_INLINE_VISIBILITY
 #ifndef _LIBCPP_CXX03_LANG
     __atomic_base() _NOEXCEPT = default;
@@ -1189,6 +1290,262 @@ struct atomic<_Tp*>
     _Tp* operator-=(ptrdiff_t __op) _NOEXCEPT          {return fetch_sub(__op) - __op;}
 };
 
+#if _LIBCPP_STD_VER > 17
+
+// atomic_ref<T>
+//
+// atomic_ref applies atomic operations to an object that keeps the type and
+// layout it was declared with, so it cannot go through _Atomic(T) like
+// atomic<T> does. The GCC-style builtins below take a plain _Tp* instead, and
+// GenMC's interpreter models them as atomic accesses to the referenced object.
+// Alignment is the one thing atomic_ref does ask for beyond the plain type;
+// see required_alignment.
+//
+// Unlike atomic<T>, every operation is const: it mutates the referent, not the
+// reference.
+//
+// The arithmetic that C++20 gives a floating-point atomic_ref is absent: the
+// interpreter implements atomic read-modify-write for integers only, so the
+// builtin cannot serve it, and reaching for it is a compile error rather than
+// a wrong answer. Loads, stores, exchanges and compare-exchanges of a
+// floating-point referent all work through the generic template.
+
+// The builtins compare and copy whole objects, padding bits included, but a
+// compare-exchange is specified to ignore those bits. Zeroing the padding of
+// every value passed to a builtin keeps the two in agreement, and also stops a
+// store from publishing indeterminate padding. Values whose padding was set by
+// a plain write, before any access through an atomic_ref, are still beyond
+// reach; nothing short of an atomic type can fix that.
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+_Tp* __atomic_ref_clear_padding(_Tp& __v) _NOEXCEPT
+{
+#if __has_builtin(__builtin_clear_padding)
+    __builtin_clear_padding(&__v);
+#endif
+    return &__v;
+}
+
+template <class _Tp, bool = is_integral<_Tp>::value && !is_same<_Tp, bool>::value>
+struct __atomic_ref_base  // false
+{
+protected:
+    _Tp* __ptr_;
+
+    // Atomic access needs natural alignment, which a type's own requirement
+    // can fall short of: an eight-byte object declared alignof(1) cannot be
+    // loaded atomically. Sizes that are not a power of two, or are wider than
+    // any supported atomic, ask for nothing extra, being never lock-free.
+    static _LIBCPP_CONSTEXPR size_t __min_alignment =
+        (sizeof(_Tp) & (sizeof(_Tp) - 1)) || sizeof(_Tp) > 16 ? 0 : sizeof(_Tp);
+
+public:
+    typedef _Tp value_type;
+
+    static _LIBCPP_CONSTEXPR size_t required_alignment =
+        alignof(_Tp) > __min_alignment ? alignof(_Tp) : __min_alignment;
+    // The null pointer in both queries below asks about a suitably aligned
+    // object, which the compiler answers at compile time. Naming __ptr_
+    // instead would leave is_lock_free() calling a runtime the interpreter
+    // does not provide.
+    static _LIBCPP_CONSTEXPR bool is_always_lock_free =
+        __atomic_always_lock_free(sizeof(_Tp), 0);
+
+    _LIBCPP_INLINE_VISIBILITY
+    bool is_lock_free() const _NOEXCEPT
+        {return __atomic_is_lock_free(sizeof(_Tp), 0);}
+
+    _LIBCPP_INLINE_VISIBILITY
+    explicit __atomic_ref_base(_Tp& __obj) _NOEXCEPT : __ptr_(&__obj) {}
+    _LIBCPP_INLINE_VISIBILITY
+    __atomic_ref_base(const __atomic_ref_base&) _NOEXCEPT = default;
+    __atomic_ref_base& operator=(const __atomic_ref_base&) = delete;
+
+    _LIBCPP_INLINE_VISIBILITY
+    void store(_Tp __d, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+      _LIBCPP_CHECK_STORE_MEMORY_ORDER(__m)
+        {__atomic_store(__ptr_, __atomic_ref_clear_padding(__d),
+                        __gcc_atomic::__to_gcc_order(__m));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp load(memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+      _LIBCPP_CHECK_LOAD_MEMORY_ORDER(__m)
+        {_Tp __r; __atomic_load(__ptr_, &__r, __gcc_atomic::__to_gcc_order(__m)); return __r;}
+    _LIBCPP_INLINE_VISIBILITY
+    operator _Tp() const _NOEXCEPT {return load();}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp exchange(_Tp __d, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {_Tp __r; __atomic_exchange(__ptr_, __atomic_ref_clear_padding(__d), &__r,
+                                    __gcc_atomic::__to_gcc_order(__m)); return __r;}
+
+    // __e is the caller's object, so the cleared copy is what the builtin
+    // compares against; on failure it holds the value read, which is what the
+    // caller is owed.
+    //
+    // Weakness is a template parameter because the builtin needs it as a
+    // constant: passed as an argument, each call site emits a weak and a strong
+    // compare-exchange behind a branch, and the weak one keeps GenMC from
+    // treating the strong form as strong.
+    template <bool _Weak>
+    _LIBCPP_INLINE_VISIBILITY
+    bool __compare_exchange(_Tp& __e, _Tp& __d,
+                            memory_order __s, memory_order __f) const _NOEXCEPT
+    {
+        _Tp __copy = __e;
+        bool __r = __atomic_compare_exchange(__ptr_,
+                                             __atomic_ref_clear_padding(__copy),
+                                             __atomic_ref_clear_padding(__d), _Weak,
+                                             __gcc_atomic::__to_gcc_order(__s),
+                                             __gcc_atomic::__to_gcc_failure_order(__f));
+        if (!__r)
+            __e = __copy;
+        return __r;
+    }
+
+    _LIBCPP_INLINE_VISIBILITY
+    bool compare_exchange_weak(_Tp& __e, _Tp __d,
+                               memory_order __s, memory_order __f) const _NOEXCEPT
+      _LIBCPP_CHECK_EXCHANGE_MEMORY_ORDER(__s, __f)
+        {return __compare_exchange<true>(__e, __d, __s, __f);}
+    _LIBCPP_INLINE_VISIBILITY
+    bool compare_exchange_strong(_Tp& __e, _Tp __d,
+                                 memory_order __s, memory_order __f) const _NOEXCEPT
+      _LIBCPP_CHECK_EXCHANGE_MEMORY_ORDER(__s, __f)
+        {return __compare_exchange<false>(__e, __d, __s, __f);}
+    _LIBCPP_INLINE_VISIBILITY
+    bool compare_exchange_weak(_Tp& __e, _Tp __d,
+                               memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return compare_exchange_weak(__e, __d, __m, __m);}
+    _LIBCPP_INLINE_VISIBILITY
+    bool compare_exchange_strong(_Tp& __e, _Tp __d,
+                                 memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return compare_exchange_strong(__e, __d, __m, __m);}
+
+    _LIBCPP_INLINE_VISIBILITY
+    void wait(_Tp __v, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {const typename __atomic_repr_type<sizeof(_Tp)>::type __want = __atomic_repr(__v);
+         while (__atomic_repr(load(__m)) == __want) ;}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_one() const _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_all() const _NOEXCEPT {}
+};
+
+// atomic_ref<Integral>
+
+template <class _Tp>
+struct __atomic_ref_base<_Tp, true>
+    : public __atomic_ref_base<_Tp, false>
+{
+    typedef __atomic_ref_base<_Tp, false> __base;
+    typedef _Tp difference_type;
+
+    _LIBCPP_INLINE_VISIBILITY
+    explicit __atomic_ref_base(_Tp& __obj) _NOEXCEPT : __base(__obj) {}
+
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp fetch_add(_Tp __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_add(this->__ptr_, __op, __gcc_atomic::__to_gcc_order(__m));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp fetch_sub(_Tp __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_sub(this->__ptr_, __op, __gcc_atomic::__to_gcc_order(__m));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp fetch_and(_Tp __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_and(this->__ptr_, __op, __gcc_atomic::__to_gcc_order(__m));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp fetch_or(_Tp __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_or(this->__ptr_, __op, __gcc_atomic::__to_gcc_order(__m));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp fetch_xor(_Tp __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_xor(this->__ptr_, __op, __gcc_atomic::__to_gcc_order(__m));}
+
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator++(int) const _NOEXCEPT         {return fetch_add(_Tp(1));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator--(int) const _NOEXCEPT         {return fetch_sub(_Tp(1));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator++() const _NOEXCEPT            {return _Tp(fetch_add(_Tp(1)) + _Tp(1));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator--() const _NOEXCEPT            {return _Tp(fetch_sub(_Tp(1)) - _Tp(1));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator+=(_Tp __op) const _NOEXCEPT    {return _Tp(fetch_add(__op) + __op);}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator-=(_Tp __op) const _NOEXCEPT    {return _Tp(fetch_sub(__op) - __op);}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator&=(_Tp __op) const _NOEXCEPT    {return _Tp(fetch_and(__op) & __op);}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator|=(_Tp __op) const _NOEXCEPT    {return _Tp(fetch_or(__op) | __op);}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator^=(_Tp __op) const _NOEXCEPT    {return _Tp(fetch_xor(__op) ^ __op);}
+};
+
+// atomic_ref<T>
+
+template <class _Tp>
+struct atomic_ref
+    : public __atomic_ref_base<_Tp>
+{
+    typedef __atomic_ref_base<_Tp> __base;
+
+    static_assert(is_trivially_copyable<_Tp>::value,
+      "std::atomic_ref<T> requires that 'T' be a trivially copyable type");
+
+    _LIBCPP_INLINE_VISIBILITY
+    explicit atomic_ref(_Tp& __obj) _NOEXCEPT : __base(__obj) {}
+    _LIBCPP_INLINE_VISIBILITY
+    atomic_ref(const atomic_ref&) _NOEXCEPT = default;
+    atomic_ref& operator=(const atomic_ref&) = delete;
+
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp operator=(_Tp __d) const _NOEXCEPT
+        {__base::store(__d); return __d;}
+};
+
+// atomic_ref<T*>
+
+template <class _Tp>
+struct atomic_ref<_Tp*>
+    : public __atomic_ref_base<_Tp*, false>
+{
+    typedef __atomic_ref_base<_Tp*, false> __base;
+    typedef ptrdiff_t difference_type;
+
+    _LIBCPP_INLINE_VISIBILITY
+    explicit atomic_ref(_Tp*& __obj) _NOEXCEPT : __base(__obj) {}
+    _LIBCPP_INLINE_VISIBILITY
+    atomic_ref(const atomic_ref&) _NOEXCEPT = default;
+    atomic_ref& operator=(const atomic_ref&) = delete;
+
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator=(_Tp* __d) const _NOEXCEPT
+        {__base::store(__d); return __d;}
+
+    // The builtins treat the referent as an integer, so pointer arithmetic
+    // has to be scaled to the pointee size by hand.
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* fetch_add(ptrdiff_t __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_add(this->__ptr_, __op * ptrdiff_t(sizeof(_Tp)),
+                                   __gcc_atomic::__to_gcc_order(__m));}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* fetch_sub(ptrdiff_t __op, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __atomic_fetch_sub(this->__ptr_, __op * ptrdiff_t(sizeof(_Tp)),
+                                   __gcc_atomic::__to_gcc_order(__m));}
+
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator++(int) const _NOEXCEPT               {return fetch_add(1);}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator--(int) const _NOEXCEPT               {return fetch_sub(1);}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator++() const _NOEXCEPT                  {return fetch_add(1) + 1;}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator--() const _NOEXCEPT                  {return fetch_sub(1) - 1;}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator+=(ptrdiff_t __op) const _NOEXCEPT    {return fetch_add(__op) + __op;}
+    _LIBCPP_INLINE_VISIBILITY
+    _Tp* operator-=(ptrdiff_t __op) const _NOEXCEPT    {return fetch_sub(__op) - __op;}
+};
+
+#endif // _LIBCPP_STD_VER > 17
+
 // atomic_is_lock_free
 
 template <class _Tp>
@@ -1752,6 +2109,14 @@ typedef struct atomic_flag
 {
     _Atomic(bool) __a_;
 
+#if _LIBCPP_STD_VER > 17
+    _LIBCPP_INLINE_VISIBILITY
+    bool test(memory_order __m = memory_order_seq_cst) const volatile _NOEXCEPT
+        {return __c11_atomic_load(&__a_, __m);}
+    _LIBCPP_INLINE_VISIBILITY
+    bool test(memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {return __c11_atomic_load(&__a_, __m);}
+#endif
     _LIBCPP_INLINE_VISIBILITY
     bool test_and_set(memory_order __m = memory_order_seq_cst) volatile _NOEXCEPT
         {return __c11_atomic_exchange(&__a_, true, __m);}
@@ -1765,6 +2130,25 @@ typedef struct atomic_flag
     void clear(memory_order __m = memory_order_seq_cst) _NOEXCEPT
         {__c11_atomic_store(&__a_, false, __m);}
 
+#if _LIBCPP_STD_VER > 17
+    _LIBCPP_INLINE_VISIBILITY
+    void wait(bool __v, memory_order __m = memory_order_seq_cst) const volatile _NOEXCEPT
+        {const bool __want = __v;
+         while (test(__m) == __want) ;}
+    _LIBCPP_INLINE_VISIBILITY
+    void wait(bool __v, memory_order __m = memory_order_seq_cst) const _NOEXCEPT
+        {const bool __want = __v;
+         while (test(__m) == __want) ;}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_one() volatile _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_one() _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_all() volatile _NOEXCEPT {}
+    _LIBCPP_INLINE_VISIBILITY
+    void notify_all() _NOEXCEPT {}
+#endif
+
     _LIBCPP_INLINE_VISIBILITY
 #ifndef _LIBCPP_CXX03_LANG
     atomic_flag() _NOEXCEPT = default;
@@ -1787,6 +2171,36 @@ private:
 #endif
 } atomic_flag;
 
+#if _LIBCPP_STD_VER > 17
+inline _LIBCPP_INLINE_VISIBILITY
+bool
+atomic_flag_test(const volatile atomic_flag* __o) _NOEXCEPT
+{
+    return __o->test();
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+bool
+atomic_flag_test(const atomic_flag* __o) _NOEXCEPT
+{
+    return __o->test();
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+bool
+atomic_flag_test_explicit(const volatile atomic_flag* __o, memory_order __m) _NOEXCEPT
+{
+    return __o->test(__m);
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+bool
+atomic_flag_test_explicit(const atomic_flag* __o, memory_order __m) _NOEXCEPT
+{
+    return __o->test(__m);
+}
+#endif
+
 inline _LIBCPP_INLINE_VISIBILITY
 bool
 atomic_flag_test_and_set(volatile atomic_flag* __o) _NOEXCEPT
@@ -1843,6 +2257,134 @@ atomic_flag_clear_explicit(atomic_flag* __o, memory_order __m) _NOEXCEPT
     __o->clear(__m);
 }
 
+#if _LIBCPP_STD_VER > 17
+
+// waiting and notifying
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_wait(const volatile atomic<_Tp>* __o, typename atomic<_Tp>::value_type __v) _NOEXCEPT
+{
+    __o->wait(__v);
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_wait(const atomic<_Tp>* __o, typename atomic<_Tp>::value_type __v) _NOEXCEPT
+{
+    __o->wait(__v);
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_wait_explicit(const volatile atomic<_Tp>* __o, typename atomic<_Tp>::value_type __v,
+                     memory_order __m) _NOEXCEPT
+{
+    __o->wait(__v, __m);
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_wait_explicit(const atomic<_Tp>* __o, typename atomic<_Tp>::value_type __v,
+                     memory_order __m) _NOEXCEPT
+{
+    __o->wait(__v, __m);
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_notify_one(volatile atomic<_Tp>* __o) _NOEXCEPT
+{
+    __o->notify_one();
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_notify_one(atomic<_Tp>* __o) _NOEXCEPT
+{
+    __o->notify_one();
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_notify_all(volatile atomic<_Tp>* __o) _NOEXCEPT
+{
+    __o->notify_all();
+}
+
+template <class _Tp>
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_notify_all(atomic<_Tp>* __o) _NOEXCEPT
+{
+    __o->notify_all();
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_wait(const volatile atomic_flag* __o, bool __v) _NOEXCEPT
+{
+    __o->wait(__v);
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_wait(const atomic_flag* __o, bool __v) _NOEXCEPT
+{
+    __o->wait(__v);
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_wait_explicit(const volatile atomic_flag* __o, bool __v, memory_order __m) _NOEXCEPT
+{
+    __o->wait(__v, __m);
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_wait_explicit(const atomic_flag* __o, bool __v, memory_order __m) _NOEXCEPT
+{
+    __o->wait(__v, __m);
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_notify_one(volatile atomic_flag* __o) _NOEXCEPT
+{
+    __o->notify_one();
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_notify_one(atomic_flag* __o) _NOEXCEPT
+{
+    __o->notify_one();
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_notify_all(volatile atomic_flag* __o) _NOEXCEPT
+{
+    __o->notify_all();
+}
+
+inline _LIBCPP_INLINE_VISIBILITY
+void
+atomic_flag_notify_all(atomic_flag* __o) _NOEXCEPT
+{
+    __o->notify_all();
+}
+
+#endif // _LIBCPP_STD_VER > 17
+
 // fences
 
 inline _LIBCPP_INLINE_VISIBILITY
diff --git a/tests/correct/infr/cpp-atomic-flag-test/args.rc11.mo.in b/tests/correct/infr/cpp-atomic-flag-test/args.rc11.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-flag-test/args.rc11.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-flag-test/args.rc11.wb.in b/tests/correct/infr/cpp-atomic-flag-test/args.rc11.wb.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-flag-test/args.rc11.wb.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-flag-test/args.sc.mo.in b/tests/correct/infr/cpp-atomic-flag-test/args.sc.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-flag-test/args.sc.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-flag-test/expected.rc11.mo.in b/tests/correct/infr/cpp-atomic-flag-test/expected.rc11.mo.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-flag-test/expected.rc11.mo.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-flag-test/expected.rc11.wb.in b/tests/correct/infr/cpp-atomic-flag-test/expected.rc11.wb.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-flag-test/expected.rc11.wb.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-flag-test/expected.sc.mo.in b/tests/correct/infr/cpp-atomic-flag-test/expected.sc.mo.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-flag-test/expected.sc.mo.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-flag-test/variants/cpp-atomic-flag-test.cpp b/tests/correct/infr/cpp-atomic-flag-test/variants/cpp-atomic-flag-test.cpp
new file mode 100644
index 00000000..b80bbc2d
--- /dev/null
+++ b/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;
+}
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/args.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-mp/args.rc11.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-mp/args.rc11.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/args.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-mp/args.rc11.wb.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-mp/args.rc11.wb.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/args.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-mp/args.sc.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-mp/args.sc.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.mo.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.mo.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.wb.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-mp/expected.rc11.wb.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/expected.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-mp/expected.sc.mo.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-mp/expected.sc.mo.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-ref-mp/variants/cpp-atomic-ref-mp.cpp b/tests/correct/infr/cpp-atomic-ref-mp/variants/cpp-atomic-ref-mp.cpp
new file mode 100644
index 00000000..f980b433
--- /dev/null
+++ b/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;
+}
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/args.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-repr/args.rc11.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-repr/args.rc11.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/args.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-repr/args.rc11.wb.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-repr/args.rc11.wb.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/args.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-repr/args.sc.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-repr/args.sc.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.mo.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.mo.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.wb.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-repr/expected.rc11.wb.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/expected.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-repr/expected.sc.mo.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-repr/expected.sc.mo.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-repr/variants/cpp-atomic-ref-repr.cpp b/tests/correct/infr/cpp-atomic-ref-repr/variants/cpp-atomic-ref-repr.cpp
new file mode 100644
index 00000000..a07e2c18
--- /dev/null
+++ b/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;
+}
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.wb.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-rmw/args.rc11.wb.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/args.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-rmw/args.sc.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-rmw/args.sc.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.mo.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.mo.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.wb.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-rmw/expected.rc11.wb.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/expected.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-rmw/expected.sc.mo.in
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-rmw/expected.sc.mo.in
@@ -0,0 +1 @@
+2
diff --git a/tests/correct/infr/cpp-atomic-ref-rmw/variants/cpp-atomic-ref-rmw.cpp b/tests/correct/infr/cpp-atomic-ref-rmw/variants/cpp-atomic-ref-rmw.cpp
new file mode 100644
index 00000000..aee63dee
--- /dev/null
+++ b/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;
+}
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.wb.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait-repr/args.rc11.wb.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/args.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-wait-repr/args.sc.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait-repr/args.sc.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.mo.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.mo.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.wb.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.rc11.wb.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.sc.mo.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait-repr/expected.sc.mo.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-wait-repr/variants/cpp-atomic-ref-wait-repr.cpp b/tests/correct/infr/cpp-atomic-ref-wait-repr/variants/cpp-atomic-ref-wait-repr.cpp
new file mode 100644
index 00000000..de10e1a7
--- /dev/null
+++ b/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;
+}
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/args.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-wait/args.rc11.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait/args.rc11.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/args.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-wait/args.rc11.wb.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait/args.rc11.wb.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/args.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-wait/args.sc.mo.in
new file mode 100644
index 00000000..8eb9c50a
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait/args.sc.mo.in
@@ -0,0 +1 @@
+ | -std=c++20
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.mo.in b/tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.mo.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.mo.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.wb.in b/tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.wb.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait/expected.rc11.wb.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/expected.sc.mo.in b/tests/correct/infr/cpp-atomic-ref-wait/expected.sc.mo.in
new file mode 100644
index 00000000..d00491fd
--- /dev/null
+++ b/tests/correct/infr/cpp-atomic-ref-wait/expected.sc.mo.in
@@ -0,0 +1 @@
+1
diff --git a/tests/correct/infr/cpp-atomic-ref-wait/variants/cpp-atomic-ref-wait.cpp b/tests/correct/infr/cpp-atomic-ref-wait/variants/cpp-atomic-ref-wait.cpp
new file mode 100644
index 00000000..d27330c0
--- /dev/null
+++ b/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;
+}
diff --git a/tests/wrong/racy/cpp-atomic-ref-mp-rlx/args.rc11.wb.in b/tests/wrong/racy/cpp-atomic-ref-mp-rlx/args.rc11.wb.in
new file mode 100644
index 00000000..e23b2aef
--- /dev/null
+++ b/tests/wrong/racy/cpp-atomic-ref-mp-rlx/args.rc11.wb.in
@@ -0,0 +1 @@
+-std=c++20
diff --git a/tests/wrong/racy/cpp-atomic-ref-mp-rlx/variants/cpp-atomic-ref-mp-rlx0.cpp b/tests/wrong/racy/cpp-atomic-ref-mp-rlx/variants/cpp-atomic-ref-mp-rlx0.cpp
new file mode 100644
index 00000000..48f9c0ff
--- /dev/null
+++ b/tests/wrong/racy/cpp-atomic-ref-mp-rlx/variants/cpp-atomic-ref-mp-rlx0.cpp
@@ -0,0 +1,37 @@
+#include <pthread.h>
+#include <atomic>
+#include <cstdint>
+
+/* Relaxed accesses through an atomic_ref order nothing, so the plain accesses
+ * to `data` race and the checker has to say so. */
+std::uint32_t data = 0;
+std::uint32_t flag = 0;
+
+void *thread_1(void *unused)
+{
+	std::atomic_ref<std::uint32_t> f{flag};
+
+	data = 1;
+	f.store(1, std::memory_order_relaxed);
+	return nullptr;
+}
+
+void *thread_2(void *unused)
+{
+	std::atomic_ref<std::uint32_t> f{flag};
+	std::uint32_t r_data = 0;
+
+	if (f.load(std::memory_order_relaxed))
+		r_data = data;
+	return nullptr;
+}
+
+int main()
+{
+	pthread_t t1, t2;
+
+	pthread_create(&t1, nullptr, thread_1, nullptr);
+	pthread_create(&t2, nullptr, thread_2, nullptr);
+
+	return 0;
+}
diff --git a/tests/wrong/racy/cpp-atomic-ref-mp-rlx/variants/cpp-atomic-ref-mp-rlx0.rc11.wb.trace b/tests/wrong/racy/cpp-atomic-ref-mp-rlx/variants/cpp-atomic-ref-mp-rlx0.rc11.wb.trace
new file mode 100644
index 00000000..7c9f3ec3
--- /dev/null
+++ b/tests/wrong/racy/cpp-atomic-ref-mp-rlx/variants/cpp-atomic-ref-mp-rlx0.rc11.wb.trace
@@ -0,0 +1,26 @@
+Error: Non-atomic race!
+Event (2, 2) conflicts with event (1, 1) in graph:
+<-1, 0> :
+	(0, 1): THREAD_CREATE [thread 1] pthread.h:146
+	(0, 2): THREAD_CREATE [thread 2] pthread.h:146
+	(0, 3): THREAD_END
+<0, 1> main:
+	(1, 1): Wna (data, ?) cpp-atomic-ref-mp-rlx0.cpp:14
+	(1, 2): Wrlx (flag, 1) atomic:1367
+	(1, 3): THREAD_END
+<0, 2> main:
+	(2, 1): Rrlx (flag, 1) [(1, 2)] atomic:1372
+	(2, 2): Rna (data, 1) [(1, 1)] cpp-atomic-ref-mp-rlx0.cpp:25
+
+Trace to (2, 2):
+[main] pthread.h: 146: (*__newthread) = __VERIFIER_thread_create(__attr, __start_routine, __arg);
+[_Z8thread_1Pv] cpp-atomic-ref-mp-rlx0.cpp: 14: data = 1;
+[_Z8thread_1Pv] atomic: 1367: {__atomic_store(__ptr_, __atomic_ref_clear_padding(__d),
+[_Z8thread_2Pv] atomic: 1372: {_Tp __r; __atomic_load(__ptr_, &__r, __gcc_atomic::__to_gcc_order(__m)); return __r;}
+[_Z8thread_2Pv] cpp-atomic-ref-mp-rlx0.cpp: 25: r_data = data;
+Trace to (1, 1):
+[main] pthread.h: 146: (*__newthread) = __VERIFIER_thread_create(__attr, __start_routine, __arg);
+[_Z8thread_1Pv] cpp-atomic-ref-mp-rlx0.cpp: 14: data = 1;
+
+*** Verification unsuccesful.
+Number of complete executions explored: 1