Summarizing procedures in concurrent programs

The ability to summarize procedures is fundamental to building scalable interprocedural analyses. For sequential programs, proce-dure summarization is well-understood and used routinely in a va-riety of compiler optimizations and software defect-detection tools. However, the benefit of summarization is not available to multi-threaded 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 proce-dure 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 mul-tithreaded programs. Our method for procedure summarization is based on the insight that in well-synchronized programs, any com-putation 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 pro-gram, 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 analy-sis for multithreaded programs with recursive procedures is unde-cidable [18]), there is a large class of programs for which our al-gorithm does terminate. We give a formal characterization of this class, which includes programs that use shared variables, synchro-nization, and recursion