robur-coop / miou

A simple scheduler for OCaml 5
https://docs.osau.re/miou/index.html
MIT License
93 stars 7 forks source link

Compiler bug in OCaml 5 affecting `Queue.snapshot` #14

Closed polytypic closed 1 year ago

polytypic commented 1 year ago

Just today we identified a compiler bug in OCaml 5.x that affects the correctness of the snapshot algorithm I suggested for the Queue implementation in #2.

Here is the current snapshot code: https://github.com/robur-coop/miou/blob/32e0b8adc7a6a92e14dae12d1fa1991ce41f71a5/lib/queue.ml#L92-L98

The problem is that currently the OCaml 5 compiler incorrectly optimizes out the Atomic.get on the last line of code. One can see this in the output of the compiler using the godbolt service. Specifically, on line 28 of the output, there is a cmpq %rdx,%rdx instruction. IOW, it is comparing a register to itself — which is always true.

One can work around this compiler bug by using Sys.opaque_identity:

 let rec snapshot t : 'a snapshot = 
   let head = Atomic.get t.head and tail = Atomic.get t.tail in 
   match Atomic.get tail.next with 
   | Some node -> 
       let _ = Atomic.compare_and_set t.tail tail node in 
       snapshot t 
   | None -> if Atomic.get (Sys.opaque_identity t.head) != head then snapshot t else (head, tail) 

The use of Sys.opaque_identity above prevents the compiler from incorrectly optimizing the Atomic.get out. You can also see this in the compiler output. Now line 28 has a movq (%rax),%rax and line 29 has cmpq %rdx,%rax.

polytypic commented 1 year ago

This compiler bug affects more things than I initially thought.

dinosaure commented 1 year ago

Fixed by ada18bcba5d27fe3448cf998abe32bf07c0a8da2, thanks!