Analysing futex-based synchronisation primitives using model checking

Abstract The futex Linux system call enables implementing performant inter-thread and inter-process synchronisation primitives, such as mutexes and condition variables. However, the futex system call is notoriously difficult to use correctly. An early implementation of futex-based mutexes in the Linux Native POSIX Thread Library suffered from a subtle defect. When teaching about clever futex-based mutex designs that avoid these early shortcomings, we have found that their intricacies are hard to understand and difficult to convey to students. In this case study, we use the Promela modelling language to model a number of futex-based mutex and condition variable implementations, and the Spin model checker to verify safety properties over these models. We show that model checking is effective at confirming known bugs that affected real-world implementations and at confirming that current implementations do indeed behave correctly in multi-threaded environments. We also investigate the effectiveness of symmetry reduction and two memory usage reduction techniques for increasing the scalability of model checking in this domain. The Promela models we have developed are available as open source. They may be useful as teaching material for classes that cover futex-based synchronisation primitives and as a template for performing formal verification on new synchronisation primitive designs.