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

TL;DR

This paper presents a formal verification of a lock algorithm in the seL4 microkernel, addressing the challenges posed by modern multicore architectures and weak memory models using rely/guarantee reasoning.

Contribution

It applies rely/guarantee reasoning to verify a lock in seL4, accounting for micro-parallelism and weak memory effects, which is a novel approach in this context.

Findings

Successful verification of the seL4 lock algorithm.

Demonstrates the effectiveness of rely/guarantee reasoning for weak memory models.

Provides a framework for verifying low-level concurrent algorithms.

Abstract

Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A particular feature is pipelined "out-of-order execution" of the code as written, the effects of which are typically summarised as 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 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 verification of the lock algorithm used in the seL4 microkernel, using rely/guarantee to handle both interthread communication as well as micro-parallelism introduced by weak memory models.