Practical Formal Verification for MLIR Programs

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

scope and claims

The paper presents PEQC-MLIR, a translation-validation system for checking whether an original MLIR program and a transformed MLIR program have the same final observable memory values. It uses hybrid concrete-symbolic interpretation: known values are evaluated concretely, while values depending on live-in inputs become symbolic computational DAGs (CDAGs). It also builds a happens-before graph to detect races and deadlocks in supported concurrent programs. The paper states: “We target the formal verification of correctness of a transformed program by computing whether a pair of programs are semantically equivalent, one being a transformed version of the other.” (Abstract, p. 1). It restricts the language and synchronization model, so the claim is about that supported class.

technique 1: hybrid concrete-symbolic interpretation

Use this when optimization changes schedules, storage, or parallel structure but the transformed program should compute the same outputs. Translate each MLIR program to PEQC-MLIR’s parallel intermediate representation (PIR), interpret each statement, and retain a normalized symbolic memory state. Concrete subexpressions are computed immediately; expressions containing an unwritten input become AST-style symbolic expressions. For example, the paper represents in1 + 1 as sym(+(in1, 1)), then updates it to sym(*(+(in1, 1), 2)) after multiplying by two (Section 3.2, p. 6). The paper restricts where symbolic expressions may occur, “for example preventing them in array subscripts (we must always be able to associate a unique name to a memory location) or in values set for semaphores” (Section 3.2, p. 6); in the formal semantics a symbolic while condition, array index or semaphore argument also leads to an error state (Fig. 6, p. 9).

The paper says: “We mix concrete evaluation and symbolic representation for expressions, and rely on correctly implementing the concrete semantics of arithmetic expressions in the interpreter.” (Section 3.2, p. 6). It also says: “Through this hybrid interpretation stage, a symbolic representation of the program is built.” (Section 2, p. 5). Steps are: translate both versions into PIR; start from an initial state with no variables defined (Section 3.3.2, p. 11); evaluate expressions whose operands are all concrete under C semantics (32-bit int); promote expressions with a live-in operand to symbolic AST nodes; execute control flow and synchronization; retain the final memory state and CDAG; compare the two states. The paper’s implementation supports C operators, loops and function calls (by inlining), but not recursive functions (Section 4.1, p. 15). Concrete evaluation of all C operators (+, *, /, !=, >>, etc.) follows C semantics (Section 4.1, p. 15).

Inference: In Verus, a Rust implementation can carry symbolic values as an algebraic expression datatype and use spec fn functions for evaluation and normalization. A proof function can establish that each Rust transition preserves the relation between concrete execution and the expression tree. Verus does not provide PEQC’s interpreter or CDAG canonicalizer; those would be ordinary Rust code plus separately proved specifications.

technique 2: happens-before graph for race and deadlock detection

Use this for asynchronous MLIR, AIR, AIE, or OpenMP-like programs with explicit semaphore synchronization. The interpreter creates a graph node for every statement instance and edges for required order. Two nodes “may happen in parallel” when neither reaches the other. After every transition, the graph must satisfy graph_valid (Section 3.3.1, p. 11): no two accesses to the same location, one of them a write, may happen in parallel; no wait has more than one corresponding set; no release has more than one corresponding acquire; no two acquires of the same semaphore may happen in parallel; and the release values matching an acquire may not sum to more than its value. Semaphore operations add ordering edges; a transition that makes the graph invalid produces an error state. The paper defines deadlock as a non-error final state (no outgoing transitions) containing a task-leaf node whose remaining program is not empty (Definition 3.9, p. 14).

The paper defines: “For graph G and two nodes n, m ∈ G, n may happen in parallel with m, denoted n ∥ m, if and only if n ̸⇝∗ m and m ̸⇝∗ n.” (Definition 3.2, p. 8). It reports: “We prove our system can only reach a final state (i.e., the program terminates without error) for deterministic parallel programs, which implies the absence of race and deadlocks.” (Section 3, p. 5). Steps are: create a node for each statement instance; add sequential and semaphore edges (a wait gets an edge from its corresponding set, an acquire from its corresponding releases); check graph_valid, in particular conflicting accesses between nodes that may happen in parallel; return an error on a race or invalid semaphore use; classify a stuck non-error final state with unfinished work as deadlock. Determinism is proved by confluence (Theorems 3.6-3.8, pp. 13-14), so a deadlock found in one execution order holds for all (Corollary 3.10, p. 14). The implementation merges nodes of statement instances that neither use semaphores nor spawn tasks into “macro-node” entries to reduce graph size (Section 4.2, p. 16). The paper’s semaphores are restricted: a release can match only one acquire, and two concurrent sets matching one wait are disallowed (Section 3.3, p. 10).

Inference: In Verus, represent the graph and reachability relation with Rust sets or sequences and prove a loop invariant that accepted parallel writes are disjoint. Semaphore counters need explicit preconditions and postconditions. A Verus proof can establish the modeled graph properties, but it cannot certify hardware scheduling unless that scheduling is included in the model.

technique 3: equivalence by final non-local memory and CDAG normalization

Use this after interpreting both programs. Strict equivalence (Theorem 3.11, p. 14) compares final memory states; the implementation compares only non-local variables, those not local to a terminated task (Theorem 3.12, p. 14). Variables are identified by name across programs, so non-local variables must have identical names in both programs (Section 3.5, p. 14). Exact CDAG identity gives linear-time checking. Optional rewrite rules normalize algebraic differences such as commutation, associativity, or neutral elements. Theorem 3.12 checks the union of both programs’ non-local variables, so a temporary loop counter may differ while an output cannot.

