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

Modular Reasoning about Global Variables and Their Initialization

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

problem and result

The paper presents a separation-logic technique for modularly verifying global variables and their module initializers, whose timing and order are not known statically and modularly, which may perform arbitrary side effects, and which may have cyclic dependencies; it supports both thread-local and shared global state. It introduces module invariants, module tokens, initialization levels, and duplicable invariants. The abstract states, “A partial order on modules and methods allows us to reason modularly about when a module invariant may be soundly assumed to hold, irrespective of when exactly the module initializer establishing it runs” (Abstract, p. 1). The logic is formalized in Iris and its soundness is proved in Rocq (Abstract, p. 1; Section 3, pp. 12–18). Implementations target Java in VerCors and Go in Gobra (Section 4, pp. 18–21).

technique: non-duplicable module invariants and tokens

Inference: use a non-duplicable module invariant for mutable global state that needs exclusive ownership while being updated. An invariant combines ownership and value facts. In the Fibonacci example, the invariant Inv_Fib owns cache with full permission, states the map is non-null, owns the hash map via is_map(m, a), requires keys 0 and 1, and states that every stored value is non-negative and equals the mathematical Fibonacci value (Section 2.1, p. 6). Fractional points-to permissions permit concurrent reads, while write access requires full ownership (Section 2.1, p. 6).

Apply it in these steps (Sections 2.1.1–2.1.2, pp. 7–8):

  1. Define Inv_M as a separation-logic assertion; the paper says it “typically contains ownership of all global variables of 𝑀”, plus value constraints
  2. Prove the initializer triple that starts with an Init_M resource and full ownership of M’s globals and ends with Inv_M
  3. Give the program entry point (main) the module token [Token M] 1 for every module M
  4. Transfer tokens like other resources (pass them to methods or threads, or include them in predicates and module invariants); the separation-logic rules prevent duplicating or forging them
  5. Open Inv_M (exchange the token for the invariant) only where IC1 (below) holds; owning the token ensures IC2
  6. Close the invariant (exchange it back for the token), which is analogous to folding a predicate, without extra proof obligations

The paper states the safety conditions as follows: “The module invariant of a module 𝑀 may be soundly used at any program point where the two following conditions hold: IC1 𝑀’s initializer has started and finished, that is, its module invariant has been established; IC2 No other thread concurrently relies on or invalidates the module invariant of 𝑀.” (Section 2.1.2, p. 7). A method can require InvFib directly, as in {Inv Fib ∧ 0 ≤ n} fib(n) {v . Inv Fib ∧ v = F(n)}, leaving the caller responsible for opening it (Section 2.1.2, p. 8).

Inference: In Verus, a global-state abstraction can be represented by a ghost token and a predicate over a static or heap object, with requires/ensures transferring exclusive ownership. Verus’s ownership model and supported synchronization differ from Iris’s fractional separation logic; the exact token algebra does not carry over. A Verus design should keep the invariant in ghost state and expose only contract functions for mutation.

technique: initialization levels for definite initialization

Use levels to prove that an invariant is opened only after the module initializer cannot still be executing. Programmers annotate each module, module initializer, and method with an element of a pre-selected partial order. The paper imposes: LC1, a module initializer’s level is strictly below its module’s level; and LC2, a method or module initializer at level l may call only methods at a level at most l (Section 2.2, p. 8). Hence the initializer of a module can (directly or indirectly) call only methods with a strictly smaller level, and all other methods “may safely assume that they are not executed while 𝑀’s module initializer runs” (Section 2.2, p. 8). Accessing a global variable or calling a static method of M yields Init_M, showing initialization has started; the level check shows it has finished (Section 2.2, p. 8).

Steps: (1) assign a level to every module; (2) assign its initializer a strictly smaller level (LC1); (3) assign each method a level at least that of every method it calls (LC2); (4) require the Init_M resource at an invariant opening; (5) check the current method’s level against M’s level (Section 2.2 says “above” and footnote 6 says not below would suffice except for cycle prevention; rule OpenMInv in Fig. 6, p. 16, states Φ(M).Level ≤ l); (6) reject level assignments violating LC1 and calls violating LC2. The paper notes that LC2 “allows recursive implementations (including mutual recursion if all involved methods have the same level)” (Section 2.2, p. 8). It also says method levels relate to termination measures, e.g., Dafny’s, whose first component is the module name ordered by the import relation (Section 2.2, p. 9).

