research-article

Open access

Certified and efficient instruction scheduling: application to interlocked VLIW processors

Authors:

Sylvain Boulmé,

David MonniauxAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA

Article No.: 129, Pages 1 - 29

https://doi.org/10.1145/3428197

Published: 13 November 2020 Publication History

Abstract

CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics, and did not attempt reordering instructions for optimization.

We present here a CompCert backend for a VLIW core (i.e. with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.

Supplementary Material

Auxiliary Presentation Video (oopsla20main-p14-p-video.mp4)

CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics, and did not attempt reordering instructions for optimization. We present here a CompCert backend for a VLIW core (i.e. with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.

Download
22.09 MB

References

[1]

Gergö Barany. 2018. A more precise, more correct stack and register model for CompCert. In LOLA 2018-Syntax and Semantics of Low-Level Languages 2018. Oxford, United Kingdom. https://hal.inria.fr/hal-01799629

[2]

Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2012. Formally verified optimizing compilation in ACG-based flight control software. In Embedded Real Time Software and Systems (ERTS2). AAAF, SEE. arXiv: hal-00653367

[3]

Armin Biere. 2008. PicoSAT Essentials. JSAT 4 ( 01 2008 ), 75-97.

[4]

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. 2006. Formal Verification of a C Compiler Front-End. In FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4085 ). Springer, 460-475. https://doi.org/10.1007/11813040_31

Digital Library

[5]

Gabriel Hjort Blindell, Mats Carlsson, Roberto Castañeda Lozano, and Christian Schulte. 2017. Complete and Practical Universal Instruction Selection. ACM Trans. Embedded Comput. Syst. 16, 5 ( 2017 ), 119 : 1-119 : 18. https://doi.org/10.1145/ 3126528

Digital Library

[6]

Sylvain Boulmé and Thomas Vandendorpe. 2019. Embedding Untrusted Imperative ML Oracles into Coq Verified Code. (March 2019 ). https://hal.archives-ouvertes.fr/hal-02062288 preprint.

[7]

Roberto Castañeda Lozano, Mats Carlsson, Gabriel Hjort Blindell, and Christian Schulte. 2019. Combinatorial Register Allocation and Instruction Scheduling. Transactions on Programming Languages and Systems (April 2019 ). arXiv: 1804.02452 https://chschulte.github.io/papers/castanedacarlssonea-toplas-2019.html Accepted for publication.

Digital Library

[8]

Benoît Dupont de Dinechin. 2004. From Machine Scheduling to VLIW Instrution Scheduling. ST Journal of Research 1, 2 ( September 2004 ), 1-35. https://www.cri.ensmp.fr/classement/doc/A-352.ps Also as Mines ParisTech research article A/352/CRI.

[9]

Heiko Falk, Sebastian Altmeyer, Peter Hellinckx, Björn Lisper, Wolfgang Pufitsch, Christine Rochange, Martin Schoeberl, Rasmus Bo Sørensen, Peter Wägemann, and Simon Wegener. 2016. TACLeBench: A Benchmark Collection to Support Worst-Case Execution Time Research. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016 ) (OpenAccess Series in Informatics (OASIcs), Vol. 55 ), Martin Schoeberl (Ed.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2 : 1-2 : 10.

[10]

Paul Feautrier. 1991. Dataflow analysis of array and scalar references. International Journal of Parallel Programming 20, 1 ( 1991 ), 23-53. https://doi.org/10.1007/BF01407931

[11]

Jean-Christophe Filliâtre and Sylvain Conchon. 2006. Type-safe modular hash-consing. In Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006. ACM, 12-19. https://doi.org/10.1145/1159876.1159880

Digital Library

[12]

Joseph A. Fisher. 1981. Trace Scheduling: A Technique for Global Microcode Compaction. IEEE Trans. Comput. 30, 07 (jul 1981 ), 478-490. https://doi.org/10.1109/TC. 1981.1675827

Digital Library

[13]

Joseph A. Fisher. 1983. Very Long Instruction Word Architectures and the ELI-512. In Proceedings of the 10th Annual Symposium on Computer Architecture, 1983. ACM Press, 140-150.

Digital Library

[14]

Joseph A. Fisher, Paolo Faraboschi, and Clif Young. 2005. Embedded Computing: A VLIW Approach to Architecture, Compilers and Tools. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.

Digital Library

[15]

Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2011. Towards Formally Verified Optimizing Compilation in Flight Control Software. In Bringing Theory to Practice: Predictability and Performance in Embedded Systems, DATE Workshop PPES 2011, March 18, 2011, Grenoble, France. (OASICS, Vol. 18 ), Philipp Lucas, Lothar Thiele, Benoit Triquet, Theo Ungerer, and Reinhard Wilhelm (Eds.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Germany, 59-68. https://doi.org/10.4230/OASIcs.PPES. 2011.59

[16]

Jean-Loup Gailly and Mark Adler. 2017. zlib. https://www.zlib.net/

[17]

Torbjörn Granlund and Peter L. Montgomery. 1994. Division by Invariant Integers using Multiplication. In Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida, USA, June 20-24, 1994, Vivek Sarkar, Barbara G. Ryder, and Mary Lou Sofa (Eds.). ACM, 61-72. https://doi.org/10.1145/178243.178249

Digital Library

[18]

Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. In ERTS2 2018-9th European Congress Embedded Real-Time Software and Systems. 3AF, SEE, SIE, Toulouse, France, 1-9. https://hal.inria.fr/hal-01643290

[19]

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 ( 1976 ), 385-394. https://doi.org/10. 1145/360248.360252

Digital Library

[20]

Monica S. Lam. 1988. Software Pipelining: An Efective Scheduling Technique for VLIW Machines. In Programming Language Design and Implementation (PLDI). ACM Press.

[21]

Tom Lane and the Independent JPEG Group (IJG). 1998. Libjpeg. http://libjpeg.sourceforge.net/

[22]

Xavier Leroy. 2009a. Formal verification of a realistic compiler. Commun. ACM 52, 7 ( 2009 ). arXiv: inria-00415861

[23]

Xavier Leroy. 2009b. A formally verified compiler back-end. Journal of Automated Reasoning 43, 4 ( 2009 ), 363-446. http://xavierleroy.org/publi/compcert-backend.pdf

Digital Library

[24]

Xavier Leroy. 2017. How I found a crash bug with hyperthreading in Intel's Skylake processors. https://thenextweb.com/ contributors/2017/07/05/found-crash-bug-hyperthreading-intels-skylake-processors/

[25]

P. Geofrey Lowney, Stefan M. Freudenberger, Thomas J. Karzes, W. D. Lichtenstein, Robert P. Nix, John S. O'Donnell, and John Ruttenberg. 1993. The Multiflow Trace Scheduling Compiler. J. Supercomput. 7, 1-2 (May 1993 ), 51-142. https://doi.org/10.1007/BF01205182

Digital Library

[26]

Andrey Makhorin. 2012. GNU Linear Programming Kit. Free Software Foundation. https://www.gnu.org/software/glpk/

[27]

Giovanni De Micheli. 1994. Synthesis and Optimization of Digital Circuits. McGraw-Hill.

[28]

Alain Mosnier. 2019. SHA-256 implementation. https://github.com/amosnier/sha-2

[29]

Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman. 2016. Verified peephole optimizations for CompCert. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery Berger (Eds.). ACM, 448-461. https: //doi.org/10.1145/2908080.2908109

Digital Library

[30]

Conor Patrick. 2015. Bitsliced AES implementation. https://github.com/conorpp/bitsliced-aes

[31]

Louis-Noël Pouchet. 2012. the Polyhedral Benchmark suite. http://web.cs.ucla.edu/~pouchet/software/polybench/

[32]

B. Ramakrishna Rau, Christopher D. Glaeser, and Raymond L. Picard. 1982. Eficient code generation for horizontal architectures: Compiler techniques and architectural support. In 9th International Symposium on Computer Architecture (ISCA 1982 ), Austin, TX, USA, April 26-29, 1982. IEEE Computer Society, 131-139. https://dl.acm.org/citation.cfm?id= 801721

[33]

Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: a Case Study on Instruction Scheduling Optimizations. In Principles of Programming Languages (POPL). ACM Press, 17-27.

[34]

Jean-Baptise Tristan. 2009. Formal verification of translation validators. Ph.D. Dissertation. Université Paris 7 Diderot.

[35]

Jean-Baptiste Tristan and Xavier Leroy. 2010. A simple, verified validator for software pipelining. In Principles of Programming Languages (POPL). ACM Press, 83-92. http://gallium.inria.fr/~xleroy/publi/validation-softpipe.pdf

[36]

Lewis Van Winkle. 2018. Genann-minimal artificial neural network. https://github.com/codeplea/genann

[37]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Programming Language Design and Implementation (PLDI). ACM Press, 283-294.

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
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
Wei ZYu JRen JDuan WWu D(2024)Progressive Simulated Annealing Algorithm for the Pipeline Allocation Problem of Protocol Independent Switch Architecture Chips2024 6th International Conference on Data-driven Optimization of Complex Systems (DOCS)10.1109/DOCS63458.2024.10704552(243-249)Online publication date: 16-Aug-2024
https://doi.org/10.1109/DOCS63458.2024.10704552
Show More Cited By

Index Terms

Recommendations

Formally verified superblock scheduling
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks ...
An evaluation of speculative instruction execution on simultaneous multithreaded processors

Modern superscalar processors rely heavily on speculative execution for performance. For example, our measurements show that on a 6-issue superscalar, 93% of committed instructions for SPECINT95 are speculative. Without speculation, processor resources ...
Machine-Description Driven Compilers for EPIC and VLIW Processors

In the past, due to the restricted gate count available on an inexpensive chip, embedded DSPs have had limited parallelism, few registers and irregular, incomplete interconnectivity. More recently, with increasing levels of integration, embedded VLIW ...

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue OOPSLA

November 2020

3108 pages

EISSN:2475-1421

DOI:10.1145/3436718

Issue’s Table of Contents

Copyright © 2020 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 November 2020

Published in PACMPL Volume 4, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
1,196
Total Downloads

Downloads (Last 12 months)526
Downloads (Last 6 weeks)51

Reflects downloads up to 15 Jan 2025

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
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
Wei ZYu JRen JDuan WWu D(2024)Progressive Simulated Annealing Algorithm for the Pipeline Allocation Problem of Protocol Independent Switch Architecture Chips2024 6th International Conference on Data-driven Optimization of Complex Systems (DOCS)10.1109/DOCS63458.2024.10704552(243-249)Online publication date: 16-Aug-2024
https://doi.org/10.1109/DOCS63458.2024.10704552
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00760-3
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
Gourdin LJul ERacordon D(2023)Lazy Code Transformations in a Formally Verified CompilerProceedings of the 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3605158.3605848(3-14)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1145/3605158.3605848
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: 18-Jul-2023
https://dl.acm.org/doi/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
Monniaux DSix C(2022)Formally Verified Loop-Invariant Code Motion and Assorted OptimizationsACM Transactions on Embedded Computing Systems10.1145/352950722:1(1-27)Online publication date: 13-Dec-2022
https://dl.acm.org/doi/10.1145/3529507
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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents