Have Your Verified Compiler And Extend It Too
Verified compilers ensure correctness and extensibility in compiler systems, addressing complex interactions and bugs commonly found in traditional compilers. By implementing compilers in a proof assistant and proving their correctness interactively, stronger guarantees of correctness are achieved. DSL-based compilers offer domain-specific language optimizations with automatic proven correctness. The contribution of adding a DSL execution engine enhances extensibility and correctness proof, while the bulk of development efforts focus on formal correctness proofs in Coq. Challenges and evaluations for extensible and correct compilers are also explored.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Have Your Verified Compiler And Extend It Too Zachary Tatlock Sorin Lerner UC San Diego
Compiler Correctness Building robust compilers is difficult complex interactions resist testing Compiler bugs are contagious invalidate source level guarantees Few users extend their compiler hand optimized, unreadable code
Verified Compilers Implement compiler in proof assistant Prove compiler correct interactively CompCert [Leroy], Lambda Tamer [Chlipala] Strong Guarantee Difficult to Extend
DSL-based Compilers Domain Specific Language for optimizations DSL opts proven correct automatically Rhodium [POPL 05], PEC [PLDI 09] Easier to Extend Weaker Guarantee
Contribution Add DSL Execution Engine + Correctness Proof Extensibility stronger guarantee CompCert CompCert XCert Reduce TCB weaker guarantee PEC PEC harder to extend easier to extend
Extensible & Correct Compiler Correct Compiler XCert Correct ? Formal Correctness Proof in Coq Rewrite Rule Main Theorem Proved in Coq : Rewrite PEC XCert Rules Locally Correct Locally Correct ? [PLDI 09] CompCert ? Bulk of the development effort XCert CompCert C Asm
Extensible & Correct Compiler Rewrite Rule 1 PEC [PLDI 09] CompCert XCert 2 3 Challenges and Evaluation C Asm
[PLDI 09] PEC Rewrite Rule while(C ) while(C ) Find & Replace I ++ I += 2 Match Pattern I ++ x < 10 I x Apply Subst C x = 0 x = 0 while(x < 10) while(x < 10) x ++ x += 2 x ++ return x return x
[PLDI 09] PEC A A PEC Checker while(C ) while(C ) 1.Convert to CFG C C C I ++ I += 2 C !C 2.Guess Sync Points !C I ++ I ++ I ++ I +=2 I +=2 3.Check w/ SMT I ++ I ++ SMT Checked B A A A A B
PEC XCert Module A 1.Rule in Coq 2.SMT Checks B SMT Checked A A A B
Extensible & Correct Compiler Rewrite Rule 1 PEC [PLDI 09] XCert 2 3 Challenges and Evaluation
XCert Correctness Proof S Small Step Execute instruction Step state S to S S
XCert Correctness Proof Equivalent Executions Initial Equiv Final Equiv Prove Simulation Diagram L R L R CompCert Small Step Library: L ~ R < R : R R L L ? Sim Diagram Progs Equiv < L ~ R
XCert Simulation Diagram XCert Module A A A B A SMT Checked A A A B B
Extensible & Correct Compiler Rewrite Rule 1 PEC [PLDI 09] XCert 2 3 Challenges and Evaluation
Challenges (see paper) XCert Execution Engine CFG pattern matching CFG splicing XCert Correctness Proof Managing case explosion Verified validation [Tristan and Leroy] Preserving non-terminating behaviors
Evaluation Engine : 1,000 lines of Coq functional code Proof : 3,000 lines of Coq proof script Trusted Computing Base (TCB) Compcert : Coq + Coq encoding of C sem XCert adds : SMT + SMT encoding of C sem
Evaluation Extensibility: Support PEC Opts [PLDI 09] No manual proof effort or TCB increase Maintain Compcert end-to-end correctness Sample of Optimizations Run: Loop Invariant Code Hoist Loop Peeling Software Pipelining Conditional Speculation Loop Unswitching Partial Redundancy Elim
Extensible & Correct Compiler Rewrite Rule 1 PEC [PLDI 09] XCert 2 Thank You!
