Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Impredicative Concurrent Abstract Predicates

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

Page numbers below are the printed LNCS page numbers (ESOP 2014, pp. 149–168; PDF page 1 is printed p. 149).

result

Svendsen and Birkedal introduce iCAP, a higher-order concurrent separation logic for a subset of C#. “We present impredicative concurrent abstract predicates – iCAP – a program logic for modular reasoning about concurrent, higher-order, reentrant, imperative code.” (Abstract, p. 149) Its distinctive mechanism is a protocol parameterized by arbitrary predicates, including predicates that refer back to protocols. The paper sketches three examples: a spin-lock (Section 2.1), a reentrant event loop (Section 2.2), and a concurrent bag implemented with helping (Section 2.3). The paper itself gives only sketches of these verifications. Full proofs and the formal proof system are in an appendix and a technical report that are not part of the paper text (Sections 1, 2.1, 2.3, 4). The paper reports no tool or mechanization; implementing a Coq-based verification tool is listed as future work (Section 5).

Inference: iCAP’s proof pattern maps to Verus transition systems and ghost state, but the mapping is conceptual. Verus does not implement iCAP’s separation-logic semantics or impredicative quantification.

technique 1: abstract predicates for shared resources

Hide representation behind abstract predicates and expose a Hoare-style module specification. For a lock, the paper quantifies a resource invariant R and gives triples for new Lock, Acquire and Release. The specification requires R to be stable, and states that isLock(R, x) is duplicable (valid(∀x : Val. isLock(R, x) ⇔ isLock(R, x) ∗ isLock(R, x))) and that isLock and locked are stable (Section 2.1, p. 152). isLock(R, x) expresses that x is a lock protecting the resource invariant R, and locked(R, x) expresses that the lock x is indeed locked (Section 1, p. 150). Acquire grants ownership of R and Release requires the client to give R up (Section 1, p. 150).

The isLock and locked predicates are existentially quantified (they support internal sharing), and R is universally quantified (it supports external sharing). Because isLock is parametric in R, clients can use it inside resource invariants, which the paper says is not possible if one asserts only a non-parametric isLockR for each R (Section 2.1, p. 153).

To verify an implementation: the paper says “To verify an implementation against this specification we have to provide concrete instantiations for the parametric isLock and locked predicates and prove that the implementation satisfies the specification with these concrete instantiations.” (Section 2.1, p. 153) The concrete proof for the spin-lock “follows the structure of the original CAP proof of a spin-lock” and is given in the appendix (Section 2.1, p. 154).

Inference: in Verus, represent the abstract resource as a ghost state-machine invariant and expose methods whose requires and ensures describe ownership and allowed transitions. Rust borrow rules provide some ownership discipline, but the protocol invariant still needs explicit proof.

technique 2: impredicative protocols

iCAP extends separation logic with shared regions. A protocol “consists of a labelled transition system, labelled with action identifiers, and an assertion for each abstract state in the transition system that describes the resources the shared region must own in the given state.” To change a region’s state from s1 to s2 a client must own permissions to labels along a path from s1 to s2 (Section 2.1, p. 153). The paper emphasizes: “A key feature of iCAP is that it supports full higher-order quantification over assertions in specifications.” (Section 2.1, p. 152)

Spin-lock instance (Section 2.1, pp. 153–154): two abstract states, locked (L) and unlocked (U), with transitions labelled Acq (U to L) and Rel (L to U). In state L the region owns the locked field containing true. In state U it owns the locked field containing false, the client’s resource invariant R, and the full permission to the Rel action. A client that locks the lock therefore takes R and the exclusive Rel permission, so only the lock holder can unlock. isLock(R, x) asserts that some region n exists, governed by this protocol and in state L or U, together with non-exclusive permission to Acq. The authors write: “Note that this spin-lock protocol is parameterized over an arbitrary resource invariant R provided by the client and is thus an impredicative protocol.” (Section 2.1, p. 154)

Guarded recursion: the model defines the space of protocols by guarded recursion in the topos of trees, and the logic includes a “later” connective used to guard recursive occurrences (Sections 2.2 and 3, pp. 156, 161–164).

Inference: a reusable recipe is to define protocol states and labelled transitions, attach a resource assertion to each state, parameterize the protocol by the client predicate, allocate a region carrying the protocol, and open the region only around one atomic operation (the paper says opening a region once per atomic instruction is the sound discipline, Section 2.3, pp. 159–160). Verus’s state_machine and invariant constructs can encode states, transitions, and a ghost representation predicate. The recursive higher-order quantification itself does not carry over; write a first-order ghost predicate and prove every transition preserves it.

technique 3: recursive event-loop abstraction

