Formal Verification of Just-In-Time Compilation.

Format:

Book

Author/Creator:

Barrière, Aurèle.

Series:

ACM Bks.

Language:

English

Subjects (All):

Formal methods (Computer science).

Just-in-time systems.

Physical Description:

1 online resource (179 pages)

Edition:

1st ed.

Place of Publication:

New York : Morgan & Claypool Publishers, 2025.

Summary:

This book outlines a methodology to develop formally verified Just-in-Time compilers. Just-in-Time compilation is a technique to execute programs, where execution is interleaved with optimizations of the program itself. These compilers often produce fast executions, so much so that their use has grown greatly for dynamic programming languages. Most modern web browsers today use Just-in-Time compilation to speed up the execution of the JavaScript programs they execute.

Contents:

Intro

Formal Verification of Just-in-Time Compilation

Contents

Preface

Acknowledgments

1 Introduction

1.1 Motivation

1.2 Contributions

1.2.1 Four JIT-Specific Verification Challenges

1.2.2 Collaborations and Publications

1.3 Outline

2 Background on Just-in-Time Compilation

2.1 Speculation in Just-in-Time Compilers

2.1.1 Speculative Optimization Example

2.1.2 Deoptimization and On-stack Replacement

2.2 Various JIT Designs

2.3 Related Work on JIT Formalization

3 Background on the CompCert Compiler

3.1 A Formally Verified C Compiler

3.1.1 CompCert Optimizations

3.1.2 The CompCert Theorem

3.2 The Simulation Framework of CompCert

4 Designing Formally Verified JITs

4.1 A Formalized JIT Architecture

4.2 JITs as Coq State Machines

4.3 Profiling as External Heuristics

4.4 A JIT Correctness Theorem

4.5 Dynamic Optimizations

4.5.1 The Nested Simulations Technique

4.5.2 Proving the External Backward Simulation

4.5.3 A JIT Optimizer Specification

5 Formally Verified Speculative Optimizations

5.1 CoreIR, an IR with Speculation

5.1.1 CoreIR Syntax

5.1.2 CoreIR Semantics

5.2 Manipulating Speculative Instructions

5.2.1 Anchor Insertion

5.2.2 Assume Insertion

5.2.3 Constant Propagation

5.2.4 Removing Anchors

5.2.5 Delayed Assume Insertion

5.2.6 Inlining with Speculations

5.3 Formal Verification of Speculation Manipulation

5.3.1 Correctness of Anchor Insertion

5.3.2 Correctness of Assume Insertion

5.3.3 Correctness of Constant Propagation

5.3.4 Correctness of Removing Anchors

5.3.5 Correctness of Delayed Assume Insertion

5.3.6 Correctness of Inlining with Speculations

5.4 A Formally Verified JIT Middle-end Compiler

6 Formal Verification of Impure Coq JITs

6.1 A Monadic Encoding for Impure JITs.

6.1.1 The Need for a New Extraction Methodology

6.1.2 JITs as Incomplete Coq Programs

6.1.3 A Minimal Interface of JIT Impure Primitives

6.2 An Existing Solution for Specifying Effects: State and Error Monads

6.3 A Solution to Write Impure JITs in Coq: Free Monads

6.4 Monadic Specifications and Semantics of Free Monads

6.5 An Impure Implementation for an Effectful JIT

6.6 Facilitating the Correctness Proofs with Refinement

6.7 Nonatomicity of Transitions: Small-step Semantics of x86 to the Rescue

6.8 Related Work on Impure Program Verification

7 Formal Verification of a JIT Backend Compiler

7.1 Splitting RTL Programs to Directly Reuse CompCert Proofs

7.2 Mixed Semantics: Interleaving Pieces of Executions Related to Multiple Languages

7.3 Correctness of RTL Generation

7.4 Correctness of Native Code Generation

7.5 A Formally Verified JIT Backend Compiler

8 Assessment

8.1 Composing all Simulations

8.2 Trusted Code Base

8.3 Our Coq JIT Implementation

8.3.1 Implementation and Proof Reuse

8.3.2 Our C Library of Impure Primitives

8.3.3 Evaluation

9 Conclusion

9.1 Summary

9.2 Perspectives

9.2.1 Recompilation and Contextual Dispatch

9.2.2 Direct Calls and Built-ins

9.2.3 Formally Verified JITs for Realistic Languages

Relating the Developments to the Book

Bibliography

Author's Biography

Index.

Notes:

Description based on publisher supplied metadata and other sources.

Part of the metadata in this record was created by AI, based on the text of the resource.

ISBN:

9798400713804

OCLC:

1496392216