Advertisement

Parallelism for free: Bitvector analyses ⇒ no state explosion!

  • Jens Knoop
  • Bernhard Steffen
  • Jürgen Vollmer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)

Abstract

One of the central problems in the automatic analysis of distributed or parallel systems is the combinatorial state explosion leading to models, which are exponential in the number of their parallel components. The only known cure for this problem are application specific techniques, which avoid the state explosion problem under special frame conditions. In this paper we present a new such technique, which is tailored to bitvector analyses, which are very common in data flow analysis. In fact, our method allows to adapt most of the practically relevant optimizations for sequential programs, for a parallel setting with shared variables and arbitrary interference between parallel components.

Keywords

Program Model Parallel Program Flow Graph Parallel Component Program Point 
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.

References

  1. [CC1]
    Cousot, P., and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4 th International Symposium on Principles of Programming Languages (POPL'77), Los Angeles, California, 1977, 238–252.Google Scholar
  2. [CC2]
    Cousot, P., and Cousot, R. Invariance proof methods and analysis techniques for parallel programs. In Biermann, A. W., Guiho, G., and Kodratoff, Y. (eds.) Automatic Program Construction Techniques, chapter 12, 243–271, Macmillan Publishing Company, 1984.Google Scholar
  3. [CHI]
    Chow, J.-H., and Harrison, W. L. Compile time analysis of parallel programs that share memory. In Conference Record of the 19 th International Symposium on Principles of Programming Languages (POPL'92), Albuquerque, New Mexico, 1992, 130–141.Google Scholar
  4. [CH2]
    Chow, J.-H., and Harrison, W. L. State Space Reduction in Abstract Interpretation of Parallel Programs. In Proceedings of the International Conference on Computer Languages, (ICCL'94), Toulouse, France, May 16–19, 1994, 277–288.Google Scholar
  5. [DBDS]
    Duri, S., Buy, U., Devarapalli, R., and Shatz, S. M. Using state space methods for deadlock analysis in Acta tasking. In Proceedings of the ACM SIGSOFT'93 International Symposium on Software Testing and Analysis, Software Engineering Notes 18, 3 (1993), 51–60.Google Scholar
  6. [DC]
    Dwyer, M. B., and Clarke, L. A. Data flow analysis for verifying properties of concurrent programs. In Proceedings of the 2 nd ACM SIG-SOFT'94 Symposium on Foundations of Software Engineering (SIG-SOFT'94), New Orleans, Lousiana, Software Engineering Notes 19, 5 (1994), 62–75.Google Scholar
  7. [DRZ]
    Dhamdhere, D. M., Rosen, B. K., and Zadeck, F. K. How to analyze large programs efficiently and informatively. In Proceedings of the ACM SIGPLAN'92 Conference on Programming Language Design and Implementation (PLDI'92), San Francisco, California, SIGPLAN Notices 27, 7 (1992), 212–223.Google Scholar
  8. [DS]
    Drechsler, K.-H., and Stadel, M. P. A variation of Knoop, Rüthing and Steffen's LAZY CODE MOTION. SIGPLAN Notices 28, 5 (1993), 29–38.Google Scholar
  9. [GS]
    Grunwald, D., and Srinivasan, H. Data flow equations for explicitely parallel programs. In Proceedings of the ACM SIGPLAN Symposium on Principles of Parallel Programming (PPOPP'93), SIGPLAN Notices 28, 7 (1993).Google Scholar
  10. [GW]
    Godefroid, P., and Wolper, P. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of the 3 rd International Workshop on Computer Aided Verification (CAV'91), Aalborg, Denmark, Springer-Verlag, LNCS 575 (1991), 332–342.Google Scholar
  11. [He]
    Hecht, M. S. Flow analysis of computer programs. Elsevier, North-Holland, 1977.Google Scholar
  12. [HU]
    Hopcroft, J. E., and Ullman, J. E. Introduction to automata theory, languages, and computation. Addison-Wesley, Reading, Massach., 1979.Google Scholar
  13. [Kil]
    Kildall, G. A. Global expression optimization during compilation. Ph.D. dissertation, Technical Report No. 72-06-02, University of Washington, Computer Science Group, Seattle, Washington, 1972.Google Scholar
  14. [Ki2]
    Kildall, G. A. A unified approach to global program optimization. In Conference Record of the 1 st ACM Symposium on Principles of Programming Languages (POPL'73), Boston, Massachusetts, 1973, 194–206.Google Scholar
  15. [KRS1]
    Knoop, J., Rüthing, O., and Steffen, B. Lazy code motion. In Proceedings of the ACM SIGPLAN'92 Conference on Programming Language Design and Implementation (PLDI'92), San Francisco, California, SIGPLAN Notices 27, 7 (1992), 224–234.Google Scholar
  16. [KRS2]
    Knoop, J., Rüthing, O., and Steffen, B. Optimal code motion: Theory and practice. Transactions on Programming Languages and Systems 16, 4 (1994), 1117–1155.Google Scholar
  17. [KRS3]
    Knoop, J., Rüthing, O., and Steffen, B. Partial dead code elimination. In Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI'94), Orlando, Florida, SIGPLAN Notices 29, 6 (1994), 147–158.Google Scholar
  18. [KRS4]
    Knoop, J., Rüthing, O., and Steffen, B. The power of assignment motion. In Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation (PLDI'95), La Jolla, California, SIGPLAN Notices 30, 6 (1995), 233–245.Google Scholar
  19. [KRS5]
    Knoop, J., Rüthing, O., and Steffen, B. Lazy strength reduction. Journal of Programming Languages 1, 1 (1993), 71–91.Google Scholar
  20. [KS]
    Knoop, J., and Steifen, B. The interprocedural coincidence theorem. In Proceedings of the 4 th International Conference on Compiler Construction (CC'92), Paderborn, Germany, Springer-Verlag, LNCS 641 (1992), 125–140.Google Scholar
  21. [KSV1]
    Knoop, J., Steffen, B., and Vollmer, J. Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. In Preliminary Proceedings of the 1 st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95), Aarhus, Denmark, BRICS Notes Series NS-95-2 (1995), 319–333.Google Scholar
  22. [KSV2]
    Knoop, J., Steffen, B., and Vollmer, J. Optimal code motion for parallel programs. Fakultät für Mathematik und Informatik, Universität Passau, Germany, MIP-Bericht 9511 (1995), 30 pages.Google Scholar
  23. [KU]
    Kam, J. B., and Ullman, J. D. Monotone data flow analysis frameworks. Acta Informatica 7, (1977), 309–317.Google Scholar
  24. [LC]
    Long, D., and Clarke, L. A. Data flow analysis of concurrent systems that use the rendezvous model of synchronization. In Proceedings of the ACM SIGSOFT'91 Symposium on Testing, Analysis, and Verification (TAV4), Victoria, British Columbia, Software Engineering Notes 16, (1991), 21–35.Google Scholar
  25. [Ma]
    Marriot, K. Frameworks for abstract interpretation. Acta Informatica 30, (1993), 103–129.Google Scholar
  26. [McD]
    McDowell, C. E. A practical algorithm for static analysis of parallel programs. Journal of Parallel and Distributed Computing 6, 3 (1989), 513–536.Google Scholar
  27. [MJ]
    Muchnick, S. S., and Jones, N. D. (Eds.). Program flow analysis: Theory and applications. Prentice Hall, Englewood Cliffs, New Jersey, 1981.Google Scholar
  28. [MP]
    Midkiff, S. P., and Padua, D. A. Issues in the optimization of parallel programs. In Proceedings of the International Conference on Parallel Processing, Volume II, St. Charles, Illinois, (1990), 105–113.Google Scholar
  29. [St]
    Steffen, B. Generating data flow analysis algorithms from modal specifications. Science of Computer Programming 21, (1993), 115–139.Google Scholar
  30. [SCKKM]
    Steffen, B., Claßen, A., Klein, M., Knoop, J., and Margaria, T. The fixpoint-analysis machine. In Proceedings of the 6 th International Conference on Concurrency Theory (CONCUR'95), Philadelphia, Pennsylvania, Springer-Verlag, LNCS 962 (1995), 72–87.Google Scholar
  31. [SHW]
    Srinivasan, H., Hook, J., and Wolfe, M. Static single assignment form for explicitly parallel programs. In Conference Record of the 20 th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'93), Charleston, South Carolina, 1993, 260–272.Google Scholar
  32. [SP]
    Sharir, M., and Pnueli, A. Two approaches to interprocedural data flow analysis. In [MJ], 1981, 189–233.Google Scholar
  33. [SW]
    Srinivasan, H., and Wolfe, M. Analyzing programs with explicit parallelism. In Proceedings of the 4 th International Conference on Languages and Compilers for Parallel Computing, Santa Clara, California, Springer-Verlag, LNCS 589 (1991), 405–419.Google Scholar
  34. [Va]
    Valmari, A. A stubborn attack on state explosion. In Proceedings of the 2 nd International Conference on Computer Aided Verification, New-Brunswick, New Jersey, Springer-Verlag, LNCS 531 (1990), 156–165.Google Scholar
  35. [Vol]
    Vollmer, J. Data flow equations for parallel programs that share memory. Tech. Rep. 2.11.1 of the ESPRIT Project COMPARE #5933, Fakultät für Informatik, Universität Karlsruhe, Germany, (1994).Google Scholar
  36. [Vo2]
    Vollmer, J. Data flow analysis of parallel programs. In Proceedings of the IFIP WG 10.3 Working Conference on Parallel Architectures and Compilation Techniques (PACT'95), Limassol, Cyprus, 1995, 168–177.Google Scholar
  37. [WS]
    Wolfe, M., and Srinivasan, H. Data structures for optimizing programs with explicit parallelism. In Proceedings of the 1 st International Conference of the Austrian Center for Parallel Computation, Salzburg, Austria, Springer-Verlag, LNCS 591 (1991), 139–156.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Jens Knoop
    • 1
  • Bernhard Steffen
    • 1
  • Jürgen Vollmer
    • 2
  1. 1.Fakultät für Mathematik und InformatikUniversität PassauPassauGermany
  2. 2.Fakultät für Informatik, Institut für Programmstrukturen und Datenorganisation (IPD)Universität KarlsruheKarlsruheGermany

Personalised recommendations