Model Checking Futexes
Abstract
The futex Linux system call enables implementing performant
inter-thread synchronization primitives, such as mutexes and
condition variables. However, the futex system call is notoriously
tricky to use correctly. In this paper, 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 synchronization
primitives, and as a template on how to perform formal verification
on new synchronization primitive designs.
inter-thread synchronization primitives, such as mutexes and
condition variables. However, the futex system call is notoriously
tricky to use correctly. In this paper, 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 synchronization
primitives, and as a template on how to perform formal verification
on new synchronization primitive designs.
