PaperlayerView exact revision on arXiv

Source-linked AI summary

A formally verified compiler back-end

Xavier Leroy

arXiv:0902.2137v3cs.LOcs.PL

TL;DR

Compiler bugs can silently produce incorrect executables, while testing becomes more complex when optimizations are involved. This article develops and formally verifies an end-to-end compilation chain, providing evidence that formally verifying a realistic compiler is achievable within current proof assistants and elementary semantic and algorithmic approaches.

  • Problem

    Compiler bugs can silently generate incorrect executables, and testing optimized compilers requires more complex test plans.

  • Method

    The work uses Coq to program and prove semantic preservation for an end-to-end compilation chain from a structured imperative language to assembly through six intermediate languages.

  • Results

    The formal verification provides strong evidence that formally verifying a realistic compiler can be achieved within the limitations of today’s proof assistants.

  • Takeaways & Limitations

    The verified compilation approach supports certification of critical software by connecting source-level safety properties with behavior of compiled code.

  • Takeaways & Limitations

    Stack-usage bounds are not naturally preserved by compilation, so the required bound may need to be established directly on compiled code under restrictions such as no recursion or function pointers.

Abstract

from arXiv · show

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.

1 Introduction

Compcert addresses the risk that compiler bugs can invalidate formally verified source programs by formally verifying a realistic, lightly optimizing back-end from Cminor to PowerPC assembly. Its proofs establish semantic preservation across a complete compilation chain, while verified validators and compositional proofs offer alternative scalable strategies.

  • Motivation: Compiler bugs can silently produce incorrect executables, making the compiler a weak link when formal guarantees are established only for source code.This risk is especially important for safety-critical software, where testing reaches its limits and formal methods are used.
  • Motivation: Testing, disabling optimizations, and manually reviewing generated assembly do not fully address compiler risk and impose development-time or performance costs.Optimization testing can require additional limit conditions, such as those introduced by loop unrolling.
  • Contribution: Compcert verifies a lightly optimizing compiler back-end that translates Cminor into PowerPC assembly using the Coq proof assistant.The broader compiler targets a large subset of C and uses multiple passes, register allocation, and basic optimizations for critical embedded software.
  • Novelty: The work emphasizes end-to-end verification from a structured imperative language to assembly through 6 intermediate languages, rather than verifying only selected compiler components.The authors report that even non-optimizing translations considered obvious can be surprisingly difficult to prove correct formally.
  • Novelty: Most of the compiler is written directly in Coq and automatically extracted to Caml, an approach applied here to an optimizing compiler of unprecedented size and complexity.The article presents the development at a high level and refers readers to the extensively commented Coq source for proofs and low-level details.
  • Verification strategy: The verified back-end proves forward simulation for safe programs and target determinism, yielding preservation of all source specifications relevant to compiler users.Semantic preservation also ensures that compiled code has only acceptable observable behaviors and, with a separate source typing check, executes without memory violations.
  • Verification strategy: Verified validators can replace direct verification of compiler implementations, and verified compilation passes compose when semantic preservation is transitive.These alternatives can reduce the code requiring proof while retaining formal guarantees, and Coq proof terms can theoretically support proof-carrying code.

3 Infrastructure

