Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Getting Rid of Store-Buffers in TSO Analysis
verfasst von : Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.