Staged Concurrent Program Analysis

Опубликовано 17 августа 2016, 1:45

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.