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...

• Type: Journal
• Year: 2010
• Where: SIGSOFT
• Authors: Nishant Sinha, Chao Wang
• Keywords: Bi-modal Reasoning, Inter-thread Reasoning, Reasoning, SIGSOFT 2010, Software Engineering