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

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction

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

what the paper proves or measures

Beck, Yoon, Chen, Zakowski, and Zdancewic formalize a low-level memory model that separates optimization from finite-machine effects. The infinite phase has unbounded addresses and an unbounded iptr integer type; ordinary fixed-width integers remain bounded. The finite phase uses 64-bit addresses and iptr values and can produce out-of-memory (OOM). The paper’s key idea is stated directly: “The advantage of this is that many optimizations, such as dead allocation elimination, are always valid in the infinite memory model without any additional reasoning (though some optimizations are valid in both).” (Introduction, p. 3). A Coq formalization instantiates the model in the VIR LLVM-like semantics, proves an infinite-to-finite refinement that introduces only OOM behavior, and supplies executable reference interpreters.

The paper proves semantic theorems and verifies three representative transformations: dead-allocation removal, removing a dead pointer-to-integer cast together with its allocation, and adding an allocation. It does not claim to verify full optimization passes: “Though we have not (yet) verified full-blown optimization passes based on these transformations, the semantic reasoning used in the following refinement proofs is representative of the key ideas needed for the general case.” (Section 5, p. 21). Section 6.2.1 (p. 24) reports “several hundred hand-written unit tests” and tests generated by compiling C programs. It also says: “We have also experimented with using QuickChick [11] to randomly generate LLVM IR programs that stress-test the memory model, and we can use the ability to generate LLVM IR to instantiate parts of the Alive2 [28] suite as executable tests.” The comparison is explicit: “In all cases, we do differential testing of the executable VIR model versus llc to look for problems on either side.” Exact test counts and runtime measurements are not reported.

technique 1: split compilation into infinite and finite phases

what it is: perform nearly all optimization under an unbounded model, then translate the optimized program to a bounded model. The finite translation is almost syntactic identity but may add OOM points. The authors summarize: “Once optimizations are performed, there is an explicit translation to the finite model.” (Section 3, p. 8).

when to use: Inference: use this when a language exposes pointer–integer casts and finite machine memory but compiler optimizations need abstract, unbounded allocation. It avoids requiring every optimization to prove that allocations always succeed.

how to do it:

  1. Define the infinite model with Coq integers for addresses and an unbounded iptr (Sections 3 and 4.2, pp. 8–16)
  2. Define the finite model with 64-bit addresses and iptr, using OOM for address overflow and out-of-range iptr arithmetic (Sections 3.2 and 4.3.3, pp. 9 and 18)
  3. Prove an operation-level relation between the two configurations and operations, allowing finite executions to stop with OOM (Section 3.5, pp. 13–14)
  4. Optimize the program under infinite semantics, where dead allocations and casts can be removed (Section 5, pp. 21–22)
  5. Translate the optimized syntax to the finite VIR semantics and use the refinement theorem to relate behaviors (Sections 3.5 and 4.5, pp. 13–14 and 20–21)

Verus form: Inference: model an abstract unbounded address/provenance state with ghost maps and a concrete bounded Rust representation with explicit OOM/error results. Use spec fn relations between abstract and concrete states, requires for valid allocations, ensures for preservation/refinement, and proof fn lemmas for each memory operation. The phase split is an architectural proof pattern; Verus does not supply Coq’s nondeterministic semantics or a compiler-level refinement theorem automatically.

evidence and limits: The formal result is a Coq refinement theorem for the paper’s VIR semantics; it is not a Rust compiler proof. The authors state: “Our memory model is currently just a sequential one.” (Section 7.1, p. 25). They propose extending the approach to concurrency as future work. OOM is intentionally permissive: “Perhaps surprisingly we always allow operations to halt preemptively with an out-of-memory behavior.” (Section 3.4, p. 12). The refinement must preserve the execution before OOM; unlike UB, OOM does not justify changing earlier behavior (Section 4.4, p. 19). Inference: product claims must decide whether this permissive OOM abstraction is acceptable for the target runtime.

technique 2: provenance-aware specification monad

what it is: configurations contain byte memory with provenance, heap allocation roots, stack frames, and used provenances. Each primitive is a nondeterministic MemSpec mapping an initial configuration to a set of Result behaviors: UB, OOM, FAIL, or ok. The paper explains the purpose: “The monadic specification is particularly useful for maintaining very similar structures between the memory model and the executable interpreter (See Section 6), which simplifies maintenance and the proof that the executable implementations of the memory model respect the specifications.” (Section 3.3, p. 10).

when to use: Inference: use this to specify byte reads/writes, stack/heap allocation, free, and frame operations while preserving alias provenance and permitting implementation nondeterminism.

how to do it:

  1. Parameterize the configuration by address and symbolic-byte types; store (byte, provenance) at each address (Sections 3.1–3.2, pp. 9–10)
  2. Define pointer access as an address lookup with a provenance check; invalid reads and writes may raise UB (Sections 3.2–3.4, pp. 9–12). Account for the wildcard provenance used by integer-to-pointer casts; this implementation does not track provenance through integers (footnote 13, p. 16)
  3. Define MemSpec(X) = Conf → P(Result(Conf × X)) and compose operations with ret and bind (Section 3.3, p. 10)
  4. Specify read_b, write_b, alloca, malloc, free, pushf, and popf with frame/heap and unchanged-memory conditions (Section 3.4, pp. 10–13)
  5. Relate operation results to the infinite/finite refinement relation (Section 3.5, pp. 13–14)

