Model Checking Futexes.

The futex Linux system call enables implementing performant inter-thread synchronisation primitives, such as mutexes and condition variables. However, the futex system call is notoriously tricky to use correctly. In this case study, we use the Spin model checker to verify safety properties of a number of futex-based mutex and condition variable implementations. We show how model checking is able to detect bugs that affected real-world implementations, and confirm current implementations are correct. The Promela models we have developed are available as open source, and may be useful as teaching material for classes that cover futex-based synchronisation primitives, and as a template on how to perform formal verification on new synchronisation primitive designs.