Summarizing procedures in concurrent programs

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 ...

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof
• Keywords: Multithreaded Programs, POPL 2004, Procedure Summarization, Procedures, Programming Languages