Embedding Hindsight Reasoning in Separation Logic

TL;DR

This paper introduces temporal interpolation as a novel proof principle for verifying linearizability in concurrent data structures using hindsight reasoning within separation logic, simplifying proofs and revealing previously unnoticed errors.

Contribution

It presents a new proof technique integrating hindsight reasoning into separation logic, enabling formal verification of complex concurrent data structures like the LO-tree.

Findings

Verified linearizability of the LO-tree and RDCSS

First formal proof of the LO-tree data structure

Discovered an unknown bug and corrected an informal proof

Abstract

Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal reasoning offers an easy-to-use alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. To hindsight theory, our work brings the formal rigor and proof machinery of concurrent program logics. We substantiate the usefulness of our development by verifying the linearizability of the Logical Ordering (LO-)tree and RDCSS. Both of these involve complex proof arguments due to future-dependent linearization points. The LO-tree additionally features complex structure overlays. Our proof of the LO-tree is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.