CompCert’s infrastructure provides common program, value, memory, environment, and transition-semantics frameworks for verified compilation. Compilation passes are total transformations, and simulation theorems establish semantic preservation for successful, non-wrong executions.

  • Program representation: CompCert programs share a common structure across source, intermediate, and target languages, including globals, functions, and an entry point.Programs contain initialized or reserved global data, internal or external function definitions, and a distinguished entry function.
  • Program transformations: Compilation passes are total functions that return either a transformed result or an error, then map function-level transformations over whole programs.Unchanged external definitions are preserved, while successful internal-function transformations are assembled into the resulting program.
  • Values and memory: The semantics use discriminated values, block-based memory, and typed load/store quantities, with failed or mismatched accesses modeled explicitly.Values include integers, floats, pointers, and undef; memory operations can fail on invalid or out-of-bounds accesses, while incompatible overlaps yield undef.
  • Values and memory: The memory model hides endianness and bit-level representations by using casts and undef for incompatible or partially overlapping accesses.A load after a store returns a cast value for matching locations and sizes, the prior value for disjoint ranges, and undef otherwise.
  • Global environments: Global environments and initial memories model linking and loading, with deterministic block allocation preserving symbols, function associations, and initialized memory across transformations.The cited preservation properties include unchanged initial memory, preserved symbol blocks, and corresponding transformed function definitions.
  • Simulation and preservation: Semantic preservation is proved by relating source and target states through simulations, including lock-step and star variants that imply preservation of non-wrong behaviors.Theorems 3 and 4 derive target behavior from initial-state, final-state, and simulation hypotheses; either stronger simulation variant implies star simulation.

4 The source language: Cminor

Cminor is a processor-independent, low-level imperative language whose dynamic semantics combine natural expression evaluation with labeled transitions for statements and functions.

  • Cminor is a stripped-down, typeless variant of C and the lowest-level processor-independent language in the CompCert chain.
  • Cminor supports integer and floating-point arithmetic, comparisons, explicit conversions, memory operations, and address formation without overloading or implicit conversions.
  • Expressions are pure, while assignments, memory writes, calls, returns, sequencing, conditionals, loops, blocks, exits, switches, labels, and gotos are statements.
  • Internal functions contain signatures, parameters, locals, stack-size declarations, and bodies; explicitly allocated stack data receives a fresh memory block.
  • Its semantics use big-step evaluation for expressions and a labeled transition system for statement and function execution, with states carrying functions, continuations, stack data, environments, and memory.
  • Theorem 5 establishes that terminating and diverging natural-semantic executions correspond to executions in the transition semantics.
  • The weak int-or-float type system preserves broad value categories but does not guarantee freedom from run-time type errors.

5 Instruction selection

Instruction selection rewrites Cminor expressions and statements into processor-specific CminorSel operations, exploiting PowerPC addressing modes and combined instructions while preserving semantics.

  • 5 Instruction selection: The pass performs bottom-up expression rewriting, reassociation, constant propagation, and exploitation of combined arithmetic operations and target addressing modes.
  • 5.1 The target language: CminorSel: CminorSel adds processor-specific operators, addressing modes, and condition expressions while retaining the surrounding Cminor statement structure.
  • 5.1 The target language: CminorSel: For PowerPC, CminorSel includes immediate operators and combined operations such as rotate-and-mask, while synthesizing unsupported remainder operations.
  • 5.2 The code transformation: Smart constructors pattern-match shallowly over translated expressions to select immediate or combined CminorSel operations.
  • 5.2 The code transformation: The constructors can reduce 8 + (x + 1) × 4 to x × 4 + 12 and recognize a PowerPC rotate-and-mask instruction for a common bit-rotation encoding.
  • 5.2 The code transformation: Condition and addressing-mode recognition accompanies a straightforward bottom-up traversal that applies the appropriate constructors at each expression.
  • 5.3 Semantic preservation: Semantic preservation is proved first for smart constructors and then for translated expressions by induction on Cminor evaluation derivations.
  • 5.3 Semantic preservation: A lock-step simulation follows because translated statements retain their structure, with matching states sharing environments and memories.

6 RTL generation

RTL generation converts structured CminorSel code into control-flow graphs with pseudo-register instructions, using a relational specification and simulation proofs to establish semantic correspondence.

  • RTL represents each function as a control-flow graph of abstract instructions operating on unlimited pseudo-registers whose values survive calls.
  • Instructions encode operations, memory access, calls, tail calls, branches, and returns, with successor labels attached to instruction nodes.
  • RTL states include the current CFG, program point, stack block, pseudo-register assignment, memory, and a list of call-stack frames.
  • The translation encodes structured control as a CFG and decomposes expressions into instruction sequences, using pseudo-registers for variables and intermediate values.
  • RTL lacks N-way branch instructions, so Cminor switch statements are translated into binary decision trees.
  • The relational specification associates each expression or statement with a CFG subgraph whose paths compute values, preserve registers, and expose appropriate exits.
  • Freshness conditions keep temporary registers separate from source-variable registers and earlier expression temporaries.
  • Lemma 5 proves that generated RTL runs from an expression’s start to end node, stores its value in the destination register, and preserves designated registers.

