research-article

A simple, verified validator for software pipelining

Authors:

Jean-Baptiste Tristan,

Xavier LeroyAuthors Info & Claims

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

Pages 83 - 92

https://doi.org/10.1145/1706299.1706311

Published: 17 January 2010 Publication History

Abstract

Software pipelining is a loop optimization that overlaps the execution of several iterations of a loop to expose more instruction-level parallelism. It can result in first-class performance characteristics, but at the cost of significant obfuscation of the code, making this optimization difficult to test and debug. In this paper, we present a translation validation algorithm that uses symbolic evaluation to detect semantics discrepancies between a loop and its pipelined version. Our algorithm can be implemented simply and efficiently, is provably sound, and appears to be complete with respect to most modulo scheduling algorithms. A conclusion of this case study is that it is possible and effective to use symbolic evaluation to reason about loop transformations.

References

[1]

A. V. Aho, M. Lam, R. Sethi, and J. D. Ullman. Compilers: principles, techniques, and tools. Addison-Wesley, second edition, 2006.

Digital Library

[2]

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

Digital Library

[3]

C. W. Barret, Y. Fang, B. Goldberg, Y. Hu, A. Pnueli, and L. Zuck. TVOC: A translation validator for optimizing compilers. In Computer Aided Verification, 17th Int. Conf., CAV 2005, volume 3576 of LNCS, pages 291--295. Springer, 2005.

Digital Library

[4]

J. M. Codina, J. Llosa, and A. González. A comparative study of modulo scheduling techniques. In Proc. of the 16th international conference on Supercomputing, pages 97--106. ACM, 2002.

Digital Library

[5]

B. Goldberg, E. Chapman, C. Huneycutt, and K. Palem. Software bubbles: Using predication to compensate for aliasing in software pipelines. In 2002 International Conference on Parallel Architectures and Compilation Techniques (PACT 2002), pages 211--221. IEEE Computer Society Press, 2002.

Digital Library

[6]

Y. Huang, B. R. Childers, and M. L. Soffa. Catching and identifying bugs in register allocation. In Static Analysis, 13th Int. Symp., SAS 2006, volume 4134 of LNCS, pages 281--300. Springer, 2006.

Digital Library

[7]

R. A. Huff. Lifetime-sensitive modulo scheduling. In Proc. of the ACM SIGPLAN '93 Conf. on Programming Language Design and Implementation, pages 258--267. ACM, 1993.

Digital Library

[8]

A. Kanade, A. Sanyal, and U. Khedker. A PVS based framework for validating compiler optimizations. In SEFM '06: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, pages 108--117. IEEE Computer Society, 2006.

Digital Library

[9]

S. Kundu, Z. Tatlock, and S. Lerner. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 2009 Conference on Programming Language Design and Implementation (PLDI 2009), pages 327--337. ACM Press, 2009.

Digital Library

[10]

M. Lam. Software pipelining: An effective scheduling technique for VLIW machines. In Proc. of the ACM SIGPLAN '88 Conf. on Programming Language Design and Implementation, pages 318--328. ACM, 1988.

Digital Library

[11]

X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107--115, 2009.

Digital Library

[12]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 2009. To appear.

Digital Library

[13]

X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1--31, 2008.

Digital Library

[14]

R. Leviathan and A. 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

[15]

J. Llosa, A. González, E. Ayguadé, and M. Valero. Swing modulo scheduling: A lifetime-sensitive approach. In IFIP WG10.3 Working Conference on Parallel Architectures and Compilation Techniques, pages 80--86, 1996.

Digital Library

[16]

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

Digital Library

[17]

M. O. Myreen and M. J. C. Gordon. Transforming programs into recursive functions. In Brazilian Symposium on Formal Methods (SBMF 2008), volume 240 of ENTCS, pages 185--200. Elsevier, 2009.

Digital Library

[18]

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

Digital Library

[19]

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

[20]

A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98, volume 1384 of LNCS, pages 151--166. Springer, 1998.

Digital Library

[21]

W. Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Supercomputing '91: Proceedings of the 1991 ACM/IEEE conference on Supercomputing, pages 4--13. ACM Press, 1991.

Digital Library

[22]

B. R. Rau. Iterative modulo scheduling. International Journal of Parallel Processing, 24(1):1--102, 1996.

