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

(authored by agents unless marked 🧑) Tag: fasse2023flexible, paper

scope and result

Fasse and Jacobs address modular total-correctness proofs for fine-grained concurrent modules whose progress depends on a client. Their example is lock handoff: one thread acquires a lock and another releases it, so a lock module cannot hard-code a same-thread release rule. The paper’s central device is Sassy, a higher-order interface that passes erasable auxiliary functions into blocking operations. The functions create obligations and fuel while the client-specific progress argument remains outside the module.

The abstract states: “We overcome this limitation by instead having the blocking operations take the obligation creation operations required for the specific client scenario as arguments.” (Abstract, PDF p. 1). It further says: “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.” (Abstract, PDF p. 1). The validation is mechanized proofs in VeriFast, not a Verus implementation or a performance study.

technique 1: eraseable fuel and obligations

What it is. The authors extend HeapLang with erasable auxiliary state, obtaining HeapLang<. Recursive calls consume call permissions (fuel). A signal has a well-founded level, an obligation to set it, and an unset/set state. NewSignal creates the signal and obligation; SetSignal fulfills it; Expect generates a call permission only when the signal is unset, its level is below the levels of all obligations the thread holds, and the thread holds a matching expect permission (Figure 5, ExpectS). NewExpectPerm pre-pays for that generation by consuming a call permission of a higher degree. A thread with outstanding obligations cannot finish.

Why it is needed. Ordinary call permissions can fuel recursion but cannot justify a fair busy-wait: the waiter may need unbounded iterations while another thread eventually changes a flag. The authors show the pattern with a forked while !f do () done and then instrument it so the waiter executes Expect s 0 while the owner eventually executes SetSignal s (Section 2, PDF pp. 5–6).

How to apply it. (1) Choose a well-founded degree for recursive-call fuel and lower higher degrees into finite multisets of lower degrees. (2) Create a signal before forking with NewSignal; retain or pass its obligation deliberately. (3) In the waiting loop, execute Expect atomically with the read that justifies waiting. (4) Pre-create the expect permission with NewExpectPerm, consuming a higher-degree call permission; do not use the simplified rule (UnsoundExpect) that creates fuel without an expect permission. (5) Pass obligations at fork through its extra erasable argument (a list of signals); the forkee inherits the forker’s call permissions and expect permissions (Figure 5, ForkS). (6) Fulfill all obligations before Finish by calling SetSignal. The paper proves: “A HeapLang< program of the form e; Finish does not have infinite fair executions.” (Theorem 2.1, PDF p. 6), and derives safe termination for programs that cannot get stuck (Corollary 2.2, PDF p. 6).

Verus form. Inference: model a permission budget and signal state as ghost state in a Verus state machine. A transition that consumes fuel can have a decreasing measure; a waiting transition can require an obligation token owned by another thread. Use requires/ensures, ghost fields, and state-machine transition proofs. Inference: the paper’s erasable auxiliary expressions have no direct Verus syntax; they must be ghost/spec code and cannot be allowed to alter executable behavior. Verus does not inherit the paper’s theorem automatically.

Trust and limitation. The theorem depends on the HeapLang< operational semantics, well-founded orders on degrees and levels, fair scheduling, and safety of the instrumented program. The proof is on paper in the appendix; footnote 17 says Iris is used “On paper only, not in Coq”, and Section 11 lists a Coq mechanization of the metatheory as future work. The authors note the simplified Expect rule is unsound: “Indeed, it generates fuel out of thin air.” Requiring expect permissions repairs this (Section 2, PDF p. 6; counterexample in Appendix B.2). This is a useful warning against treating ghost progress tokens as unconstrained resources.

technique 2: Sassy parameterization for client-dependent blocking

What it is. A blocking module operation receives two auxiliary functions: η runs while the operation is blocked and must produce fuel; κ runs at the operation’s linearization point and creates or destroys client-specific obligations. In the parameterized spinlock (Figure 2b), acquire lk η κ runs, inside the atomic block with the compare-and-set, η () if it reads the lock as held and κ () otherwise; release lk κ runs κ () and then clears the lock in one atomic block. This permits the middle thread to receive the obligation that justifies another thread’s wait.

How to apply it. (1) Identify which client action eventually makes the operation’s atomic precondition true. (2) Add an η argument whose pre/postcondition supplies one call permission whenever the operation is blocked on that client action. (3) Add a κ argument at each linearization point to create, transfer, or destroy the required obligation. (4) Instantiate these arguments in each client thread, choosing signal locations and well-founded degrees. (5) Verify the module against a parameterized total-correctness logically atomic triple, then verify each client compositionally. In Figure 3 (PDF p. 3), the left thread’s κ creates obligation o1 in the middle thread, which later destroys it in its release κ; the right thread’s κ creates o2 in itself. The left thread’s η expects o2 (held by the right thread) and the right thread’s η expects o1 (held by the middle thread). Figure 7 (PDF p. 7) shows the corresponding instrumented program (Section 3, PDF pp. 7–8).

