Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences

  • Sven Verdoolaege
  • Gerda Janssens
  • Maurice Bruynooghe
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


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.


Induction Hypothesis Equivalence Tree Dependence Graph Output Computation Transitive Closure 
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.


  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Barthou, D., Collard, J.-F., Feautrier, P.: Fuzzy array dataflow analysis. J. Parallel Distrib. Comput. 40(2), 210–226 (1997)CrossRefzbMATHGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Feautrier, P.: Array expansion. In: ICS 1988: Proceedings of the 2nd international conference on Supercomputing, pp. 429–441. ACM Press, New York (1988)Google Scholar
  10. 10.
    Feautrier, P.: Dataflow analysis of array and scalar references. International Journal of Parallel Programming 20(1), 23–53 (1991)CrossRefzbMATHGoogle Scholar
  11. 11.
    Feautrier, P., Collard, J., Bastoul, C.: Solving systems of affine (in)equalities. Technical report, PRiSM, Versailles University (2002)Google Scholar
  12. 12.
    Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)Google Scholar
  13. 13.
    Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega library. Technical report, University of Maryland (November 1996)Google Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Not. 35(5), 83–94 (2000)CrossRefGoogle Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Sven Verdoolaege
    • 1
  • Gerda Janssens
    • 1
  • Maurice Bruynooghe
    • 1
  1. 1.Department of Computer ScienceKatholieke Universiteit LeuvenLeuvenBelgium

Personalised recommendations