[23]

B. R. Rau, M. S. Schlansker, and P. P. Timmalai. Code generation schema for modulo scheduled loops. Technical Report HPL-92-47, Hewlett-Packard, 1992.

[24]

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

Digital Library

[25]

R. Tate, M. Stepp, Z. Tatlock, and S. Lerner. Equality saturation: a new approach to optimization. In 36th symposium Principles of Programming Languages, pages 264--276. ACM Press, 2009.

Digital Library

[26]

J.-B. Tristan and X. Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In 35th symposium Principles of Programming Languages, pages 17--27. ACM Press, 2008.

Digital Library

[27]

J.-B. Tristan and X. Leroy. Verified validation of Lazy Code Motion. In Proceedings of the 2009 Conference on Programming Language Design and Implementation (PLDI 2009), pages 316--326. ACM Press, 2009.

Digital Library

[28]

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

[29]

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

Digital Library

Cited By

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
Li XLiang HFeng X(2024)Verified Validation for Affine Scheduling in Polyhedral CompilationTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_17(287-305)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_17
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
Show More Cited By

Index Terms

A simple, verified validator for software pipelining
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

Recommendations

A simple, verified validator for software pipelining
POPL '10

Software pipelining is a loop optimization that overlaps the execution of several iterations of a loop to expose more instruction-level parallelism. It can result in first-class performance characteristics, but at the cost of significant obfuscation of ...
Single-dimension software pipelining for multidimensional loops

Traditionally, software pipelining is applied either to the innermost loop of a given loop nest or from the innermost loop to outer loops. This paper proposes a three-step approach, called single-dimension software pipelining (SSP), to software pipeline ...
Software Pipelining Irregular Loops On the TMS320C6000 VLIW DSP Architecture
LCTES '01: Proceedings of the ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems

The TMS320C6000 architecture is a leading family of Digital Signal Processors (DSPs). To achieve peak performance, this VLIW architecture relies heavily on software pipelining. Traditionally, software pipelining has been restricted to regular (FOR) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 2010

520 pages

ISBN:9781605584799

DOI:10.1145/1706299

General Chair:
Manuel Hermenegildo
IMDEA-Software and T.U. of Madrid, Spain
,
Program Chair:
Jens Palsberg
UCLA, University of California, Los Angeles

ACM SIGPLAN Notices Volume 45, Issue 1
POPL '10
January 2010
500 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1707801
Issue’s Table of Contents

Copyright © 2010 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

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '10

Sponsor:

SIGPLAN

POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 17 - 23, 2010

Madrid, Spain

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

47
Total Citations
View Citations
486
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Li XLiang HFeng X(2024)Verified Validation for Affine Scheduling in Polyhedral CompilationTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_17(287-305)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_17
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
Desharnais MBrunthaler SHriţcu CPopescu A(2021)Towards efficient and verified virtual machines for dynamic languagesProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439923(61-75)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439923
Courant NLeroy X(2021)Verified code generation for the polyhedral modelProceedings of the ACM on Programming Languages10.1145/34343215:POPL(1-24)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434321
Wiesner MJakobs M(2021)Verifying Pipeline Implementations in OpenMPModel Checking Software10.1007/978-3-030-84629-9_5(81-98)Online publication date: 3-Aug-2021
https://doi.org/10.1007/978-3-030-84629-9_5
Parthasarathy GMüller PSummers A(2021)Formally Validating a Practical Verification Condition GeneratorComputer Aided Verification10.1007/978-3-030-81688-9_33(704-727)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_33
Brocanelli MWang X(2019)SODACM Transactions on Autonomous and Adaptive Systems10.1145/327552113:3(1-24)Online publication date: 15-Mar-2019
https://dl.acm.org/doi/10.1145/3275521
Becker HDarulova EMyreen MTatlock Z(2019)Icing: Supporting Fast-Math Style Optimizations in a Verified CompilerComputer Aided Verification10.1007/978-3-030-25543-5_10(155-173)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_10
Kang JKim YSong YLee JPark SShin MKim YCho SChoi JHur CYi K(2018)Crellvm: verified credible compilation for LLVMACM SIGPLAN Notices10.1145/3296979.319237753:4(631-645)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192377
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