Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)

Frank Schüssele, Matthias Zumkeller, Miriam Lagunes-Rochin, Dominik Klumpp

TL;DR

The paper tackles the exponential blow-up of interleaving-based correctness proofs for concurrent programs by automatically converting them into compact thread-modular proofs in the style of Owicki-Gries. It introduces empires as an abstract representation of interleaving information and shows how ghost variables can encode this information to enable valid OG annotations. Through symbolic execution, it builds saturated empires that group control states into regions and territories, yielding smaller, more modular proofs. A focused variant distributes invariant-domain information to reduce annotation size further. Empirical evaluation demonstrates substantial gains in annotation compactness and validation efficiency, suggesting practical applicability for certifying verifier soundness and increasing trust in verification results.

Abstract

Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact correctness proofs for concurrent programs is challenging, as the correctness arguments may depend on the particular interleaving, which can lead to exponential explosion. We present an approach that converts an interleaving-based correctness proof, as generated by many algorithmic verifiers, into a thread-modular correctness proof in the style of Owicki and Gries. We automatically synthesize ghost variables that capture the relevant interleaving information, and abstract away irrelevant details. Our evaluation shows that the approach is efficient in practice and generates compact proofs, compared to a baseline.

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)

TL;DR

The paper tackles the exponential blow-up of interleaving-based correctness proofs for concurrent programs by automatically converting them into compact thread-modular proofs in the style of Owicki-Gries. It introduces empires as an abstract representation of interleaving information and shows how ghost variables can encode this information to enable valid OG annotations. Through symbolic execution, it builds saturated empires that group control states into regions and territories, yielding smaller, more modular proofs. A focused variant distributes invariant-domain information to reduce annotation size further. Empirical evaluation demonstrates substantial gains in annotation compactness and validation efficiency, suggesting practical applicability for certifying verifier soundness and increasing trust in verification results.

Abstract

Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact correctness proofs for concurrent programs is challenging, as the correctness arguments may depend on the particular interleaving, which can lead to exponential explosion. We present an approach that converts an interleaving-based correctness proof, as generated by many algorithmic verifiers, into a thread-modular correctness proof in the style of Owicki and Gries. We automatically synthesize ghost variables that capture the relevant interleaving information, and abstract away irrelevant details. Our evaluation shows that the approach is efficient in practice and generates compact proofs, compared to a baseline.

Paper Structure

This paper contains 25 sections, 8 theorems, 18 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Example.
  3. Related Work.
  4. Contributions and Roadmap.
  5. Background: Concurrent Programs
  6. Concurrent Control Flow.
  7. Correctness.
  8. Interleaving-Based vs. Thread-Modular Correctness Proofs
  9. Interleaving-Based Correctness Proofs
  10. Owicki-Gries Annotations
  11. Empires: An Abstract Representation of Interleaving Information
  12. Constructing Empires by Symbolic Execution
  13. A Straightforward Approach to Constructing Empires
  14. Constructing Larger Regions
  15. Focus: Modular and Succinct Owicki-Gries Annotations
  16. ...and 10 more sections

Key Result

proposition 1

If there exists a safe invariant domain for $\mathcal{P}$, then $\mathcal{P}$ is correct.

Figures (10)

  • Figure 1: Example Program
  • Figure 2: Petri program corresponding to \ref{['fig:example-pseudocode']}. Transitions are drawn as black boxes, places as circles. Double circles indicate error places. Arrows represent the flow relation. Initially, only $p_0$ has a token (black dot).
  • Figure 3: Owicki-Gries annotation for the program in \ref{['fig:petri-program']}, with $\rho(\mathghost_1)=\rho(\mathghost_2)=\bot$. The transitions $t$ are labeled with the ghost updates $\gamma(t)$ (in green). Each place $p$ is annotated (in purple) with the formula $\omega(p)$.
  • Figure 4: Excerpt of the naïve Owicki-Gries annotation for the Petri program from \ref{['fig:petri-program']}.
  • Figure 5: A valid empire for the Petri program in \ref{['fig:petri-program']}.
  • ...and 5 more figures

Theorems & Definitions (30)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • proposition 1
  • definition 7
  • definition 8
  • definition 9
  • ...and 20 more