Staged concurrent program analysis

9 years 5 months ago
Staged concurrent program analysis
Concurrent program verification is challenging because it involves exploring a large number of possible thread interleavings together with complex sequential reasoning. As a result, concurrent program verifiers resort to bi-modal reasoning, which alternates between reasoning over intra-thread (sequential) semantics and interthread (concurrent) semantics. Such reasoning often involves repeated intra-thread reasoning for exploring each interleaving (interthread reasoning) and leads to inefficiency. In this paper, we present a new two-stage analysis which completely separates intra- and inter-thread reasoning. The first stage uses sequential program semantics to obtain a precise summary of each thread in terms of the global accesses made by the thread. The second stage performs inter-thread reasoning by composing these thread-modular summaries using the notion of sequential consistency. Assertion violations and other concurrency errors are then checked in this composition with the help o...
Nishant Sinha, Chao Wang
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Authors Nishant Sinha, Chao Wang
Comments (0)