Sciweavers

POPL
2004
ACM

Summarizing procedures in concurrent programs

13 years 9 months ago
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 ...
Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where POPL
Authors Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof
Comments (0)