research-article

Formal verification of translation validators: a case study on instruction scheduling optimizations

Authors:

Jean-Baptiste Tristan,

Xavier LeroyAuthors Info & Claims

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 17 - 27

https://doi.org/10.1145/1328438.1328444

Published: 07 January 2008 Publication History

Abstract

Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of itssemantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The validators are designed for two instruction scheduling optimizations: list scheduling and trace scheduling.

References

[1]

Andrew W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998.

Digital Library

[2]

Clark W. Barret, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck. TVOC: A translation validator for optimizing compilers. In Computer Aided Verification, 17th Int. Conf., CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 291--295. Springer, 2005.

Digital Library

[3]

Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In Functional and Logic Programming, 8th Int. Symp., FLOPS 2006, volume 3945 of Lecture Notes in Computer Science, pages 114--129. Springer, 2006.

Digital Library

[4]

Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, 2004.

Digital Library

[5]

David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 342(1):56--78, 2005.

Digital Library

[6]

Coq development team. The Coq proof assistant. Software and documentation available at http://coq.inria.fr/, 1989--2007.

[7]

Maulik A. Dave. Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes, 28(6):2--2, 2003.

Digital Library

[8]

John R. Ellis. Bulldog: a compiler for VLSI architectures. ACM Doctoral Dissertation Awards. The MIT Press, 1986.

[9]

Benjamin Goldberg, Lenore Zuck, and Clark Barret. Into the loops: Practical issues in translation validation for optimizing compilers. In Proc. Workshop Compiler Optimization Meets Compiler Verification (COCV 2004), volume 132 of Electronic Notes in Theoretical Computer Science, pages 53--71. Elsevier, 2005.

Digital Library

[10]

Yuqiang Huang, Bruce R. Childers, and Mary Lou Soffa. Catching and identifying bugs in register allocation. In Static Analysis, 13th Int. Symp., SAS 2006, volume 4134 of Lecture Notes in Computer Science, pages 281--300. Springer, 2006.

Digital Library

[11]

Gerwin Klein and Tobias Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 298(3):583--626, 2003.

Digital Library

[12]

Gerwin Klein and Tobias Nipkow. A machine-checked model for a Javalike language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems, 28(4):619--695, 2006.

Digital Library

[13]

D. Leinenbach, W. Paul, and E. Petrova. Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In Int. Conf. on Software Engineering and Formal Methods (SEFM 2005), pages 2--11. IEEE Computer Society Press, 2005.

Digital Library

[14]

Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languages, pages 42--54. ACM Press, 2006.

Digital Library

[15]

Xavier Leroy et al. The Compcert certified compiler back-end. Development available at http://gallium.inria.fr/~xleroy/ compcert-backend/, 2003--2007.

[16]

Raya Leviathan and Amir Pnueli. Validating software pipelining optimizations. In Int. Conf. On Compilers, Architecture, And Synthesis For Embedded Systems (CASES 2002), pages 280--287. ACM Press, 2006.

Digital Library

[17]

Steven S. Muchnick. Advanced compiler design and implementation. Morgan Kaufmann, 1997.

Digital Library

[18]

George C. Necula. Translation validation for an optimizing compiler. In Programming Language Design and Implementation 2000, pages 83--95. ACM Press, 2000.

Digital Library

[19]

Amir Pnueli, Ofer Shtrichman, and Michael Siegel. The code validation tool (CVT) - automatic verification of a compilation process. International Journal on Software Tools for Technology Transfer, 2:192--201, 1998a.

[20]

Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98, volume 1384 of Lecture Notes in Computer Science, pages 151--166. Springer, 1998b.

Digital Library

[21]

Xavier Rival. Symbolic transfer function-based approaches to certified compilation. In 31st symposium Principles of Programming Languages, pages 1--13. ACM Press, 2004.

Digital Library

[22]

Emin Gun Sirer and Brian N. Bershad. Testing Java virtual machines. In Proc. Int. Conf. on Software Testing And Review, 1999.

