2011 | OriginalPaper | Chapter
Getting Rid of Store-Buffers in TSO Analysis
Authors : Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We propose an approach for reducing the TSO reachability analysis of concurrent programs to their SC reachability analysis, under some conditions on the explored behaviors. First, we propose a
linear
code-to-code translation that takes as input a concurrent program
P
and produces a concurrent program
P
′ such that, running
P
′ under SC yields the same set of reachable (shared) states as running
P
under TSO with at most
k
context-switches for each thread, for a fixed
k
. Basically, we show that it is possible to use only
O
(
k
) additional copies of the shared variables of
P
as local variables to simulate the store buffers, even if they are unbounded. Furthermore, we show that our translation can be extended so that an
unbounded
number of context-switches is possible, under the condition that each write operation sent to the store buffer stays there for at most
k
context-switches of the thread. Experimental results show that bugs due to TSO can be detected with small bounds, using off-the-shelf SC analysis tools.