Multi-stage On-Demand Program Slicing for Modular Analysis of Multi-threaded Programs

Precise analysis of multi-threaded programs requires combining flow-sensitive pointer analysis (FSPTA) with interleaving and lock analysis (ILA) to reason about cross-thread value flows under feasible concurrent executions. ILA computes may-happen-in-parallel (MHP) relations and lock-release spans to determine when shared accesses can occur concurrently. Unfortunately, these analyses are both expensive and tightly coupled: FSPTA needs ILA to rule out infeasible inter-thread def-use relations, while ILA needs alias information to identify interference-relevant interactions. As a result, whole-program analyses often spend most of their time on code that is irrelevant to the client query. We present MSli, an on-demand slicing framework for modular analysis of multi-threaded programs. It extracts compact, query-relevant program slices while preserving the answers of downstream analyses. Unlike single-pass slicing over a unified dependence graph, MSli performs multi-stage slicing with analysis-specific criteria. Concretely, a lightweight pre-analysis establishes an overapproximation of inter-thread value flows and performs ILA slicing source extraction to identify the MHP and lock-span queries required later for ILA slicing. The refined main-phase ILA results then enable reconstruction of a thread-aware value-flow graph to guide FSPTA slicing, supporting modular analysis and downstream clients. We implement MSli in SVF and evaluate it on ten large real-world projects with data race detection as a representative client. Compared with the unsliced baseline (FSAM), MSli reduces the analyzed ICFG to 5.4% (ILA) and 25.7% (FSPTA), reduces ILA/FSPTA runtimes to 4.7%/18.3%, and cuts total analysis time to 20.8% on average, while producing identical query outcomes and race alarms.

CCS Concepts: • Software and its engineering → Automated static analysis; Multithreading; • Theory of computation → Program analysis.