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 [Lipton75] 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 [Ramalingam00]),
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.
