CSE of non-atomic load around atomic load breaks SC

[polytypic]

Here is an example (see also in godbolt):

let cse_breaks_sc non_atomic atomic =
  let before = !non_atomic in
  (* happens before *)
  let fence = Atomic.get atomic in
  (* happens before *)
  let after = !non_atomic in
  (* The above non_atomic read is optimized away, which breaks sequential consistency. *)
  before - after + fence

What can happen is that another domain executes something like:

non_atomic := also_new_value;
(* happens before *)
Atomic.set atomic new_value;

and due to the CSE on the second load of non_atomic the program can give results that are not consistent with the memory model.

Specifically, the Atomic.get atomic gives the new_value (which means the Atomic.set happens before the Atomic.get), but then the second read of the non_atomic does not return the also_new_value, because it has been optimized away.

The arithmetic at the end is just so that the compiler doesn't just optimize out all the reads. Also, the example is minimized. (In practical use cases there is typically more work between the reads of the non_atomic. The first read is done to see if it makes sense to try to do that work (which also includes the atomic read, which is typically more expensive (i.e. it is reading a contested memory location)) and the second read (after the atomic read) is to ensure that in fact no other domain running in parallel has completed the work before we did.)

I checked that this also happens with 5.2.0+trunk switch freshly created with opam.

[kayceesrk]

This is a bug. Here, the non-atomic load (let after = !non_atomic) is moved before an atomic load (let fence = Atomic.get atomic). The memory model disallows this. See Section 7.1 in https://kcsrk.info/papers/pldi18-memory.pdf,

$\text{po}_{at-}$: Operations must not be moved before prior atomic operations.

The fix in #12715 is not strong enough. In particular, Op_other chosen for atomic loads only makes the result of the operation unpredictable and, hence, unreusable. However, it does not invalidate any other equations.

ocaml/asmcomp/CSEgen.ml

Lines 333 to 334 in a46fd9e

	(* An initializing store or an "other" operation do not invalidate
	any equations, but we do not know anything about the results. *)

However, we should invalidate prior loads of mutable fields and stores. IINM, OCaml doesn't eliminate redundant stores: https://godbolt.org/z/s9GoK1Keb. So treating atomic loads in the same category as a non-initialising store would fix this issue:

ocaml/asmcomp/CSEgen.ml