The abstract specification of a single-threaded event loop is ∃eloop : Val → Prop with triples for new EventLoop, loop, signal and when; when(f) requires the nested triple f → {eloop(x)}{eloop(x)}, so event handlers may use the loop resource to emit events (Section 2.2, p. 155). The paper notes this is “in a sense 
 a very weak specification, in that it only allows us to reason about memory safety of our clients”, but verifying an implementation against it in the presence of reentrancy is highly non-trivial (Section 2.2, p. 155).

The concrete eloop is defined by guarded recursion (fix, with the “later” guard on the handler specifications): it owns the signals and handlers fields and the two sets, and asserts that all registered handlers satisfy the handler specification one step later (Section 2.2, p. 156). The paper says eloop is not definable by induction, nor by Tarski’s fixed-point theorem, because nested Hoare triples are contravariant in the precondition and covariant in the postcondition (p. 156). The paper says that once the resource is defined, “the verification is routine” (p. 156); it does not spell out the proof steps.

Multi-threaded variant (Section 2.2, pp. 156–157): add the axiom valid(∀x : Val. eloop(x) ⇔ eloop(x) ∗ eloop(x)). The implementation adds a lock protecting the sets, and eloop is defined in terms of the abstract isLock, whose resource invariant mentions eloop. Guardedness across the abstraction boundary is enforced automatically in iCAP. The paper concludes: “These two event loop examples illustrate how we can reason about recursive abstractions in iCAP and also exemplify the power of impredicative protocols.” (Section 2.2, p. 157)

Inference: in Verus, model callbacks as ghost identifiers with a spec function describing permitted effects, and use a transition system to connect dispatch to callback transitions. Dynamic function pointers and arbitrary reentrancy require explicit modeling assumptions.

technique 4: helping with a modular concurrent bag

Specification pattern (Section 2.3, pp. 158–159, from the authors’ earlier HOCAP work): keep a phantom field (cont for the bag) holding the abstract state, with the data structure owning half and clients sharing the other half. Each method’s specification is parameterized by a client-provided view shift that performs the abstract update (for Push, from X to X âˆȘ {y}) and by client predicates P and Q (“synchronization pre- and postconditions”). The view shift is indexed by RId\{n} so the client cannot open the bag’s region n. The paper states: “Since updating the phantom field requires both halves, this forces clients to prove that the abstract effects of any call to the Push method satisfies any protocols clients may have imposed.” (p. 159) Figure 1 gives the specification of new Bag and Push only; Pop is “similar and omitted”.

Helping protocol (Section 2.3, pp. 160–161): a pusher may offer its push on a side channel. A popper may accept the offer and thereby complete the pusher’s operation. The offer protocol Toffer has states pending, accepted, ack’ed and revoked, with actions Accept, Ack and Revoke. In pending, the region owns P(b, y) and the pusher’s push view shift. In accepted it owns Q(b, y). To accept an offer the popper must perform the pusher’s push view shift, so “the offer protocol “transfers” the pusher’s view shift to the popper”. The paper says the combination of view shifts and impredicative protocols is what makes this verification possible.

The paper only sketches this verification and defers the full proof to the technical report (pp. 158, 160, 161). The paper states: “We now sketch how iCAP can be used to verify that a sophisticated fine-grained concurrent implementation using cooperation actually meets the modular bag specification.” (Section 2.3, p. 160)

Inference: a Verus encoding would use a ghost bag model, a client-supplied update at the atomic commit step, offer-state transitions, and proof lemmas connecting concrete atomics to abstract effects. Linearization points (the paper does not use that term) and interference assumptions must be explicit.

soundness, evidence, and limits

The paper’s evidence is a soundness argument plus sketched examples, not a benchmark count. “The presence of these features means that soundness of iCAP is non-trivial. Thus a key technical contribution of our work is our soundness proof of iCAP, which uses a novel model construction that we explain in Section 3” (Section 1.1, p. 152). Section 3 defines the model in the topos of trees, using the Views framework, over a concrete semantics that is a subset of C# with an interleaving semantics. The stated result (Section 4, p. 166) is that a derivable triple implies safe(s, ...); the soundness proof itself is in the technical report, not in this paper. Inference: the trusted base includes the model, its proof in the report, and the per-example proofs, also in the report and appendix. Inference: it does not verify arbitrary Rust, compiler behavior, scheduler fairness, or a product’s specification.

techniques for the catalog

  • abstract resource predicates: hide shared representation behind predicates and prove implementations against modular Hoare triples
  • impredicative protocols: parameterize region transitions by arbitrary predicates, including guarded recursive references
  • recursive event-loop specs: let callback contracts refer to the loop resource and define the resource by guarded recursion
  • helping-based modular ADTs: connect fine-grained cooperative operations to abstract effects through protocol transitions and transferred view shifts
  • semantic soundness model: establish safety of the proof logic with a guarded-recursive model construction and operational semantics

Last edited: