Synthesizing Short-Circuiting Validation of Data Structure Invariants

TL;DR

This paper introduces incremental verification-validation, combining static separation logic analysis with efficient, short-circuiting dynamic validation to verify complex data structure invariants more efficiently and accurately.

Contribution

It presents a novel approach that synthesizes short-circuiting dynamic validation from static proofs, improving efficiency and handling imprecision in static analysis.

Findings

Short-circuiting validation yields asymptotic performance improvements.

The approach maintains low overhead even with incomplete static verification.

Empirical results demonstrate efficiency gains in dynamic validation.

Abstract

This paper presents incremental verification-validation, a novel approach for checking rich data structure invariants expressed as separation logic assertions. Incremental verification-validation combines static verification of separation properties with efficient, short-circuiting dynamic validation of arbitrarily rich data constraints. A data structure invariant checker is an inductive predicate in separation logic with an executable interpretation; a short-circuiting checker is an invariant checker that stops checking whenever it detects at run time that an assertion for some sub-structure has been fully proven statically. At a high level, our approach does two things: it statically proves the separation properties of data structure invariants using a static shape analysis in a standard way but then leverages this proof in a novel manner to synthesize short-circuiting dynamic validation of the data properties. As a consequence, we enable dynamic validation to make up for imprecision in sound static analysis while simultaneously leveraging the static verification to make the remaining dynamic validation efficient. We show empirically that short-circuiting can yield asymptotic improvements in dynamic validation, with low overhead over no validation, even in cases where static verification is incomplete.