Verus form: Inference: encode Result as an enum, memory as a ghost map from address to (byte, provenance), and pointer validity as a spec fn. Verified wrappers can return Result and use ensures to state that writes change only the pointed location and allocation returns disjoint addresses. Verus’s executable Rust is deterministic unless modeled otherwise; nondeterministic choices should be represented as ghost relations or a separately verified reference model.

evidence and limits: The Coq proofs establish operation-level soundness and refinement. The paper elides FAIL using partial specifications; FAIL covers intended static checks and unimplemented language features. OOM is broadly permitted, while source UB permits arbitrary refinements (Sections 3.3–3.4, pp. 10–12). Inference: provenance prevents cross-allocation aliasing only under the model’s pointer rules; unsafe Rust, FFI, integer casts, and allocator behavior need separate contracts.

technique 3: refine VIR with symbolic bytes, undef, and iptr

what it is: the authors instantiate the generic model in VIR, an LLVM-like semantics containing pointer/integer casts, undef, poison, symbolic bytes, and nondeterministic memory. The infinite and finite models differ in pointer and iptr types; concretization maps symbolic/undef values to concrete values while preserving refinement. Section 4.5 proves the finite lowering relation, and Theorem 6.1 proves the executable interpreter is a valid refinement.

when to use: Inference: use this pattern when a language’s IR has underdefined values and low-level casts that cannot be represented safely by a single concrete execution semantics.

how to do it:

  1. Define dynamic and under-defined VIR values, including iptr, symbolic bytes, and undef (Section 4.2, pp. 15–17)
  2. Serialize a stored value into symbolic bytes with a fresh store ID. Recover the original value when loading the complete byte sequence from one store with the same type; otherwise retain a concatenation of symbolic bytes (Section 4.2.2, pp. 16–17)
  3. Define concretization into sets of concrete values or exceptional results, without a finiteness restriction. Concretize bytes from the same store consistently before concatenating and converting them to the requested type (Section 4.3.1, pp. 17–18)
  4. Use unbounded arithmetic for infinite iptr; halt with OOM on out-of-range finite iptr arithmetic instead of wrapping or introducing UB (Sections 4.3.2–4.3.3, p. 18)
  5. Prove behavioral refinement within each model and then lowering from VIRinf to VIRfin (Sections 4.4–4.5, pp. 18–21)
  6. Instantiate executable operations and show the deterministic interpreter’s singleton behavior refines the nondeterministic specification (Sections 6.1–6.2, pp. 23–24)

Verus form: Inference: use ghost enums/records for symbolic bytes and undef choices, with spec fn concretization and proof fn refinement lemmas. Keep executable code explicit about Result/OOM/UB; do not erase undefined behavior into assume or mark the verified implementation external_body. The paper’s coinductive interaction trees and Coq module abstraction do not carry over directly.

evidence and limits: Theorem 6.1 states the interpreter is sound with respect to the VIR specification (Section 6.2, p. 24). Differential tests found unclear LLVM corner cases involving sub-byte structure addresses and extractelement (Section 6.2.1, p. 24); this is evidence of model-testing value, not a proof that LLVM itself is unambiguous.

technique 4: optimization proofs under the model

what it is: prove refinement relations for transformations as small semantic blocks. Optimization 1 removes a dead allocation in the infinite model. Optimization 2 removes both a dead ptrtoint cast and its allocation, so the displayed transformation is infinite-only; removing the cast alone is valid in both models. Optimization 3 adds an alloca and is allowed in both models because OOM refinement accounts for the extra allocation (Section 5, pp. 21–22).

how to do it:

  1. State source and target snippets as VIR programs (Figure 10 and Section 5, p. 21)
  2. Choose the appropriate model: removing the allocation, including in the cast-plus-allocation example, is infinite-only; removing the cast alone and adding an allocation are valid in both (Section 5, pp. 21–22)
  3. Prove a behavioral refinement relation between source and target interaction trees (Sections 4.4 and 5, pp. 18–19 and 21–22)
  4. Inference: use transitivity to compose such relations in a future verified pass (Theorem 4.2, p. 20). The paper leaves whole-pass static analysis and syntax manipulation outside scope (footnote 15, p. 21)

Verus form: Inference: represent a source and optimized Rust function, define an observational spec fn relation over return values and allowed errors, and prove it with ensures/proof fn. For allocation changes, include OOM/error behavior in the postcondition. Rust’s ownership may rule out some aliases, but integer-to-pointer casts and unsafe code still require explicit provenance assumptions.

evidence and limits: The paper’s three transformations are Coq-verified examples, not a full compiler. The authors expect finite bounds-check costs to be small: “We believe that the flexibility our memory model allows for optimizations prior to the finite language level will outweigh these rare costs.” (Section 5.1, p. 23). This is an expectation; the paper provides no runtime measurements. Inference: this is a semantic foundation for a verifier, not evidence of production compiler speed.

techniques for the catalog

  • two-phase memory refinement — optimize under unbounded addresses, then lower to bounded memory with explicit OOM refinement
  • provenance-aware specification monad — specify byte operations and allocation as nondeterministic behaviors over pointer provenance
  • undef and cast concretization — relate symbolic bytes, undef, and pointer/integer values to their allowed concretizations
  • executable reference interpreter — implement deterministic operations and prove result membership in the specification or source UB
  • block-level optimization proofs — prove dead-allocation, cast-removal, and allocation-addition refinements before composing passes

Last edited: