Article

Validating software pipelining optimizations

Authors:

Raya Leviathan,

Amir PnueliAuthors Info & Claims

CASES '02: Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems

Pages 280 - 287

https://doi.org/10.1145/581630.581676

Published: 08 October 2002 Publication History

Abstract

The paper presents a method for translation validation of a specific optimization, software pipelining optimization, used to increase the instruction level parallelism in EPIC type of architectures. Using a methodology as in [15] to establish simulation relation between source and target based on computational induction, we describe an algorithm that automatically produces a set of decidable proof obligations. The paper also describes SPV, a prototype translation validator that automatically produces verification conditions for software pipelining optimizations of the SGI Pro-64 compiler. These verification conditions are further checked automatically by the CVC [12] checker.

References

[1]

V. Allan, R. Jones, R. Lee, and S. Allan. Software pipelining. ACM Computing Surveys, 27(3):368--432, September 1995.]]

Digital Library

[2]

N. Bjorner, A. Browne, M. Colon, B. Finkbeiner, Z. Manna, M. P. H. B. Simpa, and T. Uribe. step The Stanford Temporal Prover Educational Release. Computer Science Department, Stanford University, July 1998.]]

Digital Library

[3]

K. Engelhardt, W.-P. de Roever, et al. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1999.]]

Digital Library

[4]

J.-C. Filliåtre, SamOwre, H. Rueß, and N. Shanka. ICS: Integrated canonizer and solver. In Proc. 13th Intl. Conference on Computer Aided Verification (CAV'01), 2001.]]

Digital Library

[5]

S. Glenser, R. Geiß, and B. Boesler. Verified code generation for embedded systems. In Compiler Optimization meets Compiler Verification, pages 23--40, 2002.]]

[6]

G. Goos and W. Zimmermann. Verification of compilers. In B. Steffen and E. R. Olderog, editors, Correct System Design, volume 1710, pages 201--230. Springer, Nov 1999.]]

Digital Library

[7]

R. Huff. Lifetime-sensitive modulu scheduling. In Programming Language Design and Implementation. SIGPLAN, 1993.]]

Digital Library

[8]

C. Jaramillo, R. Gupta, and M. Soffa. Debugging and testing optimizers through comparision checking. In Compiler Optimization meets Compiler Verification, pages 87--103, 2002.]]

[9]

Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.]]

Digital Library

[10]

G. C. Necula. Translation validation for an optimizing compiler. In A. Press, editor, Proceedings of the ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI, pages 83--95, 2000.]]

Digital Library

[11]

B. Rau, M. Schlansker, and P. Tirumalai. Code generation schemas for modulo scheduling loops. In Proc. 25th annual international symposium on microarchitectur, pages 158--169, 1992.]]

Digital Library

[12]

A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, 2002.]]

Digital Library

[13]

W. Zimmermann and T. Gaul. On the Construction of Correct Compiler Back-Ends: An ASM Approach. Journal of Universal Computer Science, 3(5):504--567, May 1997.]]

[14]

L. Zuck, A. Pnueli, Y. Fang, and B. Goldberg. Voc: A translation validation for optimizing compilers. In Compiler Optimization meets Compiler Verification, pages 6--22, 2002.]]

[15]

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

Digital Library

Cited By

Dutta S(2023)Localizing faults using verification techniqueJournal of Systems and Software10.1016/j.jss.2023.111897(111897)Online publication date: Nov-2023
https://doi.org/10.1016/j.jss.2023.111897
Lopes NLee JHur CLiu ZRegehr JFreund SYahav E(2021)Alive2: bounded translation validation for LLVMProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454030(65-79)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454030
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
Show More Cited By

Index Terms

Validating software pipelining optimizations

Recommendations

Validating Software Pipelining Optimizations,
Validating More Loop Optimizations

Translation validation is a technique for ensuring that a translator, such as a compiler, produces correct results. Because complete verification of the translator itself is often infeasible, translation validation advocates coupling the verification ...
Will you still compile me tomorrow? static cross-version compiler validation
ESEC/FSE 2013: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering

This paper describes a cross-version compiler validator and measures its effectiveness on the CLR JIT compiler. The validator checks for semantically equivalent assembly language output from various versions of the compiler, including versions across a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CASES '02: Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems

October 2002

324 pages

ISBN:1581135750

DOI:10.1145/581630

General Chairs:
Shuvra S. Bhattacharyya
University of Maryland
,
Trevor Mudge
University of Michigan
,
Program Chairs:
Wayne Wolf
Princeton University
,
Ahmed Jerraya
TIMA, Grenoble, France

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

ACM: Association for Computing Machinery

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 October 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 52 of 230 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
400
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dutta S(2023)Localizing faults using verification techniqueJournal of Systems and Software10.1016/j.jss.2023.111897(111897)Online publication date: Nov-2023
https://doi.org/10.1016/j.jss.2023.111897
Lopes NLee JHur CLiu ZRegehr JFreund SYahav E(2021)Alive2: bounded translation validation for LLVMProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454030(65-79)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454030
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
Goldberg B(2010)Translation validation of loop optimizations and software pipelining in the TVOC frameworkProceedings of the 17th international conference on Static analysis10.5555/1882094.1882097(6-21)Online publication date: 14-Sep-2010
https://dl.acm.org/doi/10.5555/1882094.1882097
Tristan JLeroy X(2010)A simple, verified validator for software pipeliningACM SIGPLAN Notices10.1145/1707801.170631145:1(83-92)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1707801.1706311
Tristan JLeroy XHermenegildo MPalsberg J(2010)A simple, verified validator for software pipeliningProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1706299.1706311(83-92)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1706299.1706311
Goldberg B(2010)Translation Validation of Loop Optimizations and Software Pipelining in the TVOC FrameworkStatic Analysis10.1007/978-3-642-15769-1_3(6-21)Online publication date: 2010
https://doi.org/10.1007/978-3-642-15769-1_3
Tristan JLeroy X(2008)Formal verification of translation validatorsACM SIGPLAN Notices10.1145/1328897.132844443:1(17-27)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328897.1328444
Tristan JLeroy XNecula GWadler P(2008)Formal verification of translation validatorsProceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1328438.1328444(17-27)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328438.1328444
Gopalakrishnan GKirby R(2006)Toward reliable and efficient message passing software through formal analysisProceedings of the 20th international conference on Parallel and distributed processing10.5555/1898699.1898805(284-284)Online publication date: 25-Apr-2006
https://dl.acm.org/doi/10.5555/1898699.1898805
Show More Cited By

View Options

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