LoadBufferingLitmusTest

test.litmus

{ *x = 0, *y = 0 } // fixed initial state, shared memory x and y

// Concurrent Program with threads P0 and P1
P0 (atomic_int* y,atomic_int* x) {
  int r0 = atomic_load_explicit(x,memory_order_relaxed);
  atomic_store_explicit(y,1,memory_order_relaxed);
}

P1 (atomic_int* y,atomic_int* x) {
  int r0 = atomic_load_explicit(y,memory_order_relaxed);
  atomic_store_explicit(x,1,memory_order_relaxed);
}

// Question over the final state
exists (P0:r0=1 /\ P1:r0=1)

Per the C11 standard section 5.1.2.4 Multi-threaded executions and data races:
Clause 5 ... In addition, there are relaxed atomic operations, which are not synchronization operations, ...
And section 7.17.3 Order and consistency:
Clause 2 For memory_order_relaxed, no operation orders memory.

So relaxed atomic operations don't impose any ordering requirements (even among themselves) and cannot be used for synchronization.

Using relaxed atomics for synchronization (between threads) is against the standard and could be considered invoking undefined behaviour (UB). The compiler and hardware are thus free to generate unexpected results.

Yes you are right - the idea behind this test is that we wish to strengthen the implementation, which would inform changes in the standard later, if accepted. The standard ratifies existing practice, I propose to change the practice.

Why do we wish to strengthen the implementation? What practice requires a stronger implementation?

One reason is that we currently permit re-ordering (observable on AArch64, RISC-V, and PPC) which breaks the ability to reason about relaxed atomics - and verify anything regarding them.

and cannot be used for synchronization.

Wait, I checked C23 and it doesn't say cannot, only that the above outcome { P0:r0 = 1 /\ P1:r0 = 1} is permitted. Where do you see cannot as that has a particular meaning in standards.

As far as I can see, the standard provides no guarantees for what happens on hardware, and says operations using memory_order_relaxed is not considered a synchronisation operation.

So, according to the current standard, my proposal is to implement a model that enforces synchronisation between loads and stores on each thread, which is strictly stronger than what is allowed but not UB. Much like how the standard permits behaviours (for example the above) outcome that you wouldn't observe anyway (e.g. on x86 or MIPS)

I am quoting from the C11 standard so text might have changed in later revisions.
there are relaxed atomic operations, which are not synchronization operations ⇒ relaxed atomics cannot be used for synchronization

Understood, the term "shall" is required to make that implication hold. From section 4: "In this document, "shall" is to be interpreted as a requirement on an implementation or on a program; conversely, "shall not" is to be interpreted as a prohibition."

Further "Undefined behavior is otherwise indicated in this document by the words "undefined behavior" or by the omission of any explicit definition of behavior. There is no difference in emphasis among these three; they all describe "behavior that is undefined". No notion of 'Not' here.

The behaviour of relaxed is well defined in C23 with example litmus tests like the above, but its not UB as this test would still exhibit a subset of behaviours permitted by the standard

Possibly undefined behaviour is a bit over the top. But using a language feature (e.g. relaxed atomics) for something is the standard specifies is not supported should be considered to invoke implementation defined behaviour or unspecified behaviour.