Automating Deductive Verification for Weak-Memory Programs (extended version)

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

scope and result

The paper encodes Relaxed Separation Logic (RSL), Fenced Separation Logic (FSL), and FSL++ (together “the RSL logics”) for C11 weak memory into the intermediate verification language Viper, and uses the existing Viper verification backends to check the encoded programs. “Our work enables, for the first time, the (unbounded) verification of C11 programs at the level of abstraction provided by the program logics” (Abstract, p. 1). The user still writes the specifications of the logic: “the only necessary user interaction is in the form of specifications written in the program logic” (Abstract, p. 1). In the paper these are pre/postconditions, loop invariants, and a few other annotations such as location invariants on allocation statements (Sec. 7, p. 16).

technique 1: fractional permissions for non-atomic memory

RSL treats a points-to assertion l ↦ᵏ e as a transferrable resource. “Points-to resources can be split and recombined, but never duplicated or forged” (Section 2, p. 4). Full permission (k=1) permits read and write; a fraction 0<k<1 permits read-only access; Uninit(l) gives exclusive access to an allocated but uninitialised location, which may be written but not read.

Steps from Section 2 (pp. 3–5): (1) assume locations are partitioned into non-atomic locations and atomic locations; (2) annotate allocation with the access mode; (3) represent each C location as a Viper reference l with fields val and init; (4) encode l ↦ᵏ e as acc(l.val, k) && acc(l.init, k) && l.val == e && l.init (Fig. 4); (5) translate allocation to new() plus inhale of the Uninit encoding (full permission to val and init, and !l.init); (6) a read asserts l.init and then reads l.val; a write sets l.val and l.init := true. Viper implicitly checks the field permissions, so these need no explicit encoding, and Viper splits and combines fractions itself, so the equivalence in Fig. 3 need not be encoded.

Inference: in Verus, use a ghost predicate describing ownership and initialisation, and requires/ensures to transfer it between functions or threads. Verus has no Viper inhale/exhale, so one would prove explicit consume/produce lemmas, and fraction arithmetic is then an obligation of the encoding.

technique 2: defunctionalising release/acquire invariants

Release/acquire atomics attach a value-indexed invariant Q to an atomic location. A release write exhales Q[e/V]; an acquire read inhales Q[x/V] for the value x read, and later reads of the same value get nothing. “Multiple acquire reads might read the value written by a single release write operation; RSL prevents ownership of the transferred resources from being obtained (unsoundly) by multiple readers in two ways” (Section 3, p. 7): Acq assertions cannot be duplicated, only split by partitioning the invariant, and the acquire rule adjusts the invariant in Acq so that subsequent reads of the same value obtain no ownership.

Steps (Section 3, pp. 6–9): (1) give a unique index to each syntactically occurring invariant Q, and to each immediate conjunct of these invariants (defunctionalisation); (2) encode Rel(l,Q) as a wildcard permission to a rel field whose value is the index of Q; (3) encode Acq(l,Q) as a wildcard permission to an acq field plus one abstract predicate AcqConjunct(l,i) per conjunct, each with valsRead(l,i) equal to the empty set; (4) on a release write, assert some Rel is held, branch on l.rel, exhale the invariant with e for V, and inhale Init(l); (5) on an acquire read, assert Init(l) and some Acq, havoc the value x, and for each index whose AcqConjunct is held and whose valsRead does not contain x, inhale the indexed invariant for x and add x to valsRead. Init(l) is encoded as a wildcard permission to init, so it is duplicable. Splits other than along top-level conjuncts need a rewrite annotation (App. C, pp. 19–21).

Inference: a Verus model could represent the index and valsRead as ghost state and prove an acquire lemma that consumes a one-shot token. Viper’s wildcard permissions and abstract predicates have no direct Verus counterpart.

technique 3: modalities with multiple heaps for relaxed accesses and fences

FSL and FSL++ use two modalities, “up” (assertion prepared by a release fence to be transferred by a relaxed write) and “down” (assertion obtained by a relaxed read, unusable until an acquire fence). The encoding represents each source location by three Viper references and relates them by axiomatised bijections. “The main challenge in encoding the FSL rules for fences is how to represent the two new modalities.” (Section 4, p. 10)

Steps (Section 4, pp. 9–12): (1) declare a Viper domain with functions up and down, with inverses, so that each source reference r has counterparts up(r) and down(r); (2) add a heap function labelling references with 0 (real), 1 (up), or -1 (down), which tells the verifier the heaps are disjoint; (3) encode an assertion under the up modality by replacing every reference r in the encoded assertion with up(r), and likewise down(r) for the down modality; (4) encode a relaxed write like a release write but with the up version of the invariant, and a relaxed read like an acquire read but with the down version (Fig. 10); (5) encode fencerel(A) as exhale of the encoded A followed by inhale of its up version, which needs the assertion A as an annotation; (6) encode fenceacq by havocing the set of references with some permission in the down heap, inhaling the same permission to the real location, assuming equal values, and exhaling the down permission, per field and predicate; no annotation is needed. Because the mappings are bijective, the last two rules of Fig. 8 (modalities distribute over connectives) need no explicit encoding.

