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.

Getting Rid of Store-Buffers in TSO Analysis

PARLATO G
2011-01-01

Abstract

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.
2011
978-3-642-22109-5
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11695/88382
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 49
  • ???jsp.display-item.citation.isi??? ND
social impact