Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
<|reference_start|>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 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.<|reference_end|>
@article{colvin2024practical,
    title={Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on
  Multicore Architectures},
    author={Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter H"ofner, Larissa
  Meinicke and Roger C. Su},
    journal={arXiv preprint arXiv:2407.20559},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.20559},
    primaryClass={cs.LO}
}