Abstract
Designers often apply manual or semi-automatic loop and data transformations on array and loop intensive programs to improve performance. The transformations should preserve the functionality, however, and this paper presents an automatic method for constructing equivalence proofs for the class of static affine programs. The equivalence checking is performed on a dependence graph abstraction and uses a new approach based on widening to handle recurrences. Unlike transitive closure based approaches, this widening approach can also handle non-uniform recurrences. The implementation is publicly available and is the first of its kind to fully support commutative operations.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alias, C., Barthou, D.: On the recognition of algorithm templates. In: Int. Workshop on Compilers Optimization Meets Compiler Verification, Warsaw, April 2003. ENTCS, vol. 82, pp. 395–409. Elsevier Science, Amsterdam (2003)
Allen, J.R., Kennedy, K., Porterfield, C., Warren, J.D.: Conversion of control dependence to data dependence. In: POPL 1983, pp. 177–189. ACM, New York (1983)
Amarasinghe, S., Anderson, J., Lam, M.S., Tseng, C.-W.: An overview of the SUIF compiler for scalable parallel machines. In: Proceedings of the Seventh SIAM Conference on Parallel Processing for Scientific Computing (1995)
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Barthou, D., Collard, J.-F., Feautrier, P.: Fuzzy array dataflow analysis. J. Parallel Distrib. Comput. 40(2), 210–226 (1997)
Barthou, D., Feautrier, P., Redon, X.: On the equivalence of two systems of affine recurrence equations. In: Monien, B., Feldmann, R.L. (eds.) Euro-Par 2002. LNCS, vol. 2400, pp. 309–313. Springer, Heidelberg (2002)
Bastoul, C.: Code generation in the polyhedral model is easier than you think. In: PACT 2004: Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques, Washington, DC, USA, 2004, pp. 7–16. IEEE Computer Society, Los Alamitos (2004)
Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Feautrier, P.: Array expansion. In: ICS 1988: Proceedings of the 2nd international conference on Supercomputing, pp. 429–441. ACM Press, New York (1988)
Feautrier, P.: Dataflow analysis of array and scalar references. International Journal of Parallel Programming 20(1), 23–53 (1991)
Feautrier, P., Collard, J., Bastoul, C.: Solving systems of affine (in)equalities. Technical report, PRiSM, Versailles University (2002)
Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)
Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega library. Technical report, University of Maryland (November 1996)
Kelly, W., Pugh, W., Rosser, E., Shpeisman, T.: Transitive closure of infinite graphs and its applications. Int. J. Parallel Program. 24(6), 579–598 (1996)
Manjunathaiah, M., Megson, G.M., Rajopadhye, S.V., Risset, T.: Uniformization of affine dependance programs for parallel embedded system design. In: Ni, L.M., Valero, M. (eds.) ICPP 2002, Proceedings, pp. 205–213. IEEE Computer Society, Los Alamitos (2001)
Mateev, N., Menon, V., Pingali, K.: Fractal symbolic analysis. In: ICS 2001: Proceedings of the 15th international conference on Supercomputing, pp. 38–49. ACM, New York (2001)
Matsumoto, T., Seto, K., Fujita, M.: Formal equivalence checking for loop optimization in C programs without unrolling. In: IASTED Proc. ACST 2007: Advances in Computer Science and Technology, Anaheim, CA, USA, pp. 43–48. ACTA Press (2007)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 330–341 (2004)
Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Not. 35(5), 83–94 (2000)
Shashidhar, K.C.: Efficient automatic verification of loop and data-flow transformations by functional equivalence checking. Ph.D thesis, Katholieke Universiteit Leuven, Belgium (May 2008)
Shashidhar, K.C., Bruynooghe, M., Catthoor, F., Janssens, G.: Verification of source code transformations by program equivalence checking. In: Bodik, R. (ed.) CC 2005. LNCS (LNAI), vol. 3443, pp. 221–236. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Verdoolaege, S., Janssens, G., Bruynooghe, M. (2009). Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_44
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)