Techniques for formal modelling and verification on dynamic memory allocators

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

This thesis addresses sequential dynamic memory allocators (SDMA) that manage heap chunks with heap and free lists. It has two complementary methods. First, Event-B models are refined from an abstract allocator into concrete policies, with Rodin proving invariant preservation and refinement. Second, a Separation Logic fragment called SLMA supplies a hierarchical abstract domain for static analysis that infers shape, content, and numerical invariants from existing C implementations. The abstract states the purpose directly: “This thesis contributes to the formal specification and verification of Sequential Dynamic Memory Allocators (SDMA, for short), which are key components of operating systems or standard libraries.” (Abstract, p. II).

technique: abstract Event-B allocator model

What it is. Represent allocator state with sets and mappings: H for chunk start addresses, F for free chunks, csz for chunk sizes, and cst for status. Constants bound the memory region, header size, alignment, and fitting function. The most abstract model has six invariants I1–I6: address bounds, alignment, positive header size, each chunk size at least the header size, consistency of F and cst, and pairwise non-overlap of chunks (Section 3.2, pp. 34–36, Table 3.3). Its events are initialization, successful and failed free, successful and failed allocation, and three realloc cases.

How to apply it. (1) Define the state variables and constants. (2) Write invariants as set-theoretic formulas. (3) Define each operation as an atomic Event-B event with a guard and simultaneous assignments. (4) Generate INIT and INV proof obligations: I(V) ∧ Qe0(V,V') ⇒ I(V') for initialization and I(V) ∧ P(X,V) ∧ Qe(V,V') ⇒ I(V') for every event (Section 3.1.1, pp. 26–27). (5) Use Rodin to discharge the obligations; optionally prove deadlock freedom using the disjunction of event guards (Section 3.1.1, p. 27). The thesis explains the semantic discipline: “Only states that satisfy the invariants properties over the state machine variables are included in the behavior of the state machine.” (Section 3.1.1, p. 24).

Inference: in Verus, encode allocator state as a Rust struct plus a spec fn predicate for chunk bounds, alignment, status, and non-overlap. Put operation preconditions in requires, postconditions in ensures, and preservation facts in proof lemmas. Use invariant clauses on loops that scan the heap or free list. Event atomicity becomes a sequential function body or a Verus state-machine transition; do not write Event-B syntax as if it were Verus.

Evidence and limits. The abstract model deliberately assumes a fixed chunk set, ignores chunk-body contents, and abstracts away chunk disposition; the thesis says these assumptions are removed by later refinements (Section 3.2.1, p. 34). Realloc movement therefore cannot be precisely specified at this layer. Rodin proof statistics for ten models show 2–41 obligations per model, with 66–100% automatically discharged and the rest interactive (Table 4.22, p. 62). These percentages use proof obligations for each named model, not all allocator code.

technique: modular refinement hierarchy

What it is. A concrete Event-B machine refines an abstract machine when its events simulate abstract events under a gluing invariant. Refinement adds implementation detail while preserving abstract behavior. The thesis checks guard strengthening, simulation, and re-establishment of the gluing invariant, named GRD, SIM, and GLU (Section 3.1.2, pp. 29–31).

How to apply it. (1) Start with the abstract allocator. (2) Refine the heap list, adding insertion, removal, splitting, and coalescing (eager, lazy, partial, or none; or a fixed-size array). (3) Refine the singly linked free list, choosing acyclic or cyclic shape and unsorted or address-sorted order. (4) Refine the fit policy after the free list, selecting first-fit, best-fit, or next-fit. (5) Add the backward link for doubly linked lists; the thesis applies it last, but says the proof effort is the same if the fit policy comes after the doubly linked step, and the two steps can be joined (Section 3.3.2, pp. 39–41). (6) For each event, prove the concrete guard implies the abstract guard, the concrete action simulates an abstract action, and the gluing invariant holds afterward (Section 3.3, pp. 37–40). The thesis states the ordering principles: “Refinements of the heap list precede the ones of the free list.” and “Refinements of the fit policy shall be done after the refinement for the free list.” (Section 3.3.2, p. 39).

