Consider the following function/loop:
let rec will_this_ever_return x =
let before = Atomic.get x in
if Atomic.get x == before then
will_this_ever_return xIn OCaml 5, a call of will_this_ever_return x will never return even if the atomic location x would be mutated in parallel. The reason is that the compiler optimizes the second Atomic.get away:
camlExample__will_this_ever_return_268:
subq $8, %rsp
.L101:
cmpq (%r14), %r15
jbe .L102
.L103:
movq (%rax), %rbx ;; <-- let before = Atomic.get x
cmpq %rbx, %rbx ;; <-- Atomic.get x == before
jne .L100
jmp .L101
.L100:
movl $1, %eax
addq $8, %rsp
ret
.L102:
call caml_call_gc@PLT
.L104:
jmp .L103
The Bounding Data Races in Space and Time paper has an example of a "Redundant load (RL)" optimization (page 8), but the location a in that example is a nonatomic location. No "Redundant load" optimization should be applied in the case of an atomic location.
Consider the following function/loop:
In OCaml 5, a call of
will_this_ever_return xwill never return even if the atomic locationxwould be mutated in parallel. The reason is that the compiler optimizes the secondAtomic.getaway:The Bounding Data Races in Space and Time paper has an example of a "Redundant load (RL)" optimization (page 8), but the location
ain that example is a nonatomic location. No "Redundant load" optimization should be applied in the case of an atomic location.