Getting Rid of Store Buffers in PSO Analysis

We propose an approach for reducing the PSO 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 under SC yieldsthe same set of reachable (shared) states as running P under PSO 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 common store buffer and all the buffers per variable, 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 PSO can be detected with small bounds, using off-the-shelf SC analysis tools