Parallelizing Top-Down Interprocedural Analyses

Modularity is a central theme in any scalable program analysis. The core idea in a modular analysis is to build summaries at procedure boundaries, and use the summary of a procedure to analyze the effect of calling it at its calling context. There are two ways to perform a modular program analysis: (1) top-down and (2) bottomup. A bottom-up analysis proceeds upwards from the leaves of the call graph, and analyzes each procedure in the most general calling context and builds its summary. In contrast, a top-down analysis starts from the root of the call graph, and proceeds downward, analyzing each procedure in its calling context. Top-down analyses have several applications in verification and software model checking. However, traditionally, bottom-up analyses have been easier to scale and parallelize than top-down analyses.

In this paper, we propose a generic framework, Bolt, which uses MapReduce style parallelism to scale top-down analyses. In particular, we consider top-down analyses that are demand driven, such as the ones used for software model checking. In such analyses, each intraprocedural analysis happens in the context of a reachability query. A query Q over a procedure P results in sub-queries over the procedures called by P. The key insight in Bolt is that the query tree can be explored in parallel using MapReduce style parallelism – the map stage can be used to run a set of enabled queries in parallel, and the reduce stage can be used to manage inter-dependencies between queries. Iterating the map and reduce stages alternately, we can exploit the parallelism inherent in topdown analyses. Another unique feature of Bolt is that it is parameterized by the algorithm used for intraprocedural analysis. Several kinds of analyses, including may-analyses, must-analyses, and may-must-analyses can be parallelized using Bolt.

We have implemented the Bolt framework and instantiated the intraprocedural parameter with a may-must-analysis. We have run Bolt on a test suite consisting of 45 device drivers and 150 safety properties. Our results demonstrate an average speedup of 3.71x and a maximum speedup of 7.4x with 8 cores. Moreover, in several checks where a sequential analysis fails, Bolt is able to successfully complete its analysis.