Validating software pipelining optimizations

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: Vicki H. Allan , Reese B. Jones , Randall M. Lee , Stephen J. Allan, Software pipelining, ACM Computing Surveys (CSUR), v.27 n.3, p.367-432, Sept. 1995 [doi>10.1145/212094.212131]
• 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.
• 3: W. DeRoever , Kai Engelhardt, Data Refinement: Model-Oriented Proof Methods and Their Comparison, Cambridge University Press, New York, NY, 1999
• 4: Jean-Christophe Filliâtre , Sam Owre , Harald Rueß , Natarajan Shankar, ICS: Integrated Canonizer and Solver, Proceedings of the 13th International Conference on Computer Aided Verification, p.246-249, July 18-22, 2001
• 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: Gerhard Goos , Wolf Zimmermann, Verification of Compilers, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.201-230, January 1999
• 7: Richard A. Huff, Lifetime-sensitive modulo scheduling, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.258-267, June 21-25, 1993, Albuquerque, New Mexico, United States
• 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: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 10: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: B. Ramakrishna Rau , Michael S. Schlansker , P. P. Tirumalai, Code generation schema for modulo scheduled loops, Proceedings of the 25th annual international symposium on Microarchitecture, p.158-169, December 01-04, 1992, Portland, Oregon, United States
• 12: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 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 , R. Leviathan, Validation of Optimizing Compilers,, Weizmann Science Press of Israel, Jerusalem, Israel, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
      C.1.3 Other Architecture Styles
          Subjects: Pipeline processors

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Validation
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

General Terms:
Verification

Keywords:
compilers, optimization, pipeline processors, translation validation, verification