CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer

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

what the paper proves and builds

CleanQ is a formal model and C interface for descriptor-ring data transfer. The paper’s goal is a sound specification that clients and implementations can share, rather than a verified implementation. It states: “CleanQ is a specification and not an implementation, thus leaving orthogonal issues like metadata, setup, and additional semantics to the implementation while adhering to a single common model for data transfer.” (Section 2.3, PDF p. 3). The authors model ownership transfer, refine the model to FIFO lists and then to a hardware ring, formalize state relations and operations in Isabelle/HOL, and implement modules for network, storage, inter-process communication, debugging, and protocol stacking.

technique 1: ownership as the abstract transfer model

what it is and when to use it

The primitive is exclusive ownership of buffers by communicating entities. The model has owner sets OA and OB, and transfer queues QAB and QBA; the allowed cycle is OA → QAB → OB → QBA → OA. The four required properties are: one owner at most, exclusive use by the owner, knowledge of ownership, and transferable ownership (Section 3, PDF p. 3). The paper derives disjointness of all four sets and conservation of the universe of registered buffers: “A thing has at most one owner.” and “A thing has exclusive use of it.” (Section 3, PDF p. 3). It also states: “One final invariant completes the model, and expresses that buffers are never lost, or invented out of thin air” (Section 3, PDF p. 4).

how to apply it

1. Define the communicating entities and the set of buffers registered with the queue (Section 3).
2. Represent each buffer in exactly one owner or transfer set; assert pairwise disjointness and that their union is constant (Section 3, PDF p. 4).
3. Define register and deregister as changes to the abstract universe, and define enqueue as removing a buffer from the caller’s owner set and putting it in the outgoing queue; define dequeue as the corresponding move into the caller’s owner set (Section 3, PDF pp. 4–5).
4. Require an implementation to make the ownership transition occur at the specified API operation. The paper says: “Any implementation of A.enqueue() must cause A to relinquish ownership of X and that of A.dequeue() cause A to take ownership of Y.” (Section 3.1, PDF p. 4).

Verus form

Inference: Model the queue state as a ghost state machine with sets or finite maps for owner and in-flight membership, and expose transitions for register, enqueue, and dequeue. Use requires and ensures on executable Rust methods, and proof functions to establish disjointness and conservation. Verus’s state-machine APIs and ghost fields are the closest available constructs in the local Verus guide; the Isabelle set-theoretic formalization does not carry over as Isabelle syntax. Keep buffer payload code executable and keep ownership bookkeeping ghost. Do not claim that a Verus proof validates hardware behavior unless the hardware transition and memory model are also modeled.

evidence, assumptions, limits

The formal evidence is Isabelle/HOL state-relation, noninterference, and refinement proofs; the paper says: “We have formalized these, also in Isabelle/HOL, including noninterference and refinement proofs for all abstract levels.” (Section 3.3, PDF p. 5). The model assumes ownership is the right abstraction and that registration establishes a fixed universe. It does not prove a complete OS, a C implementation, or external hardware. The paper explicitly says its goal is not a full-stack verified system (Section 2.3, PDF p. 3).

technique 2: stepwise refinement to a real descriptor ring

what it is and when to use it

Refinement connects an abstract ownership specification to an implementation with concrete pointers. The paper first refines sets to FIFO lists (LAB, LBA) and then lists to the Intel i82599 ring (head, tail, and done). Figure 3 shows A.enqueue(X) as set insertion, list append, and pointer update. Use this when the implementation has a low-level representation whose correctness must be related to a simpler abstract contract.

how to apply it

1. Choose a concrete hardware ring and identify which descriptor interval denotes each abstract queue. For i82599, descriptors from head up to tail represent QAB; done identifies completed descriptors (Section 3.1, PDF p. 4).
2. Define a state relation: each abstract set equals the elements of the corresponding list, and each list equals the descriptors in its ring interval (Section 3.2, PDF p. 5).
3. Refine each abstract operation in stages. Append X to the abstract list, then show that the concrete atomic pointer increment has the same effect and preserves guards against head overtaking tail (Sections 3.1–3.2).
4. Prove that every concrete step simulates an abstract step and that invariants survive interference. The paper calls this “a stepwise refinement of A.enqueue(X) from the abstract set-based model described so far, via an intermediate model where queues become lists (establishing FIFO order), to the ring buffer model just described.” (Section 3.2, PDF p. 5).

Verus form

Inference: Encode the abstract state and concrete ring in ghost fields, define a view function from ring indices to the abstract sequence, and prove a lemma that each pointer update preserves the view relation. Use invariant declarations inside loops (the construct is a declaration, not a function call), requires/ensures, and proof functions. Verus can express arithmetic guards and sequence/set relations; Isabelle’s existing automation and its exact theory source do not transfer. Atomic hardware updates require an explicit concurrency model or trusted external specification.

evidence, assumptions, limits

The paper provides a worked i82599 interpretation and formalized refinement, but it does not print the Isabelle theory. It assumes the hardware’s atomic pointer operations and descriptor ordering match the chosen abstraction. The concrete model has only the hardware-defined pointer meanings; ownership of shared pools is kept abstract (Section 3.1, PDF p. 4).

