A simple, verified validator for software pipelining. (English) Zbl 1312.68069
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 83-92 (2010).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N20 | Theory of compilers and interpreters |
References:
| [1] | A. V. Aho, M. Lam, R. Sethi, and J. D. Ullman. Compilers: principles, techniques, and tools. Addison-Wesley, second edition, 2006. |
| [2] | A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998. |
| [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. 10.1007/11513988_29 · Zbl 1081.68606 |
| [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. 10.1145/514191.514208 |
| [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. |
| [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. 10.1007/11823230_19 |
| [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. 10.1145/155090.155115 |
| [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. 10.1109/SEFM.2006.4 |
| [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. 10.1145/1542476.1542513 |
| [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. 10.1145/53990.54022 |
| [11] | X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. 10.1145/1538788.1538814 |
| [12] | X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 2009. To appear. 10.1007/s10817-009-9155-4 · Zbl 1185.68215 |
| [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. 10.1007/s10817-008-9099-0 · Zbl 1154.68039 |
| [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. 10.1145/581630.581676 |
| [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. |
| [16] | S. S. Muchnick. Advanced compiler design and implementation. Morgan Kaufmann, 1997. |
| [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. 10.1016/j.entcs.2009.05.052 · Zbl 1347.68304 |
| [18] | G. C. Necula. Translation validation for an optimizing compiler. In Programming Language Design and Implementation 2000, pages 83-95. ACM Press, 2000. 10.1145/349299.349314 |
| [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. · Zbl 1022.68733 |
| [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. |
| [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. 10.1145/125826.125848 |
| [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. 10.1145/964001.964002 · Zbl 1325.68070 |
| [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. 10.1145/1480881.1480915 · Zbl 1315.68078 |
| [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. 10.1145/1328438.1328444 · Zbl 1295.68074 |
| [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. 10.1145/1542476.1542512 |
| [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. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