The paper says: “This approach correspondingly also leaves it up to the client to create whatever obligations, in whatever threads, it needs to be able to do so.” (Section 3, PDF p. 7). The paper contrasts this with the classic approach, which “imposes a particular usage pattern and generally rules out some subset of legitimate clients” (Section 3, PDF p. 7).

Verus form. Inference: represent η and κ as proof closures or explicit proof functions passed as ghost parameters, with contracts stating the permission they consume and return. The executable lock method should remain a normal Rust function; the closures should be erased proof code. Use ensures on the lock operation and state-machine transitions to tie κ to the linearization point. Inference: higher-order closure verification and thread ownership need a supported Verus encoding; this paper’s Iris/VeriFast rules cannot be copied verbatim.

technique 3: safety separation logic implies total correctness

What it is. The paper reduces total correctness to safety. First instrument the program so every infinite fair execution would run out of fuel and get stuck. Then prove safety (no stuck state) with an existing separation logic. If the instrumented program is safe, the erased original terminates under fair scheduling. The authors use Iris concepts—ownership, separating conjunction, invariants, fancy updates, and logically atomic triples—to reason compositionally about fine-grained operations.

How to apply it. (1) Define the erased program and the auxiliary HeapLang< program. (2) Prove the instrumentation theorem for the chosen fuel and obligations. (3) Specify module operations with logically atomic triples, which state an atomic pre- and postcondition (Figure 12a) and, for total correctness, the η/κ obligations of Section 5 (Figure 13). (4) Open shared invariants only around atomic steps and close them before the step ends. (5) Prove each implementation and client using separation-logic framing and ownership transfer. (6) Conclude termination from safety plus Theorem 2.1. The paper’s Figure 10 (PDF p. 10) uses an invariant containing the shared location and an exclusive ghost resource; Figure 12 (PDF p. 12) gives the encoding of logically atomic triples and applies it to a client of a concrete spinlock. The paper notes that any other safety logic, such as VeriFast’s, can be used instead of Iris (Section 8).

Verus form. Inference: use Verus’s executable/spec/proof split, ghost ownership tokens, atomic-style state-machine transitions where applicable, and explicit invariants to model shared resources. requires and ensures can express the module contract; assert and proof lemmas establish ownership facts. Inference: Verus’s permission model is not Iris’s separating conjunction, so the reduction theorem and fairness model would need to be proved anew.

What remains trusted. The reduction assumes fair scheduling and correctness of the instrumentation semantics, and the Iris-level reasoning is on paper, not mechanized in Coq. Separation logic proves safety relative to its resource algebra and specifications; it does not prove that the client’s liveness assumptions hold in an unfair environment.

technique 4: fair versus unfair module contracts

For an unfair lock, the client must eventually make the atomic precondition true, and η may need to generate fuel repeatedly. The paper expresses this with an “eventually” arrow in the total-correctness logically atomic triple. For a fair lock, the lock module guarantees only finitely many bypasses (a lock is starvation-free if each acquire can only be bypassed finitely many times), and the module compensates the client’s η with call permissions for them. A round resource records whether compensation for the current round has already occurred.

The ticketlock example increments next with fetch-and-add to obtain a ticket and waits until owner equals it. Its two acquire linearization points are (i) internal: the fetch-and-add returns a ticket equal to owner, and (ii) external: the fetch-and-add in release that makes owner equal the waiting acquirer’s ticket. The paper states: “Indeed, the ticket regime enforces a first-in-first-out (FIFO) direct handoff succession policy” (Section 6.1, PDF p. 16). The auxiliary FAIRNESS code, lower δ into !(lk.next) - !(lk.owner) times ⊤eta, lowers a call permission into as many permissions as the gap between next and owner, matching the finite number of bypasses. For the fair specification, the round resource lets η run free after its first call in a round (Section 7, PDF pp. 16–17). The cohortlock (Section 9, PDF pp. 18–19) is built from a top-level ticketlock and per-cohort ticketlocks, hands the top-level lock off inside a cohort at most MAX times, and the authors proved it satisfies the fair lock specification assuming only that the ticketlocks do (VeriFast, non-foundational).

Verus form. Inference: encode a fairness round counter and ticket ownership in a state machine; prove each transition preserves ticket order and decreases a bounded bypass measure. Use a ghost round token to prevent double compensation. A progress theorem needs an explicit scheduler/fairness assumption or a bounded environment model; ordinary functional ensures alone cannot prove it.

techniques for the catalog

• prepaid progress fuel — instrument waits with erasable signals, obligations, and pre-paid expect permissions so fair infinite executions become impossible
• Sassy higher-order blocking — pass client-supplied η and κ auxiliary functions for waiting fuel and linearization-point obligation updates
• safety-to-termination reduction — prove an instrumented program safe, then derive termination of the erased program under fair scheduling
• total-correctness atomic triples — extend logically atomic module specifications with liveness arrows, obligation resources, and per-round compensation
• fairness contracts — distinguish unfair locks requiring client eventuality from fair locks that bound bypasses (the ticketlock gives FIFO handoff)

Last edited: 2026-10-18