technique 3: interference-aware postconditions and fence derivation

what it is and when to use it

Strict sequential postconditions become false under concurrent dequeue by the other endpoint. CleanQ weakens them to facts stable under interference: after A.enqueue(X), X is in one of QAB, OB, or QBA. The paper states: “In reasoning about A, we cannot rely on X being in QAB, just because A has executed enqueue(X).” (Section 3.3, PDF p. 5). These postconditions support Owicki–Gries-style noninterference proofs.

For weak memory, derive barriers from ownership obligations. Before enqueue, the sender must publish writes and stop relying on reads; after dequeue, the receiver may use the buffer. The paper’s example shows that absent fences a receiver can overwrite X[1], while the sender’s earlier write to X[0] becomes visible later. The paper says, “the execution order indicated by the circled red numbers is consistent with the constraints (and can actually be observed).” (Section 3.4, PDF p. 5).

how to apply it

1. Enumerate all states an interfering endpoint can move the buffer through and write a disjunctive postcondition (Section 3.3).
2. Prove noninterference for each operation against the other’s transitions (Section 3.3).
3. Identify the last sender instruction that can affect the buffer and place a write fence before publishing the ownership transfer; place a read fence before the sender relinquishes the buffer. Apply the symmetric argument at the receiver (Section 3.4, PDF pp. 5–6).
4. Validate the required barriers for the target memory model; the paper notes that all four are necessary when not all instructions are known (Section 3.4).

Verus form

Inference: Represent the weak postcondition as a disjunction over abstract queue states in ensures, and use a Verus transition-system proof for interference. Verus proofs can state ordering contracts, but actual ARM/Power fence instructions and cache coherence need trusted specifications or an external model. A Rust wrapper should make publishing and relinquishing a single verified operation and attach the fence contract to it; an ordinary Rust borrow does not by itself prove device visibility.

evidence, assumptions, limits

The paper reports formal noninterference and refinement proofs in Isabelle/HOL and gives an executable weak-memory counterexample plus fence placement argument. It does not report a machine-checked proof of every C module or automatic fence inference; it says automatic placement “should be possible” and cites earlier work (Section 3.4, PDF p. 6). Inference: a VL product using this technique must treat device registers, cache operations, and foreign code as trusted boundaries unless modeled separately.

measured evidence and product implications

The evaluation ran on a two-socket Intel Xeon E5-2670 v2 at 2.5 GHz, with hyper-threading disabled, on Ubuntu 18.04 and a microkernel OS (Section 5, PDF p. 8). Each stated sample count is explicit: the Memcached CDF uses 100,000 set/get operations (Section 5.3, PDF p. 9), and Table 1 reports median packets per second over 10 runs (Section 5.7, PDF p. 11). CleanQ enqueue/dequeue cost 72/64 cycles including its loopback module, versus Virtio add/get at 56/100 cycles (Section 5.2, PDF p. 9). The Memcached path totals about 10,950 cycles and CleanQ library overhead is reported as less than 1% (Section 5.3, PDF p. 9). Table 1 reports 705,000 packets/s for DPDK, 713,100 for DPDK with CleanQ, and 742,600 for CleanQ UDP, each the median of 10 runs (Section 5.7, PDF p. 11). The paper also reports debug checks adding 50–80 cycles to enqueue/dequeue, with 100,000 repetitions (Section 5.5, PDF p. 10).

Inference: the threat to VL is substantial for verified networking or shared-buffer APIs because ownership, refinement, interference, and fence obligations are exactly the proof obligations that unsafe Rust leaves implicit. CleanQ already supplies the abstraction and performance evidence; VL should reuse its ownership state machine and refinement pattern rather than rediscover a generic descriptor-ring interface. Inference: what remains product-specific is a Verus library for concrete devices, Rust FFI and register contracts, and evidence that the chosen hardware memory model is represented.

what remains trusted and what should not be repeated

The paper trusts Isabelle/HOL, its formalized model, the assumed hardware semantics, C compiler/runtime behavior, and the implementation’s adherence to the specification. It measures performance, not end-to-end functional correctness of each module. Inference: VL should not claim that CleanQ’s measurements verify a Rust implementation; they only show that strict semantics can be inexpensive. Inference: VL should also avoid repeating the paper’s generic ownership-ring design as a new contribution and instead focus on checked Verus encodings and device-specific proofs.

techniques for the catalog

• ownership-transfer state machine — represent exclusive owner and in-flight sets, conserve registered buffers, and make enqueue/dequeue transfer ownership
• abstract-to-ring refinement — relate sets to FIFO lists and then concrete descriptor pointers with simulation proofs
• interference-aware postconditions — weaken operation postconditions to states stable under concurrent endpoint actions
• ownership-derived fences — place publication and acquisition barriers where ownership guarantees require visibility and non-use Checked 2026-10-14 against the paper by a Codex agent: audit record haecki2019lightweight; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15