7 Optimizations based on dataflow analysis

CompCert uses generic, mechanically verified dataflow analyses to support constant propagation and common subexpression elimination while proving each transformation semantically preserving.

  • Generic dataflow solvers: The compiler formalizes forward dataflow analyses over control-flow graphs using transfer functions, abstract values, ordering, and constraints.The analysis computes abstract values after each instruction from values before it.
  • Generic dataflow solvers: Inequations are solved for correctness rather than optimality, so upper-bound operations need not compute least upper bounds.This choice supports simpler generic solvers.
  • Generic dataflow solvers: The two Coq functor solvers implement Kildall’s worklist algorithm and propagation over extended basic blocks.Kildall’s solver requires decidable equality, a least element, and an upper-bound operation.
  • Generic dataflow solvers: Because termination is not guaranteed, solvers return failure after a bounded iteration count, allowing compilation to abort or disable the optimization.The fallback can return the input code unchanged.
  • Constant propagation: Constant propagation tracks known register constants and addresses, specializes instructions when values are known, and defaults loads to unknown without alias analysis.The transformation can create load-constant instructions, simplify conditions, and use cheaper immediate forms.
  • Semantic preservation: Both optimization proofs use lock-step simulations whose invariants relate concrete execution states to the corresponding static-analysis results.Constant propagation uses register–abstract-value agreement, while common subexpression elimination uses satisfaction of value-numbering facts.
  • Common subexpression elimination: Common subexpression elimination uses local value numbering over extended basic blocks and rewrites redundant operations or loads as moves from previously computed results.Its approximate dataflow solver orders value numberings by entailment.

8 Register allocation

Register allocation maps RTL pseudo-registers to hardware registers or stack slots through verified analyses and graph coloring, while preserving values live before each instruction.

  • Target language: LTL replaces RTL pseudo-registers with locations, which are hardware registers or abstract stack-slot designations.Its semantics uses location maps and anticipates later memory placement.
  • Target language: LTL call semantics undefines temporary and caller-save registers after calls, requiring allocation to keep live-across-call values elsewhere.This enforces the relevant calling-convention constraint.
  • Allocation analysis: Type reconstruction assigns each pseudo-register an int-or-float type, using untrusted unification followed by a verified Coq type checker.The assignment guides allocation toward locations of the correct kind.
  • Allocation analysis: Liveness is computed by backward dataflow analysis, and the resulting interference graph records conflicts between pseudo-registers and machine registers.Move-related affinities are also recorded to enable coalescing.
  • Graph coloring: An untrusted George–Appel coloring implementation is checked by a verified validator for color correctness, register-class preservation, and valid locations.The resulting mapping Φ assigns pseudo-registers to locations.
  • Semantic preservation: The semantic-preservation invariant preserves the values of all pseudo-registers live before the current instruction, rather than requiring every pseudo-register to retain its value.This weaker relation permits sharing locations among pseudo-registers whose values are dead.

9 Branch tunneling and no-op elimination

Branch tunneling removes no-op chains and redirects control flow to effective destinations, with a well-founded construction supporting semantic-preservation proofs.

  • No-op elimination: No-op instructions generated by coalescing and dead-code elimination are made unreachable and removed during control-flow linearization.The same pass performs branch tunneling by eliminating branches to branches.
  • Branch tunneling: Branch tunneling replaces each successor with its effective destination, computed by following no-op instructions to the first non-no-op instruction.The naive recursive definition is represented by DF.
  • Branch tunneling: No-op-only cycles can make naive destination chasing nonterminating, so recursion depth may be bounded by the function’s instruction count.A bounded computation returns the current label when the counter reaches zero.
  • Branch tunneling: A union-find structure provides an alternative effective-destination computation by making each label’s canonical representative its destination.The graph scan unions no-op edges unless endpoints already share an equivalence class.
  • Semantic preservation: The proof uses an option simulation in which one source step corresponds to one target step or to a shorter sequence of skipped no-ops.The number of skipped no-ops supplies the well-founded measure preventing infinitely many zero-step cases.

