Analysing Futex-based Synchronisation Primitives Using Model Checking
Abstract
The futex Linux system call enables implement-
ing performant inter-thread and inter-process synchronisa-
tion 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 mu-
tex designs that avoid these early shortcomings, we have
found that their intricacies are hard to understand and dif-
ficult 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 con-
firming known bugs that affected real-world implementa-
tions, and confirming that current implementations do in-
deed behave correctly in multi-threaded environments. 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 for performing formal verification on new synchro-
nisation primitive designs.
ing performant inter-thread and inter-process synchronisa-
tion 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 mu-
tex designs that avoid these early shortcomings, we have
found that their intricacies are hard to understand and dif-
ficult 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 con-
firming known bugs that affected real-world implementa-
tions, and confirming that current implementations do in-
deed behave correctly in multi-threaded environments. 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 for performing formal verification on new synchro-
nisation primitive designs.
