Non-blocking concurrent algorithms are hard!

• In published work on Synthesis, a non-blocking operating system implementation, three separate races were found:

  • One ABA problem in LIFO stack
  • One likely race in MP-SC FIFO queue
  • One interesting corner case in quaject callback handling

• It's hard to get these right! Ad hoc reasoning doesn't cut it.

• Non-blocking algorithms are too hard for the programmer

• Let's get it right once (and verify this!)

Notes: