VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs

TL;DR

The paper addresses how to verify fine-grained concurrent programs in a modular way without relying on the later modality. It introduces a formalization of VeriFast's ghost-code-based logic with atomic spaces and fractional ownership, and proves its soundness. It discusses the trade-offs with Iris and related later-less approaches (Nola, Lilo), clarifying capabilities and limitations. The results support scalable, semi-automated verification of concurrent C/Java/Rust programs and illuminate practical design choices for invariant reasoning without laters.

Abstract

VeriFast is one of the leading tools for semi-automated modular formal program verification. A central feature of VeriFast is its support for higher-order ghost code, which enables its support for expressively specifying fine-grained concurrent modules, without the need for the later modality. We present the first formalization and soundness proof for this aspect of VeriFast's logic, and we compare it both to Iris, a state-of-the-art logic for fine-grained concurrency which features the later modality, as well as to some recent proposals for Iris-like reasoning without the later modality.

Figures (8)

• Figure 1: An example program. $\mathbf{cons}(0)$ allocates a memory cell, initializes it to 0, and returns its address. The $\mathbf{FAA}$ command performs a sequentially consistent atomic fetch-and-add operation. $c_1\,||\, c_2$ is the parallel composition of commands $c_1$ and $c_2$. $*\mathsf{x}$ returns the value stored at address $\mathsf{x}$.
• Figure 2: Syntax of the expressions $e$, instructions $i$, and commands $c$ of the programming language. We assume a set $\mathcal{X}$ of program variable names. $c; c'$ is a shorthand for $\mathbf{let}\ \_ = c\ \mathbf{in}\ c'$, where $\_$ is a designated element of $\mathcal{X}$
• Figure 3: Small-step operational semantics of the programming language
• Figure 4: Syntax of ghost declarations $\mathit{gdecl}$, ghost instructions $I$, inner ghost commands $G$, outer ghost commands $C$ (collectively called ghost commands), and annotated commands $\hat{c}$. Heap chunk assertions and heap chunk update commands are internal; they are not accepted by VeriFast in source code and are introduced here only for the sake of the soundness proof.
• Figure 5: VeriFast proof of the example program. $\mathsf{Nx} \triangleq ()$.

Theorems & Definitions (9)

• theorem 1
• Lemma 1: Soundness of inner ghost command correctness
• proof
• Lemma 2
• proof
• Lemma 3
• proof
• theorem 1
• proof