Inference: Verus has no built-in initialization-level construct. VL could encode levels as ghost type parameters or a separate static dependency analysis that rejects calls before generating Verus code. decreases measures can supply related well-founded ordering for recursion, but they do not by themselves model runtime module initialization.

technique: duplicable invariants for immutable or synchronized globals

Use a duplicable invariant when its assertion P satisfies P ≡ P * P; such an invariant cannot grant full ownership or a fixed fraction of a resource. This handles immutable global constants and mutable globals protected by a lock. Opening does not require a module token; it requires that the current method or initializer owns Init_M and its level is at least M’s level, the initializer must establish the invariant, and LC1 and LC2 must hold (Section 2.3, p. 10).

For the Counter example, the global cl is declared final and holds a lock, and the mutable count is owned by the lock invariant lock_inv ≜ count ↦1 _. The duplicable module invariant asserts fractional ownership of cl (pointing to lock object o) plus is_lock(o, lock_inv) (Section 2.3, p. 10). Steps: (1) establish the duplicable invariant in the initializer; (2) obtain Init_Counter by accessing cl; (3) assign getAndInc a level at least Counter’s and the lock operations levels below Counter’s; (4) acquire the lock to obtain full count ownership; (5) increment; (6) release the lock, giving back the lock invariant. The paper says, “A duplicable invariant cannot provide full ownership (or even a fixed fraction) of a resource” (Section 2.3, p. 10); consequently, once established, it cannot be violated by writes and IC2 holds automatically (Section 2.3, p. 10).

Inference: In Verus, immutable global facts can be spec fn predicates with read-only proofs; lock-protected state needs a ghost lock invariant and Rust synchronization API contracts. Verus’s tracked permissions and ownership must replace Iris’s fractional resource algebra; do not encode a runtime lock invariant as executable proof code.

technique: reject cyclic initialization with LC3

LC1 and LC2 alone do not prevent cycles between module initializers. The paper’s classes A and B (Listing 3) show A’s initializer calling B.foo before setting A.f = 1, while B’s initializer opens A’s invariant to assert A.f == 1; this verifies under LC1/LC2 (pick B.foo < A < B) although the assertion is reached before f is initialized (Section 2.4, pp. 10–11). Add LC3: a method or module initializer at level l may access a global field or call a static method of M only if it owns Init_M or M’s level is at most l (Section 2.4, p. 11).

Steps: (1) treat accesses to globals and calls to static methods of M as “calling” M’s initializer in case it has not been started; (2) check LC3 at every such access; (3) a program whose level constraints are unsatisfiable fails to verify. In the example, LC3 adds the constraint B < A for the call to B.foo, making the set of level constraints unsatisfiable (Section 2.4, p. 11).

Inference: A Verus tool can build a module/method dependency graph and check for cycles before emitting Rust proof obligations. A Rust Once or lazy_static! implementation still needs contracts for initialization state; Verus alone will not infer the runtime order.

technique: language-specific simplification

The core logic assumes only C1–C3 (Section 1, p. 4): C1, M’s initializer starts at the latest at the first definitely-initialized execution point for M and finishes before the next operation unless it does not terminate or M is part of a cyclic initialization dependency; C2, only the first occurrence of an operation that triggers initialization triggers it, and “No other operations wait for module initialization to finish”; C3, each initializer runs at most once. Stronger language guarantees simplify proof obligations. In Java, a subclass’s level must be at least its superclass’s level (to prevent indirect cycles; the paper says this is not necessary for soundness), and an overridden method’s level must be at least that of its overrides (Section 4.1.1, pp. 18–19). In sequential Java, tokens are not used because IC2 holds trivially; levels track which invariants may be opened, code that runs while a non-duplicable invariant of level l is open must be correct at a level strictly less than l, and initializers must close all non-duplicable invariants they opened before terminating (Section 4.1.2, p. 19). Go package imports form a DAG, packages initialize eagerly and sequentially in reverse import order, levels can be inferred from imports, and all non-duplicable invariants can conceptually be opened at the beginning of main, removing module tokens; level annotations are needed only for methods that may be called from the package initializer (Section 4.2.1, p. 20), which Gobra marks mayInit (Section 4.2.2, p. 21).

