Staged Concurrent Program Analysis

April 21, 2011
Nishant Sinha | NEC Labs

Concurrent program verification is challenging because it involves exploring a large number of possible thread interleavings together with complex sequential reasoning. Consequently, most concurrent program verifiers resort to some form of bi-modal reasoning, which alternates between reasoning over intra-thread (sequential) semantics and inter-thread (concurrent) semantics. Such reasoning often involves repeated sequential reasoning for exploring each interleaving and leads to inefficiency. Moreover, most methods employ a control-centric mechanism, e.g., a scheduler, for composing threads which obstructs direct reasoning about inter-thread data flow.

In this talk, I will present a new staged analysis technique which both (a) decouples intra- and inter-thread reasoning and (b) enables data-centric reasoning. The first stage uses sequential program semantics to obtain a precise summary of each thread in terms of its global memory accesses only. The second stage performs inter-thread reasoning by employing the data-centric notion of sequential consistency to compose these thread-modular summaries. Concurrency errors are then checked using an off-the-shelf SMT solver. An implementation of our approach in the FUSION framework developed at NEC for checking concurrent C programs shows that staged reasoning improves the scalability of the analysis significantly.

Speaker Details

Nishant Sinha is a Research Staff Member in the System Analysis and Verification group at the NEC Labs, Princeton, USA. He obtained his M.S. and Ph.D. in Computer Engineering from Carnegie Mellon University, USA and B. Tech. (Hons.) in Computer Science and Engineering from Indian Institute of Technology, Kharagpur. His interests lie in analysis algorithms for sequential and concurrent programs, automated compositional analysis, automata theory, rewriting and automated decision procedures.