Inference: a Verus version uses an abstract state predicate and a concrete representation predicate, with lemmas relating them. A public Rust API can preserve the abstract contract while changing the concrete list representation. requires and ensures express the simulation boundary; proof fn lemmas establish the gluing relation. Verus does not automatically infer an Event-B refinement map, so VL must generate and check that relation explicitly.

Evidence and limits. The thesis proves in Rodin one correctness theorem for the heap-list models (Theorem 4.1, p. 52: operations preserve the model invariants; Table 4.11, p. 53: 8–143 obligations per model, 69–100% automatic) and one for the free-list models: “Every operation of a model for SDMA with free list preserves the invariants of the model. Moreover, the refinement relations in Figure 3.3 are valid.” (Theorem 4.2, p. 61). Applications include refinement to code, code generation, runtime invariant checks, and model-based test sequences (Section 4.3, pp. 63–64). For test generation, the thesis reports that the tool could produce test cases only for models near the top of the hierarchy; the lower models, with more complex invariants, could not be handled by the SMT theories connected to the tool (Section 4.3, p. 63). The thesis also says that existing Event-B-to-C and Event-B-to-Java translation tools have no formal result that the translation preserves semantics (Section 8.2, p. 149). Inference: the model hierarchy covers list-based SDMA, assumes sequential use, and does not by itself verify arbitrary C implementation details.

technique: SLMA hierarchical abstract interpretation

What it is. SLMA extends symbolic heaps with predicates for heap and free lists and a composition operator connecting them. Its abstract domain is a product of a heap-shape domain and a finite-array location domain (Abstract, p. II); Chapter 6 builds it as a cofibered product of shape, numerical, and data-word domains (Section 6.3, p. 98). A first abstraction level represents all chunks; a second selects chunks available for allocation. Universal numerical constraints describe sizes and fit policies (Abstract, p. II; Chapter 5, p. 67).

How to apply it. (1) Parse the C program and represent its memory with SLMA atoms for chunks, blocks, and list segments. (2) Step one of the analysis: run inter-procedural, non-relational symbolic execution on a correct client program (minit, malloc, mfree calls) over chunk and block atoms only, which discovers the heap-list and free-list organization and selects list-segment predicates. (3) Step two: project the client variables out and apply folding lemmas to obtain a precondition for each SDMA method; it is not the weakest one. (4) Step three: run forward abstract interpretation from those preconditions, using the transformers for assignments, sbrk, and condition tests (Section 7.3, pp. 134–143) and widening to reach a fixpoint on loops (Section 6.3.7.4, p. 113; Section 7.4.1, pp. 143–145). The thesis says: “The third step does forward, non-relational abstract interpretation [CC77a] starting from the computed pre-conditions of each SDMA method.” (Section 7.4.1, p. 145).

Inference: Verus can use the inferred invariants as candidate predicates and loop invariants, but an inference result is not a Verus proof. Translate list-shape facts into recursive spec fn predicates over sequences or maps, numerical facts into quantified requires/ensures, and discharge them with proof fn lemmas. Keep the analyzer as a specification discovery and review tool; Verus should prove the final executable Rust implementation.

Evidence. The prototype is an OCaml Frama-C plug-in using APRON polyhedra with congruence constraints (Section 7.4.2, p. 145). On five allocators under 300 LOC, analysis took 0.05 seconds for DK FF, DK BF, and DK NF, 0.07 seconds for LA, and 2.8 seconds for KR; the abstract values had 25–32 disjuncts (Table 7.2, p. 145). Its Invariants column lists first-fit for DK FF, DK NF, LA, and KR, best-fit for DK BF, and MIN_SIZE-size (all chunk sizes at least 8) or 0-size (at least sizeof(HDR), 4) invariants; the list predicates are hlsc and flso for all five. The text calls next-fit “a first-fit from the roving pointer” for DK NF (Section 7.4.2, p. 146). The machine was a 2.53 GHz Intel Core 2 Duo laptop with 4 GB RAM, and times include all three analysis steps (Section 7.4.2, p. 146). These are five small C benchmarks, not evidence for arbitrary allocators.