For Go packages with multiple initializers across files, over-approximate the unknown order by modeling each initializer as a thread running in parallel with the others, whose precondition contains only the permissions to the globals declared in its file; establish the package invariant after all initializer threads conclude (Section 4.2.1, p. 21). The authors added or modified about 1,000 lines of code in VerCors for Java and added around 900 new lines to Gobra for Go (Sections 4.1.3 and 4.2.2, pp. 20–21). The paper notes that Rust has no initializers but the lazy_static! macro provides similar functionality (footnote 2, p. 2).

Inference: For Rust, OnceLock, lazy_static!, and linker/static initialization semantics must be modeled explicitly. VL can simplify levels for a single-threaded or eagerly initialized deployment only after stating and checking those runtime assumptions.

formal soundness, evidence, and limits

The Iris/Rocq formalization proves soundness for an ML-like concurrent language with global modules, given semantics by translation to HeapLang with each initializer run in its own thread (Section 3, pp. 12–18). Initialization cycle freedom follows from asserting that blocking module accesses are strictly monotonic in runtime levels; the paper says, “We do not mechanize this proof beyond showing that accesses are monotonic.” (Section 3.5, p. 18). The implementation evaluation contains 11 small case studies. Table 1 reports Go and Java LOC, annotation lines, module-invariant-specific annotation lines, and times averaged over 10 runs on a laptop with an Apple M2 Max and 64GB of RAM (Section 5.1, pp. 22–23). Initialization-specific annotations were at most 22% of the total code in Go and at most 25% in Java, except the Java Client class at 35% (Section 5.1, p. 23). The slowest Finalizer example took 33.46 seconds in Go and 21.35 seconds in Java; the paper attributes this to a method using a module invariant with heavy use of quantifiers and sequences, “a known issue unrelated to initialization-specific proof obligations” (Table 1 and Section 5.1, pp. 22–23).

The real-world evaluation covers the SCION router’s Go code base of about 4.7k lines. Eight packages use duplicable invariants; three of them also use non-duplicable invariants. The additions are 67 lines of duplicable invariants, 27 lines of non-duplicable invariants, and 30 lines of initialization-related ghost code or annotations. Verification averaged 45m46s without the initialization-related proof obligations and 47m05s with them, an increase of less than 3% (Section 5.2, p. 23). The authors also found a previously unknown Go compiler bug while testing that their Gobra implementation matches the Go language specification (Section 4.2.2, p. 21).

Inference: trusted assumptions include the language initialization conditions C1–C3, the soundness of the VerCors and Gobra encodings (the Rocq proof covers the core language), specifications for library methods such as HashMap, and the correctness of synchronization primitives; the technique does not prove compiler, runtime, hardware, or library implementations. Inference: agent-written verified Rust is threatened by unsound static/initializer models, incorrect lock contracts, and ghost invariants that do not describe actual global state. The paper’s levels and token discipline are reusable safeguards, but a passing Verus proof is only as strong as the runtime model and trusted libraries.

Inference: VL should reuse module invariants, explicit initialization-order constraints, duplicable lock/constant invariants, and language-specific simplifications. It should not redo the paper’s Iris soundness proof or 4.7k-line router evaluation; it should adapt the obligations to Rust initialization mechanisms and test generated contracts against actual runtime behavior.

techniques for the catalog

  • module invariants: combine ownership of global variables with value properties and establish the assertion in each module initializer
  • module tokens: use non-duplicable resources to prevent concurrent opening and mutation of mutable global invariants
  • initialization levels: impose a partial order on modules and methods so an opened invariant is definitely initialized
  • duplicable invariants: model immutable globals and lock-protected mutable state without exclusive module tokens
  • cycle prevention LC3: constrain global accesses and static calls to make initialization dependency cycles unsatisfiable
  • language-specific simplification: exploit Java or Go initialization guarantees to remove unnecessary token and level obligations
  • parallel initializer over-approximation: model unordered Go file initializers as parallel threads with disjoint global ownership Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “In this encoding, the program expression is executed in one thread, and each module initializer is executed in a separate thread forked from the main one.”): checked every quotation, number, section and page reference, technique step, and the DOI against the paper text; changed section page ranges (Section 3 pp. 12–18, Section 4 pp. 18–21, Section 4.1.2 p. 19), the reversed method-override level rule, the C2 paraphrase, the LC1/LC2 step wording, the Counter invariant, the token-transfer and closing steps, the recursion note, mayInit attribution, the VerCors line count wording, and added the unmechanized cycle-freedom caveat and the Rust lazy_static! footnote; marked the trusted-assumption and VL-recommendation paragraphs “Inference:”; did not check the extended version, the artifact, or the Rocq development.

Last edited: