A flexible specification approach for verifying total correctness of fine-grained concurrent modules

TL;DR

This work tackles modular verification of total correctness for fine-grained concurrent modules by removing the rigid obligation-creation constraint in standard proofs. It introduces Sassy, a higher-order specification approach where blocking operations receive client-specific auxiliary code ($\eta$ and $\kappa$) that generates fuel and manages progress, enabling non-standard handoffs across threads. The authors combine a terminating language Heap-Lang< with Ghost Signals to prepaid fuel, and they build modular proofs using Iris’s safety framework to establish termination under fair scheduling for both unfair and fair locking schemes, including spinlock, ticketlock, and cohortlock. The methodology supports data abstraction and modular reasoning about progress, validated by machine-checked proofs in VeriFast and related tooling, illustrating practical applicability to complex lock hierarchies and NUMA-aware designs. This work advances modular termination verification for blocking concurrency and provides a flexible, client-driven specification pattern with potential for broader tool support and mechanized proofs.

Abstract

A well-established approach to proving progress properties such as deadlock-freedom and termination is to associate obligations with threads. For example, in most existing work the proof rule for lock acquisition prescribes a standard usage protocol by burdening the acquiring thread with an obligation to release the lock. The fact that the obligation creation is hardcoded into the acquire operation, however, rules out non-standard clients e.g. where the release happens in a different thread. We overcome this limitation by instead having the blocking operations take the obligation creation operations required for the specific client scenario as arguments. We dub this simple instance of higher-order programming with auxiliary code Sassy. To illustrate Sassy, we extend HeapLang, a simple, higher-order, concurrent programming language with erasable code and state. The resulting language gets stuck if no progress is made. Consequently, we can apply standard safety separation logic to compositionally reason about termination in a fine-grained concurrent setting. We validated Sassy by developing (non-foundational) machine-checked proofs of representative locks -- an unfair Spinlock (competitive succession), a fair Ticketlock (direct handoff succession) and the hierarchically constructed Cohortlock that is starvation-free if the underlying locks are starvation-free -- against our specifications using an encoding of the approach in the VeriFast program verifier for C and Java.

Figures (15)

• Figure 1: The lock handoff between the left and middle thread is challenging for the modular verification of progress. This example reflects the key challenge also encountered when verifying a starvation-free cohortlock. Here, we simplify the handoff by "synchronizing" via the exit statement, guarded by the dereference () of flag initialized to true (not shown).
• Figure 2: Spinlock implementation with two approaches to obligation-handling expressed as auxiliary (pseudo) code. The angle brackets indicate the atomic execution of the contained expression to associate auxiliary code with the two cases of (compare-and-set). If $\mathop{!} x = y$, assigns $y$ to $x$ and return true. Otherwise false is returned, leaving $x$ unchanged.
• Figure 3: The pieces of auxiliary code passed to and encapsulate the client-dependent part of the progress proof: ${\color{myghostcode}\kappa}\xspace$ is executed at the point of lock acquisition/release; ${\color{myghostcode}\eta}\xspace$ justifies 's blocking. The left thread's blocking is justified by obligation o2 held by the right thread; the right thread's blocking is justified by obligation o1 held by the middle thread. Threads must destroy their obligations before they finish.
• Figure 4: Syntax of Heap-Lang<. Differences to Heap-Lang are highlighted in blue and are introduced in Section \ref{['sec:overview']}. We write $\lambda \mathit{x}. e \triangleq {\boldsymbol{\mu}_{\texttt{\bfseries e}}} {} \mathit{x}.\,e$, $\lambda . e \triangleq {\boldsymbol{\mu}_{\texttt{\bfseries e}}} {} {}.\,e$, and $\operatorname{\texttt{\bfseries ref}}~e \triangleq \texttt{\bfseries AllocN} 1 eme$.
• Figure 5: Heap-Lang< operational semantics. $\cyrell \prec O$ means $\forall (s, \cyrell') \in O.\;\cyrell < \cyrell'$.

Theorems & Definitions (4)

• theorem 1: Absence of infinite fair executions
• proof
• corollary 1: Safe termination
• proof