AbstractWe provide a uniform framework for the analysis of programs with procedures and explicit, unbounded, fork/join parallelism covering not only bitvector problems like reaching definitions or live variables but also non-bitvector problems like strong copy constant propagation. Due to their structural similarity to the sequential case, the resulting algorithms are as efficient as their widely accepted sequential counterparts, and they can easily be integrated in existing program analysis environments like e.g. MetaFrame or PAG. We are therefore convinced that our method will soon find its way into industrial-scale computer systems.
Categories and Subject Descriptors: F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; D.1.3 [Programming Techniques]: Concurrent Programming; D.2.5 [Software Engineering]: Testing and Debugging; F.1.1 [Computation by Abstract Devices]: Models of Computation
Additional Key Words and Phrases: inter-procedural program analysis, explicit parallelism, bitvector problems, strong copy constant propagation, coincidence theorems
Selected references
- Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238-252, Los Angeles, California, January 1977.