The paper states: “we typically rely exclusively on exact matching between the two memory states: that is, computing whether CDAGs are identical, a simple linear-time process.” (Section 4.3, p. 16). It cautions: “The user must ensure that these are semantically applicable on the program verified; we do not perform any such analysis.” (Section 4.3, p. 16). The paper adds: “We did not use nor need any such custom rewrites in our experiments in Sec. 6.” (Section 4.3, p. 16). Steps are: collect the final non-local memory locations; canonicalize CDAGs by exact identity or configured rewrite rules; compare corresponding values; report equivalence or a mismatch. (The paper does not describe the exact mismatch-reporting order; the appendix, A.1, says its visualizer color-codes the first mismatched node.) Associative/commutative operations can be flattened and lexicographically sorted; simple normalizations include +($x 0) = $x and *($x 0) = 0 (Section 4.3, p. 16).

Inference: In Verus, state the output relation as an ensures predicate over visible Rust data, and prove equivalence with a lemma that invokes normalization lemmas. Any rewrite rule must have a proved semantic side condition; an unproved rewrite is a trust assumption.

technique 4: lower MLIR dialects to PIR and validate compiler transformations

Use this as staged translation validation. Lower standard dialects with existing MLIR passes, lower AIR/AIE with dedicated conversions, translate to C-like PIR plus the PEQC concurrency API, then run interpretation and pairwise equivalence. async tokens become semaphores; memref copies and subviews become pointwise loops and temporary buffers (Section 5.1, p. 17); AIR channels become buffers, layout-copy loops, one semaphore per channel, and waits/sets around reads and writes (Section 5.3, p. 19). The input must lie in a subset of func, arith, math, memref, scf and async (Section 5.1, p. 17). The paper says: “These PIR files are then checked pairwise for equivalence, following Sec. 3.” (Section 6.1, p. 20). It also explicitly scopes trust: “Correctness verification of these lowering passes is outside the scope of this paper.” (Section 5.2, p. 17).

Inference: For Verus, a similar pipeline would require a verified or separately audited Rust IR translator and a specification relating source and lowered states. Verus can prove the PIR interpreter or generated Rust kernel, but not an unmodeled MLIR pass.

evidence, limits, and product threat

On an Intel Xeon E3-1240v6 at 3.70 GHz with 32 GB memory, the AIR case used a 32×32 matrix. The air.placed variant had 190 source lines, 902 converted lines, 1,030 PIR lines, 1,320,799 interpreted statements, 440 concurrent tasks, and 77,815 synchronizations; interpretation took 9.01 s and equivalence 0.04 s (Table 1, p. 20). All files in that table were proved equivalent for symbolic input matrices with fixed problem size. The AIE case had a 753-line AIE file and about 2.2k PIR lines; PEQC-MLIR reported a possible race (a nondeterministic lock acquisition) in under 5 s, with early exit on the first error, and took 31 s on a corrected equivalent version (Section 6.2, pp. 21-22). The paper says testing alone did not find this error; the fix used additional locks. The PolyBench evaluation used 22 optimization paths and 30 benchmarks, producing 580 variants actually generated; the mini dataset took under 30 minutes total, with about 15 minutes generating files and 10 minutes converting/checking (Section 6.3, p. 22). The throughput plot covers 2,160 variants (Figure 10, p. 25).

What is proved is equivalence of the translated, supported PIR programs and absence of modeled races/deadlocks, for the formal featherweight language of Section 3 (the paper gives proofs there, not for the full implementation). Stated in the paper: the interpreter relies on “correctly implementing the concrete semantics of arithmetic expressions” (Section 3.2, p. 6); lowering passes are outside scope (Section 5.2, p. 17); rewrite applicability is the user’s responsibility (Section 4.3, p. 16); the guarantee holds for two programs that “have necessarily the same execution context” (Section 4.1, p. 15); termination needs deterministically computed control flow, for which “Typically, this requires fixed problem sizes” (Section 3.5, p. 15); recursive functions are unsupported (Section 4.1, p. 15); the AIE lowering is not the full dialect, e.g. packet_flow and switchbox are not implemented (Section 5.4, p. 19). Inference: the trusted base therefore includes the MLIR-to-PIR translators and the interpreter itself. Inference: Agent-written verified Rust faces a high product threat if translation, specifications, or normalization silently omit behavior; this work’s pairwise checking and race detection are useful defenses, but the translator and model remain critical trust boundaries.

techniques for the catalog

• hybrid concrete-symbolic interpretation — execute known values and represent live-in-dependent values as normalized symbolic CDAGs
• happens-before race/deadlock checking — build synchronization edges and reject conflicting or stuck concurrent executions
• non-local memory equivalence — compare final visible memory values, optionally after semantic rewrite normalization
• staged MLIR translation validation — lower dialects to PIR and check each transformed pair mechanically Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “This is a case where testing alone did not discover the concurrency error, which is unlikely to be triggered except in unusual scenarios involving significant stalling.”): read the whole paper text (pp. 1-32 including appendix); checked every quotation, page and section reference, Table 1 numbers, the section 6.2, 6.3 and Figure 10 numbers, the definitions of deadlock and graph validity, and the technique steps; changed the Section 2 quote page (p. 5), the example page (p. 6), the capitalization of one quotation, the deadlock and race-check descriptions, the rewrite and non-local equivalence details, and the trust-limit paragraph (marked as Inference where it is mine); did not check the proofs in Section 3.4 line by line, the referenced prior work [43], the PDF figures and tables beyond the text extraction, or the Verus inferences beyond marking them as such.

Last edited: 2026-10-17