Limits. The client programs are intentionally chosen to reveal list organization and avoid incorrect call sequences that enlarge abstract values (Section 7.4.1, p. 144). Bit-vector statements are manually transformed into polyhedra-compatible statements for precise numerical invariants (Section 7.4.2, p. 145). Inference: this manual preprocessing and bounded benchmark selection are a threat if VL treats inferred facts as complete specifications.

what is proved, what remains trusted, and product relevance

The Event-B part proves invariant preservation and refinement of the modeled allocator family in Rodin (Theorems 4.1 and 4.2, pp. 52, 61). The SLMA part states soundness theorems for unfolding and for the assignment transformers (Theorems 7.1–7.3, pp. 124, 136) and for the guard transformer (Property 7.3.1, p. 143); in the thesis text only the order soundness (Theorem 6.3, p. 111) is followed by a proof, a short argument, and the others carry none. It reports inferred invariants for five implementations. The thesis only conjectures that satisfiability and entailment for SLMA are undecidable (“I conjecture that the satisfiability problem for SLMA is undecidable”) (Section 5.3.3, p. 78; Section 5.3.4, pp. 80–81), although the contribution list says it shows undecidability (Section 1.2, p. 5). Inference: neither part covers C compiler transformations, external calls, hardware behavior, allocator body contents omitted by the abstract model, or termination, since the thesis does not address them. The thesis itself limits the scope to sequential allocators and notes that one unsorted free-list technique needs second-order logic for its precise invariant (Section 1.2, pp. 4–5).

Inference: the threat to VeruLaw is medium to high for allocator and systems agents. The reusable lessons are to separate an abstract API contract from concrete list representations, order refinements so proofs compose, and use shape-plus-numeric invariant inference to seed Verus specifications. VL should not redo this complete allocator taxonomy. A product contribution would be translating inferred candidate invariants into Verus predicates and requiring proof obligations and counterexamples before accepting them. This is especially useful for agent-written unsafe Rust, where a candidate invariant can be checked against concrete ownership and slice bounds.

techniques for the catalog

• Event-B state-machine modeling: define allocator variables, invariants, guarded atomic events, and Rodin proof obligations
• refinement hierarchy: add heap-list, free-list, fit-policy, and doubly linked details while proving guard, simulation, and gluing conditions
• model-based allocator testing: generate finite alloc and free call sequences ending in a failed free from Event-B models, fixing only the csz and fit mappings; the tool scaled only to models near the top of the hierarchy
• SLMA shape abstraction: represent heap and free lists with symbolic-heap predicates and a composition operator
• hierarchical abstract values: abstract all chunks at one level and allocation-eligible chunks at a second level
• sound abstract transformers: compute postconditions for assignments, system allocation, and guards with widening for loops
• invariant inference: infer first-fit and best-fit policies and minimum-size properties from five small C allocator implementations Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The abstract domain is designed with a set of abstract operators manipulating the properties, i.e., abstract transformers.”): I read the whole thesis text (front matter, Chapters 1–8, French annex, symbol list, bibliography) and compared every quotation, number, section and page reference, the Event-B and SLMA technique steps, the proof statistics (Tables 4.11, 4.22), and Table 7.2 against it. Changed: link replaced by the HAL page named on the paper’s title page (the earlier DOI is not in the paper text); the I4 invariant wording; the free-list refinement step (doubly linked is its own last step, fit order note); the step list of the analysis (three steps as in Section 7.4.1) and the third-step quotation, which had dropped the citation [CC77a]; the invariants inferred per benchmark (Table 7.2 lists first-fit for DK NF and KR, not next-fit); the soundness claim (theorems are stated, only Theorem 6.3 has a proof); undecidability is only conjectured in Chapter 5; added the model-based testing scalability limit and the Event-B translation caveat; removed the word alignment from the catalog inference bullet; moved my own conclusions under the Inference label. Not checked: bibliography entries, the Verus translation advice (my inference, not from the paper), the product-relevance judgement, and the cited external works; Figures were read as extracted text only, not visually.

Last edited: 2026-10-17