Lines 338 to 344 in a46fd9e

	| Op_store true ->
	(* A non-initializing store can invalidate
	anything we know about prior mutable loads. *)
	let n1 = set_unknown_regs n (Proc.destroyed_at_oper i.desc) in
	let n2 = set_unknown_regs n1 i.res in
	let n3 = self#kill_loads n2 in
	{i with next = self#cse n3 i.next}

CC @lthls and @xavierleroy, who are familiar with the CSE code.

[lthls]

I'm not completely convinced that this is forbidden by the model (this is about a data race breaking sequential consistency, after all). But I'm fine with forgetting CSE equations on atomic loads.
Keep in mind though that at this point almost all reads are mutable, so this will also impact CSE of a lot of other expressions:

let f p atomic =
  let x = fst p in
  let y = Atomic.get atomic in
  let z = fst p (* Not CSE'd anymore *) in
  ...

[gasche]

Personally I believe that CSE of non-atomic reads across an atomic read is a bug according to the operational semantics given in the paper. When we perform an atomic read, we update the frontier of the thread, so future non-atomic reads have a more recent view of the shared state. Reusing the result of a previous non-atomic read is invalid because the result of the previous non-atomic read may be forbidden by the updated, more accurate/restricted frontier.

On the other hand, I suspect that it would be valid to move the previous non-atomic read after the atomic read, and thus recover CSE in that case.

In your example:

(* Example input: *)
  let x = fst p in
  let y = Atomic.get atomic in
  let z = fst p in

(* This is an incorrect optimization: *)
  let x = fst p in
  let y = Atomic.get atomic in
  let z = x in

(* This may be a correct optimization: *)
  let y = Atomic.get atomic in
  let x = fst p in
  let z = x in

[maranget]

KC’s explanation does convince me: this is a bug. It is my opinion that CSE on reads non-atomic reads of mutable cells should be disabled (is this possible?) . This would result in an implementation stronger than the model on machines that do not re-order reads. But this is erring on the safe side. —Luc

…

On 14 Dec 2023, at 10:29, Gabriel Scherer ***@***.***> wrote: Personally I believe that CSE of non-atomic reads across an atomic read is a bug according to the operational semantics given in the paper. When we perform an atomic read, we update the frontier of the thread, so future non-atomic reads have a more recent view of the shared state. Reusing the result of a previous non-atomic read is invalid because the result of the previous non-atomic read may be forbidden by the updated, more accurate/restricted frontier. On the other hand, I believe that it would be valid to move the previous non-atomic read after the atomic read, and thus recover CSE in that case. In your example: (* Example input: *) let x = fst p in let y = Atomic.get atomic in let z = fst p in (* This is an incorrect optimization: *) let x = fst p in let y = Atomic.get atomic in let z = x in (* This is a correct optimization: *) let y = Atomic.get atomic in let x = fst p in let z = x in — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[polytypic]

it would be valid to move the previous non-atomic read after the atomic read

Yes, the example is simplified from the actual code I had when I discovered the issue. The original code was more like:

let x = !non_atomic in
if x != this_is_done then begin
  (* ... *)
  let y = Atomic.get atomic in
  if !non_atomic == x then begin
    (* ... *)
    if Atomic.compare_and_set atomic ... ... then
      non_atomic := this_is_done
    else
      (* ... *)
  end
end

(This is part of an intricate algorithm/method I'm developing for a kind of "chainable" multi-location atomic updates, but that is beside the point.)

[kayceesrk]

I'm not completely convinced that this is forbidden by the model

The original code in the issue is a variant of the common message-passing pattern:

let msg = ref 0
let flag = Atomic.make false

let sender msg flag =
  msg := 42;
  Atomic.set flag true

let receiver msg flag =
  let m1 = !msg in
  let f = Atomic.get flag in
  let m2 = !msg in
  assert (f = false || m2 = 42);
  ignore @@ Sys.opaque_identity m1;
  ()

Due to CSE, m2 may be 0, and the assertion may fail.

This execution can be shown as invalid under axiomatic execution as well (Section 6 of https://kcsrk.info/papers/pldi18-memory.pdf). Given that the second read of msg gets the value from the initialising write to msg, we have the following relations between the operations,

  msg := 42; --po/hb--> Atomic.set flag true --rf/hb--> Atomic.get flag --po/hb--> let m2 = !msg

Since happens-before is transitive,

msg :=42 --hb--> let m2 = !msg

However, the following is also true

let m2 = !msg --fr--> msg :=42

since msg := 42 overwrites the (initialising) write to msg (let msg = ref 0 --co--> msg := 42), which the second read of msg witnesses (let msg = ref 0 --rf--> let ms = !msg). This violates CoWR.

CoWR There are no E1, E2 such that E1 hb E2, E2 fr E1

[kayceesrk]

On the other hand, I suspect that it would be valid to move the previous non-atomic read after the atomic read, and thus recover CSE in that case.

This is correct, but doesn't it go against the conventional wisdom of optimisations doing loads early and stores late?

[gasche]

I think that this is different (an atomic load is not a store, here it acts like a read barrier), but the point is moot anyway because I don't think we are going to try to do this:

• the CSE pass itself does not move instructions around
• as you suggest, moving non-atomic loads after atomic loads may not always be a good idea, so doing it unconditionally (without information on potential CSE sharing) in an earlier pass is probably not right either

I agree with @maranget that, at least in the short-medium term, we should err on the side of caution for atomic operations and not try to optimize aggressively the code that uses them.

[stedolan]

I agree that this is a bug. CSE should drop all equations at an atomic load: the point of an atomic load is to synchronise with other threads, so whatever you know about the value of nonatomic locations is out of date after an atomic load completes.

I also agree that it would be valid to turn load_na A; load_at B into load_at B; load_na A, but that we shouldn't bother because it's not obviously an improvement. To see this more formally, look at sec. 7 of the paper which determines the subsets of program order that the model is capable of noticing, and note that none of them contain orderings between a nonatomic load and a subsequent atomic load.

[gasche]

Reading this discussion again, there is one thing I missed earlier: the CSE pass will perform CSE of immutable loads anyway, whether or not there is an atomic load in between. We "lose CSE" only for mutable loads. The example of @lthls is carefully crafted because fst p happens to be compiled, today, as a possibly-mutable load -- but this is likely to change eventually. This makes the whole discussion of how exactly to preserve some sharing of (mutable) loads even less important.