[23]

Martin Strecker. Compiler verification for C0. Technical report, Université Paul Sabatier, Toulouse, April 2005.

[24]

L. Zuck, A. Pnueli, and R. Leviathan. Validation of optimizing compilers. Technical Report MCS01-12, Weizmann institute of Science, 2001.

Digital Library

[25]

Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A methodology for translation validation of optimizing compilers. Journal of Universal Computer Science, 9(3):223--247, 2003.

Cited By

Yang ZShirako JSarkar V(2024)Fully Verified Instruction SchedulingProceedings of the ACM on Programming Languages10.1145/36897398:OOPSLA2(791-816)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689739
Herklotz YWickerson J(2024)Hyperblock Scheduling for Verified High-Level SynthesisProceedings of the ACM on Programming Languages10.1145/36564558:PLDI(1929-1953)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656455
Parthasarathy GDardinier TBonneau BMüller PSummers A(2024)Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification LanguageProceedings of the ACM on Programming Languages10.1145/36564388:PLDI(1510-1534)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656438
Show More Cited By

Index Terms

Formal verification of translation validators: a case study on instruction scheduling optimizations
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics
      1. Operational semantics

Recommendations

Verified validation of lazy code motion
PLDI '09

Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, we develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is ...
Formal verification of translation validators: a case study on instruction scheduling optimizations
POPL '08

Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of itssemantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We ...
Verified validation of lazy code motion
PLDI '09: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation

Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, we develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2008

448 pages

ISBN:9781595936899

DOI:10.1145/1328438

General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

ACM SIGPLAN Notices Volume 43, Issue 1
POPL '08
January 2008
420 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1328897
Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL08

Sponsor:

POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 7 - 12, 2008

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

72
Total Citations
View Citations
690
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)6

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yang ZShirako JSarkar V(2024)Fully Verified Instruction SchedulingProceedings of the ACM on Programming Languages10.1145/36897398:OOPSLA2(791-816)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689739
Herklotz YWickerson J(2024)Hyperblock Scheduling for Verified High-Level SynthesisProceedings of the ACM on Programming Languages10.1145/36564558:PLDI(1929-1953)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656455
Parthasarathy GDardinier TBonneau BMüller PSummers A(2024)Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification LanguageProceedings of the ACM on Programming Languages10.1145/36564388:PLDI(1510-1534)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656438
Monniaux DTimany ATraytel DPientka BBlazy S(2024)Memory Simulations, Security and Optimization in a Verified CompilerProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636952(103-117)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636952
Wang YXie FYang ZCasas JCocchini PYang J(2023)An Automated Verification Framework for HalideIR-Based Compiler Transformations2023 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE56975.2023.10137308(1-6)Online publication date: Apr-2023
https://doi.org/10.23919/DATE56975.2023.10137308
Gourdin LBonneau BBoulmé SMonniaux DBérard A(2023)Formally Verifying Optimizations with Block SimulationsProceedings of the ACM on Programming Languages10.1145/36227997:OOPSLA2(59-88)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622799
Monniaux DGourdin LBoulmé SLebeltel O(2023)Testing a Formally Verified CompilerTests and Proofs10.1007/978-3-031-38828-6_3(40-48)Online publication date: 20-Jul-2023
https://doi.org/10.1007/978-3-031-38828-6_3
Albert EGenaim SKirchner DMartin-Martin E(2023)Formally Verified EVM Block-OptimizationsComputer Aided Verification10.1007/978-3-031-37709-9_9(176-189)Online publication date: 17-Jul-2023
https://doi.org/10.1007/978-3-031-37709-9_9
Pit-Claudel CPhilipoom JJamner DErbsen AChlipala AJhala RDillig I(2022)Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level codeProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523706(918-933)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523706
Six CGourdin LBoulmé SMonniaux DFasse JNardino NPopescu AZdancewic S(2022)Formally verified superblock schedulingProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503679(40-54)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503679
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents