Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su

TL;DR

This work targets the practical verification of the CLH lock used in the seL4 microkernel on multicore architectures under weak memory models. It adopts Jones' rely/guarantee reasoning and encodes the verification in Isabelle/HOL to produce a machine-checked, composite proof that covers both inter-thread communication and micro-parallelism. The key contributions include a detailed queued lock specification, a complete CLH-seL4 implementation verification with extensive auxiliary invariants, and an explicit analysis of weak memory effects and necessary ordering constraints. The results demonstrate mutual exclusion and progress properties under Arm-like memories, providing confidence in the lock's correctness for real multicore deployment of seL4.

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.

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

TL;DR

This work targets the practical verification of the CLH lock used in the seL4 microkernel on multicore architectures under weak memory models. It adopts Jones' rely/guarantee reasoning and encodes the verification in Isabelle/HOL to produce a machine-checked, composite proof that covers both inter-thread communication and micro-parallelism. The key contributions include a detailed queued lock specification, a complete CLH-seL4 implementation verification with extensive auxiliary invariants, and an explicit analysis of weak memory effects and necessary ordering constraints. The results demonstrate mutual exclusion and progress properties under Arm-like memories, providing confidence in the lock's correctness for real multicore deployment of seL4.

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.
Paper Structure (32 sections, 7 theorems, 29 equations, 4 figures)

This paper contains 32 sections, 7 theorems, 29 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Rely/Guarantee Reasoning
  3. Inference rules
  4. Invariants
  5. Specification of Locks in Rely/Guarantee
  6. Properties of a generic lock
  7. Queued lock
  8. Functional Correctness of CLH-seL4
  9. CLH-seL4 implementation
  10. Types and initialisation.
  11. Acquire.
  12. Release.
  13. Efficiency.
  14. Auxiliary variables, invariants and intermediate states of CLH-seL4
  15. Types, initialisation, and auxiliaries.
  16. ...and 17 more sections

Key Result

theorem 1

Figures (4)

  • Figure 1: Rely/guarantee inference rules adapted from SoundnessRGRGinIsabelle.
  • Figure 2: Rely/guarantee specification of the queued lock
  • Figure 3: Excerpt of the seL4 CLH implementation (focussing on the logic) CLH-seL4.
  • Figure 4: seL4 CLH proof structure

Theorems & Definitions (7)

  • theorem 1: Acquire
  • theorem 2: Release
  • theorem 3: Locking system
  • theorem 4: Parallelization of the while loop in acquire
  • theorem 5: Acquire under ${{\normalfont \textsc{arm}}}\xspace$
  • theorem 6: Release under ${{\normalfont \textsc{arm}}}\xspace$
  • theorem 7: Correctness of CLH under ${{\normalfont \textsc{arm}}}\xspace$