10 Linearization of the control-flow graph

CFG linearization converts LTL graphs into labeled instruction lists through a validated enumeration and code-generation pass, while semantic preservation remains independent of trace-picking heuristics.

  • Linearization design: Linearization replaces LTL control-flow graphs with instruction lists containing explicit labels and branches to labels.CFGs suit dataflow analysis, whereas lists simplify later instruction insertion.
  • Linearization design: The implementation separates heuristic node enumeration from correctness-critical code generation.This separation avoids entangling trace-picking choices with the semantic-preservation proof.
  • LTLin semantics: LTLin execution uses suffixes of instruction lists as program points and resolves labels through an auxiliary lookup function.Most instructions fall through from the current instruction sequence to its suffix.
  • Validated enumeration: The validator requires each reachable CFG node to appear exactly once in the enumeration.Reachability is checked using a simple forward analysis over the domain {false, true}.
  • Code generation: Code generation concatenates translated instructions in enumeration order, inserting labels and omitting gotos that target the immediately following label.Conditional branches inspect whether the generated sequence starts with the relevant labels.
  • Semantic preservation: Each original intra-function transition expands into two or three LTLin transitions, motivating a plus-style simulation invariant.The invariant maps an LTL label to findlabel in the translated function.
  • Semantic preservation: Semantic preservation requires only uniqueness and reachability of the enumeration, so many trace-picking heuristics can be changed without redoing the proofs.The result makes the linearization presentation robust to external heuristic choices.

11 Spilling, reloading, and materialization of calling conventions

This pass completes register allocation by materializing spills, reloads, and calling-convention moves in Linear code. Its semantic-preservation proof relates differing location and memory states through invariants and a star simulation.

  • Calling conventions: Calling conventions are materialized by moving arguments and results to conventional processor-register and stack-slot locations around calls and function entries.The generated code also handles tail calls and parameter locations through explicit moves.
  • The Linear language: Linear restricts arithmetic, memory-access, and branch operands to machine registers, while getstack and setstack transfer values with stack slots.This restriction matches the RISC instruction set of the target processor.
  • Calling conventions: Linear call and return states carry full location maps rather than value lists, with function-call behavior governed by entryfun and exitfun.These functions anticipate later stack-layout and callee-save-register transformations.
  • Spilling and reloading: Spilled pseudo-register uses are reloaded with getstack, and definitions are spilled with setstack operations.The strategy does not reuse reloaded values or delay spilling, reserving 3 integer and 3 float registers for reloaded values and results.
  • Calling conventions: Parallel moves are implemented with elementary moves using at most one temporary register of each kind, and their correctness is proved in Coq.The proof was a particularly difficult part of the development.
  • Semantic preservation: Semantic preservation is proved with a star simulation, whose only possible stuttering case is eliminated because the executing LTLin instruction sequence decreases in length.The proof relates LTLin and Linear states through agreement over non-temporary locations and memory-state relations.

12 Construction of the activation record

