Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures

Developers of low-level systems code providing core functionality for operating systems and kernels must address micro-architectural features of modern multicore processors, including and especially pipelined out-of-order execution of the code as written. The effects of out-of-order execution are typically summarised by a weak memory model, a term which includes further complicating factors that may be introduced by compiler optimisations. In many cases, the nondeterminism inherent in weak memory models can be expressed as micro-parallelism, i.e., parallelism within threads and not just between them. Fortunately Jones’ rely/guarantee reasoning provides a compositional method for verification of shared-variable concurrency, whether that be in terms of communication between top-level threads or micro-parallelism within threads. In this paper we provide an in-depth specification and verification of the lock algorithm used in the seL4 microkernel, using rely/guarantee to handle both inter-thread communication and micro-parallelism introduced by weak memory models. The proof is machine-checked in Isabelle/HOL, building on an existing theory for rely/guarantee reasoning, extended with rules specialised for data type invariants, spin loops, and nested parallelism.