Completeness consequence: fenceacq removes all assertions from under the down modality, which the authors consider no loss in practice (Section 6, p. 14).

Inference: Verus could model these views as ghost snapshots or histories and prove transition lemmas, but it cannot directly recreate Viper’s multiple-heap semantics without an explicit ghost representation.

technique 4: compare-and-swap encoding

The paper states: “Our encoding of the proof rule for CAS operations is somewhat involved; we give a high-level description here, and relegate the details to App. E.” (Section 5, p. 13) FSL++ uses RMWAcq(l,Q) for CAS locations; unlike Acq, it is duplicable and its invariant need not be adjusted after a successful CAS (Sec. 5, p. 12). It is encoded like Acq with wildcard permissions for the AcqConjunct predicates, and the value of field acq (false for RMWAcq) distinguishes the two.

The rule splits the acquired invariant Q[e/V] and the released invariant Q[e'/V] into an overlap T that stays with the location, a part A acquired, and a part P released. Choosing the largest T is “one of the main challenges” (Sec. 5, p. 13). Steps (Section 5, pp. 13–14; App. E, pp. 24–25): (1) assert Init, some RMWAcq, and some Rel, and havoc the value x read; (2) in the case x == e (success), inhale Q[x/V] into an extra “tmp” heap; (3) exhale Q[e'/V], taking each permission preferentially from the tmp heap (this is T) and the rest from the real heap (modes rel, rel_acq) or the up heap (otherwise) (this is P); (4) move the permissions left in the tmp heap (this is A) to the real heap (modes acq, rel_acq) or the down heap (otherwise). If the CAS fails the precondition is preserved (Sec. 5, p. 13); the Fig. 19 encoding has no else branch.

Inference: in Verus, specify CAS with a postcondition split by the returned success Boolean and use ghost state for the observed value and ownership token. The proof must cover both branches, and atomicity remains an assumption of the underlying model.

soundness, incompleteness, and evaluation

The soundness argument is an outline, not a mechanised proof: “We give a brief overview of the soundness argument for our encoding here” (Section 6, p. 14; details in App. F, pp. 26–28). “Soundness means that if the Viper encoding of a program and its specification verifies, then there exists a proof of the program and specification using the RSL logics.” (Section 6, p. 14) It has two steps: (a) the states before and after each encoded statement satisfy invariants (for example, permission to a non-atomic reference’s val field is never held without init); (b) a mapping from Viper states back to RSL assertions turns the initial and final states of each encoded statement into a provable Hoare triple, and Viper’s automatic entailment reasoning coincides with entailments sound in the RSL logics.

Completeness has three sources of incompleteness (Section 6, p. 14): no strengthening of the invariant in a Rel assertion; fenceacq removes all assertions under the down modality; and FSL++ ghost state over custom permission structures (partial commutative monoids) is not possible in Viper. The paper says the last “is the only incompleteness of our encoding arising in practice”.

The evaluation table has 19 rows (including expected-error variants), with program sizes of 6–27 LOC, 0–3 loops, and verification times of 9.57–37.53 seconds (Fig. 13, p. 15). Times are averages of 5 runs on an Intel Core i7-4770 CPU (3.40GHz, 16Gb RAM) running Windows 10 Pro (Section 7, p. 16). For the Facebook Folly reader-writer spinlock, the paper verified five of seven functions directly; the other two “employ code idioms which seem to be beyond the scope of the RSL logics”, and alternative implementations were verified instead (Section 7, p. 16). Those Folly rows are not marked as supported by the front-end prototype in Fig. 13. The Rust ARC original needs a custom permission structure, so two variants with strengthened access modes were verified (Section 7, pp. 15–16). On annotation effort: “our annotation overhead is between one and two orders of magnitude lower than the overhead of existing mechanised proofs” (Section 7, p. 16). The comparison is the “Other Annot.” column (0–3 in the table) against Coq manual proof steps “in addition to pre-post pairs” (84–654 for four examples) in Fig. 13. These are the authors’ counts and claims.

What is proved is correspondence to the encoded logics. The paper names its residual risk: “errors in the encoding or bugs in the verifier could potentially invalidate verification results” (Introduction, p. 2), mitigated by the soundness argument and “the use of a mature verification system”.

techniques for the catalog

• fractional permission encoding: represent separation-logic ownership and initialisation with Viper permissions on val and init fields
• invariant defunctionalisation: replace higher-order atomic invariants with indexed predicates and value-read sets
• multiple-heap modalities: encode relaxed accesses and fences with extra references related by bijections, and move permissions between them
• CAS tmp-heap encoding: compute the overlap of acquired and released invariants by exhaling against an extra heap
• logic-to-Viper soundness map: relate each encoded statement to a source-logic Hoare step

Last edited: 2026-10-17