This pass maps abstract Linear stack slots to activation-record memory locations and inserts frame-management code. Its correctness proof uses alternate Mach semantics to separate memory-layout reasoning from simulation.

  • Activation-record construction: The activation record allocates space for stack slots, translates slot accesses into memory loads and stores, and adds prologues and epilogues for callee-save registers.Local and outgoing slots belong to the current frame, while incoming slots belong to the caller’s frame.
  • The Mach language: Mach introduces setstack, getstack, and getparent instructions whose offsets identify data within activation records.The new move instructions carry the data type and word offset in the corresponding frame.
  • The Mach language: Mach shares one global processor-register state between caller and callee, so generated prologues and epilogues explicitly save and restore used callee-save registers.Unlike Linear, Mach does not automatically restore these registers at function return.
  • Activation-record construction: The translation first scans Linear code for used stack slots and callee-save registers, then computes frame size and byte offsets for their activation-record areas.The mapping function ∆ assigns offsets to callee-save registers and local and outgoing slots.
  • Activation-record construction: Translation fails when the activation-record frame exceeds 2^31 bytes because signed offsets would overflow.The bound excludes Cminor stack data from the frame-size condition.
  • Semantic preservation: The correctness proof is difficult because it must establish memory separation between frame areas and activation records, so it is divided into two sub-proofs connected by alternate Mach semantics.The alternate semantics stores frame contents in a separate environment Φ rather than memory.
  • Semantic preservation: The two sub-proofs establish a plus simulation from Linear to alternate Mach and a lock-step simulation from alternate to standard Mach semantics.Subject reduction preserves well-typedness, and semantic preservation for activation-record construction follows from both simulations.

13 The output language: PowerPC assembly language

PPC is an abstract syntax and operational semantics for a substantial PowerPC assembly subset, including symbolic labels, linker-resolved constants, macros, and modeled processor state. Its semantics is generally nondeterministic because external calls may return arbitrary values, but deterministic-world behaviors satisfy a qualified uniqueness theorem.

  • PPC syntax: PPC comprises 82 of the PowerPC processor’s 200-plus instructions, together with 7 macro-instructions.The supported instruction set is listed in the paper’s instruction figure.
  • PPC syntax: PPC uses integer and floating-point registers, symbolic labels, and lo16 and hi16 constants for linker-resolved symbol addresses.These constants denote the low-order and high-order 16 bits of a symbol address plus offset.
  • PPC syntax: Macro-instructions expand during pretty-printing into sequences implementing stack-frame allocation, numeric conversions, and floating-point literal loads.They are assembly-language conveniences rather than primitive machine instructions.
  • Operational semantics: PPC states pair memory with modeled processor registers, including integer and floating-point registers, condition bits, PC, LR, and CTR.The register state associates values with these processor components.
  • Operational semantics: The transition function executes one instruction, updates memory and registers, and increments or redirects the program counter for fall-through and branch instructions.Instruction decoding is modeled by reading the instruction addressed by PC.
  • Determinism and behaviors: External calls introduce nondeterminism because their result value is unconstrained, while return control uses the link register to restore the caller’s program counter.The paper distinguishes this external source from apparent nondeterminism in diverging behaviors.
  • Determinism and behaviors: Under a deterministic initial world and minimal traces, any two legal PPC executions have behaviors equal up to bisimilarity of infinite traces.The theorem applies to both executions of the same PPC program.

14 Generation of PowerPC assembly language

The final pass expands Mach instructions into PowerPC instruction sequences while preserving their control-flow and register relationships. Correctness is proved with an option simulation based on program-counter and register-state invariants.

  • Mach-to-PPC translation: Mach conditional branches expand into comparison instructions, sometimes a cror merge, and a bt or bf branch.Mach registers are injected into corresponding PPC integer or floating-point registers.
  • Mach-to-PPC translation: Smart constructors handle PowerPC restrictions such as limited immediate ranges and the special behavior of register R0.Registers R2 and F13 are reserved to support these translations.
  • Mach-to-PPC translation: PPC generation fails when a translated function contains 2^31 or more instructions because signed offsets cannot address every instruction.This is the instruction-count analogue of the activation-record size bound.
  • Semantic preservation: Semantic preservation uses an option simulation whose invariants relate the PPC program counter to the current Mach function and code suffix.The relation requires the PPC code block to contain the translated Mach function and the PC offset to select the corresponding suffix.
  • Semantic preservation: A second invariant requires Mach registers and stack pointer to agree with their associated PPC registers, with R1 serving conventionally as the stack pointer.The matching relation also tracks return addresses through LR and the Mach call stack.

