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

TL;DR

This paper introduces a method to transform interleaving-based correctness proofs into thread-modular proofs by synthesizing ghost variables, enabling efficient and compact verification of concurrent programs.

Contribution

It presents an automatic approach to convert interleaving-based proofs into thread-modular proofs using ghost variables, improving proof efficiency and size.

Findings

Efficient proof generation in practice

Compact proofs compared to baseline

Effective abstraction of irrelevant details

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.