Summarizing procedures in concurrent programs

ABSTRACT

The ability to summarize procedures is fundamental to building scalable interprocedural analyses. For sequential programs, procedure summarization is well-understood and used routinely in a variety of compiler optimizations and software defect-detection tools. However, the benefit of summarization is not available to multithreaded programs, for which a clear notion of summaries has so far remained unarticulated in the research literature.In this paper, we present an intuitive and novel notion of procedure summaries for multithreaded programs. We also present a model checking algorithm for these programs that uses procedure summarization as an essential component. Our algorithm can also be viewed as a precise interprocedural dataflow analysis for multithreaded programs. Our method for procedure summarization is based on the insight that in well-synchronized programs, any computation of a thread can be viewed as a sequence of transactions, each of which appears to execute atomically to other threads. We summarize within each transaction; the summary of a procedure comprises the summaries of all transactions within the procedure. We leverage the theory of reduction [17] to infer boundaries of these transactions.The procedure summaries computed by our algorithm allow reuse of analysis results across different call sites in a multithreaded program, a benefit that has hitherto been available only to sequential programs. Although our algorithm is not guaranteed to terminate on multithreaded programs that use recursion (reachability analysis for multithreaded programs with recursive procedures is undecidable [18]), there is a large class of programs for which our algorithm does terminate. We give a formal characterization of this class, which includes programs that use shared variables, synchronization, and recursion.

REFERENCES

• 1: Rajeev Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.390-402, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325746]
• 2: Thomas Ball , Sagar Chaki , Sriram K. Rajamani, Parameterized Verification of Multithreaded Software Libraries, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.158-173, April 02-06, 2001
• 3: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 4: Ahmed Bouajjani , Javier Esparza , Tayssir Touili, A generic approach to the static analysis of concurrent programs with procedures, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.62-73, January 15-17, 2003, New Orleans, Louisiana, USA
• 5: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 6: Giorgio Delzanno , Jean-François Raskin , Laurent Van Begin, Towards the Automated Verification of Multithreaded Java Programs, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.173-187, April 08-12, 2002
• 7: Evelyn Duesterwald , Mary Lou Soffa, Concurrency analysis in the presence of procedures using a data-flow framework, Proceedings of the symposium on Testing, analysis, and verification, p.36-48, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120811]
• 8: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 9: Javier Esparza , Andreas Podelski, Efficient algorithms for pre* and post* on interprocedural parallel flow graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325697]
• 10: Javier Esparza , Stefan Schwoon, A BDD-Based Model Checker for Recursive Programs, Proceedings of the 13th International Conference on Computer Aided Verification, p.324-336, July 18-22, 2001
• 11: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 12: C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN 03: SPIN Workshop, LNCS 2648, pages 213--225. Springer-Verlag, 2003.
• 13: C. Flanagan and S. Qadeer. Transactions for software model checking. In SoftMC 03: Software Model Checking Workshop, 2003.
• 14: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 15: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 16: S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. In FTfJP 03: Formal Techniques for Java-like Programs, 2003.
• 17: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 18: G. Ramalingam, Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.416-430, March 2000 [doi>10.1145/349214.349241]
• 19: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 20: Martin C. Rinard, Analysis of Multithreaded Programs, Proceedings of the 8th International Symposium on Static Analysis, p.1-19, July 16-18, 2001
• 21: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, pages 189--233. Prentice-Hall, 1981.
• 22: Olaf Burkart , Bernhard Steffen, Composition, decomposition and model checking of pushdown processes, Nordic Journal of Computing, v.2 n.2, p.89-125, Summer 1995

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Reliability, Security, Verification

Keywords:
concurrent programs, interprocedural dataflow analysis, model checking, procedure summaries, pushdown systems, reduction, transactions