15 The Coq development

The Coq development combines executable compiler definitions with formal specifications and machine-checked proofs. Its substantial size reflects extensive proof scripts, semantic infrastructure, and formalized machine components.

  • Proving in Coq: The development uses Coq for compiler algorithms, specifications, and machine-checked proofs, with proofs developed interactively through tactic scripts.The development also uses automation such as eauto, omega, and congruence, but applying these tactics requires manual goal preparation.
  • Proving in Coq: The development uses function definitions, inductive or coinductive predicates, and ordinary first-order predicates to express specifications and theorems.These styles keep formal statements close to those found in programming-language research papers.
  • Proving in Coq: Two unprovable axioms—function extensionality and proof irrelevance—support the development, while semantic-preservation proofs remain constructive.Classical logic is used only for a separate excluded-middle argument described in the passage.
  • Size of the development: The complete development contains approximately 37,000 lines of Coq and 1,000 lines of Caml, representing approximately 2 person-years of work.The line count excludes comments and blank lines.
  • Size of the development: Compiler definitions account for 14% of the source, while verification is about 6 times larger than the program being verified.The remainder includes specifications, theorem statements, proof scripts, and directives or custom tactics.
  • Size of the development: The most difficult passes require 2,000–3,000 lines each, while simpler passes require fewer than 1,500 lines; PPC code generation exceeds 3,300 lines.Machine integer arithmetic and the memory model require 1,900 and 2,300 lines, respectively.
  • Proving in Coq: Checking all proofs takes about 7.5 minutes of CPU time, or 4.5 minutes of wall-clock time with two-core parallel make.The measurement used a 2.4 GHz Intel Core 2 processor with 4 Gb of RAM and Coq 8.1pl3.

16 Experimental results

The extracted compiler combines verified Coq components with front-end, parsing, heuristic, printing, and driver code to produce PowerPC executables. Benchmarks show adequate generated-code performance, alongside higher but acceptable compilation times than GCC.

  • Extracting an executable compiler: Verified Compcert components are programmed in Coq and automatically extracted to executable Caml code.The executable compiler is combined with a Clight-to-Cminor front-end, a C parser, handwritten heuristic implementations, a PowerPC pretty-printer, and a compiler driver.
  • Extracting an executable compiler: The resulting compiler runs on platforms supported by Caml and generates PowerPC code for MacOS X.Its soundness proof assumes whole-program compilation and does not account for separate compilation, although separate source files can be compiled and linked for testing.
  • Benchmarks: Compcert accepts only a subset of C, so performance evaluation uses a small home-grown suite of 50–3,000-line programs spanning numerical, cryptographic, compression, interpreter, and ray-tracing workloads.Standard benchmark suites could not be used because variadic functions and long long arithmetic types are excluded.
  • Benchmarks: Compcert code is more than twice as fast as GCC without optimizations and averages 7% slower than gcc -O1 and 12% slower than gcc -O2.The authors state that the suite is too small for definitive conclusions, but generated-code performance appears adequate for critical embedded code.
  • Benchmarks: Compcert takes 4.6 s to compile the 3,000-line ray tracer, compared with 2.7 s for gcc -O1.The slowdown is attributed partly to multiple functional passes and purely functional data structures, whose chosen implementations have logarithmic overhead.

17 Discussion and perspectives

