Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
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.
Cite
@article{arxiv.2407.20559,
title = {Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures},
author = {Robert J. Colvin and Ian J. Hayes and Scott Heiner and Peter Höfner and Larissa Meinicke and Roger C. Su},
journal= {arXiv preprint arXiv:2407.20559},
year = {2024}
}