Algorithm visualization using concrete and abstract shape graphs

ABSTRACT

Traditional algorithm animation attempts to provide visualizations of the execution of a program on concrete data. In recent years a different approach has been proposed which attempts to visualize an "abstract execution" on "abstract data." This is based on Cousots' notion of abstract interpretations, in particular in the case of programs manipulating pointer structures this is based on so-called shape analysis. Shape analysis maps all possible heap configurations that can arise during a program's executions (a potentially unbounded set) to a finite number of "shape graphs" and it maps steps of the program to transitions between shape graphs. Every concrete execution of the program then corresponds to a sequence of transitions among shape graphs, the "abstract execution." Visualizing such an abstract execution is desirable since sets of shape graphs in a very strong sense encode invariants of the program and understanding the effect of a program usually benefits more from grasping what stays invariant than from seeing what changes.

In this paper we combine the two approaches and argue for simultaneously visualizing a concrete and the corresponding abstract execution of a program. We have built a Visualizer for programs manipulating pointer structures that realizes this combined abstract/concrete visualization. It uses TVLA to automatically perform the shape analysis of a program. It allows to present abstract and concrete views in an extremely customizable way. This paper however does not present our Visualizer, but focuses on the technique to combine concrete and abstract visualizations.

REFERENCES

• 1: Bieber, R. 2001. Alexsa - Algorithm Explanation by Shape Analysis. Extensions to the TVLA System. Master's thesis, Saarland University.
• 2: F. Corbera , R. Asenjo , E. L. Zapata, New shape analysis techniques for automatic parallelization of C codes, Proceedings of the 13th international conference on Supercomputing, p.220-227, June 20-25, 1999, Rhodes, Greece [doi>10.1145/305138.305196]
• 3: Camil Demetrescu , Irene Finocchi , Giuseppe F. Italiano , Stefan Näher, Visualization in algorithm engineering: tools and techniques, Experimental algorithmics: from algorithm design to robust and efficient software, Springer-Verlag New York, Inc., New York, NY, 2002
• 4: Dierk Johannes , Raimund Seidel , Reinhard Wilhelm, Algorithm animation using shape analysis: visualising abstract executions, Proceedings of the 2005 ACM symposium on Software visualization, May 14-15, 2005, St. Louis, Missouri [doi>10.1145/1056018.1056021]
• 5: Klavins, G. 2003. Algorithm Visualisation Using Shape Analysis. Master's thesis, Saarland University.
• 6: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 7: Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.26-38, August 21-24, 2000, Portland, Oregon, United States
• 8: Lev-Ami, T. 2000. TVLA:A framework for Kleene based static analysis. PhD thesis, Tel-Aviv University.
• 9: Manevich, R., and Sagiv, M. 2004. TVLA: User's Manual. Tel-Aviv University.
• 10: John L. Ross , Shmuel Sagiv, Building a Bridge between Pointer Aliases and Program Dependences, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.221-235, March 28-April 04, 1998
• 11: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.16-31, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237725]
• 12: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 13: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 14: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 15: Reinhard Wilhelm , Shmuel Sagiv , Thomas W. Reps, Shape Analysis, Proceedings of the 9th International Conference on Compiler Construction, p.1-17, March 25-April 02, 2000
• 16: Reinhard Wilhelm , Tomasz Müldner , Raimund Seidel, Algorithm Explanation: Visualizing Abstract States and Invariants, Revised Lectures on Software Visualization, International Seminar, p.381-394, May 20-25, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.6 Programming Environments
          Subjects: Graphical environments

Additional Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Graph algorithms

  H. Information Systems
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.2 User Interfaces (D.2.2, H.1.2, I.3.6)

General Terms:
Algorithms

Keywords:
algorithm animation, algorithm visualisation, invariants, shape analysis, shape graphs