The discussion examines Compcert’s portability, optimization scope, memory-model limitations, and unresolved challenges including concurrency and semantic modularity.

  • On retargeting: The back-end was retargeted to ARM, requiring changes for instruction sets, calling conventions, register pressure, spilling, and reloading.The port took about three weeks, followed by three weeks restructuring the Coq development.
  • On retargeting: 76% of the initial 37,500 Coq lines were processor-independent, while 24% were PowerPC-specific and 8,800 additional lines supported ARM.The PowerPC and ARM-specific components were adapted to share exactly the same interface.
  • On optimizations: Compcert prioritizes end-to-end semantic preservation, leaving many interesting optimizations unproved and outside the integrated compiler.Separately verified work addressed instruction scheduling, trace scheduling, and lazy code motion using translation validation.
  • On optimizations: SSA-based optimizations remain difficult to integrate because SSA semantics and its function-wide invariant complicate local proofs.The paper identifies translation validation as a possible way to use SSA algorithms while keeping the validator over conventional representations.
  • On memory: The current memory model assumes successful allocation and deallocation, while stack usage can increase through spilling and undermine resource-sensitive preservation.Heap allocation behavior is preserved, but a source program fitting within N bytes of stack may compile to code exceeding that bound.
  • On memory: A stronger stack theorem may be possible for nonrecursive programs without function pointers, but the issue remains open when recursion or function pointers are used.The proposed approach analyzes the compiled Mach code to approximate its call graph and establish a bound N.
  • On the multiplicity of passes and intermediate languages: Semantic anticipation preserves values needed by later passes, but makes intermediate-language semantics dependent on subsequent transformations.Examples include anticipating callee-save register restoration and the return address stored by generated PPC code.
  • Toward shared-memory concurrency: Naive compilation of racy concurrent programs fails semantic preservation because instruction decomposition and weak hardware memory models introduce additional interleavings.The paper leaves shared-memory concurrency as a challenge for future semantics and proofs.

18 Related work

Related work spans mechanically verified compiler components, full compiler proofs, trusted-code generation, verified analyses, and end-to-end compiler verification in several proof assistants.

  • Mechanized compiler verification: Earlier mechanized proofs covered arithmetic-expression translation and a full compiler for a low-level assembly-style source language.The paper identifies Milner and Weyhrauch’s work as an early mechanically verified semantic-preservation proof and Moore’s as probably the first mechanized full-compiler verification.
  • Verified compilers: Other projects verified compilers from subsets of Common Lisp, Java, functional languages, Pascal-like C0, and HOL specifications to virtual-machine or machine code.These efforts differ in source language, target, degree of automation, optimization support, and proof assistant.
  • Comparison with Compcert: Compared with Compcert, prior work often focused on compiler parts, bytecode rather than actual machine code, or simpler unoptimized compilation.The related projects nevertheless established multiple methodological approaches to machine-checked compiler correctness.
  • Verified analyses: Formal verification of static analyses has developed frameworks for abstract interpretation, dataflow analysis, and bytecode verification that can support compiler optimizations or program safety.The paper situates these analysis-verification efforts as related but distinct from its end-to-end back-end verification.

19 Conclusions

The paper argues that formally verifying a realistic compiler back-end is achievable with machine-checked proofs and elementary semantic and algorithmic techniques. The remaining trust boundary includes the language semantics, extraction and compilation chain, and Coq itself, while ongoing work aims to reduce it further.

  • Conclusions: The verified back-end provides strong evidence that formally verifying a realistic compiler is achievable within current proof assistants.The development uses elementary semantic and algorithmic approaches.
  • Conclusions: The work also contributes to renewed interest in mechanized operational semantics and integrated environments for programming and proving.This is presented as an additional contribution within the broader research area of formally certified software toolchains.
  • Remaining trust assumptions: Trust in the complete compiler is reduced to trusting the Cminor and PPC semantics, Coq extraction and the OCaml compiler, and the Coq proof assistant.The paper does not claim to eliminate every uncertainty about compiler soundness.
  • Future confidence building: Verifying Coq extraction and a Mini-ML-to-Cminor compiler could eventually create a more trusted execution path for Coq-written and Coq-verified programs.The paper describes this as ongoing work intended to increase confidence through bootstrapping.
  • Remaining trust assumptions: The main uncertainty concerns whether the formal Cminor and PPC semantics and memory model capture intended behaviors.The paper suggests manual review and reuse in other formal verifications as ways to increase confidence.
Loading 0902.2137v3…