Getting Rid of Store-Buffers in the Analysis of Weak Memory Models

Experimental results:

We have considered 4 mutual exclusion protocols: Dekker’s, Lamport’s, Peterson’s, and Szymanski’s. All these protocols become unsound under TSO, i.e., they do not ensure exclusive access to the critical section. We consider for each protocol two versions, one without fences (the original version of the protocol) that is buggy, and one with fences (neutralizing TSO) that is correct. 

We have encoded each of these examples as C programs and manually translated each of them by using the K-store-age translation with K=2. Then, we have used two tools to analyze the translated programs: POIROT (by MSR) and ESBMC (by the university of Southampton). Both of these tools were able to answer correctly, i.e., by finding the bugs for the buggy versions. (Except that ESBMC has not terminated the analysis in one case.) 

POIROT combines bounded model checking by bounding the number of loop unrolling and bounded delay analysis. In our experiments, we consider a bound L = 2 on the number of loop unrolling, and a bound D = 1 or D = 2 (= to the number of delays + 1). 

ESBMC combines bounded model checking by bounding the number of loop unrolling and bounded context-switch analysis. In our experiments, we consider a bound L = 2 or L = 3 on the number of loop unrolling, and a bound C = 3 or C = 4 on the number of context-switches. 

We give hereafter tables reporting the execution times for our experiments for each of the two tools in the different cases mentioned above. For each case, we provide the source code of the programs. Notice that the symbol (-) stands for the fact that the tool runs out of resources.

POIROT (with L=2)
Version with no fences
(Buggy for TSO)
Version with fences
(Correct for TSO)
Running time
(with D=1)
Source code of the
 translated program
Running time
(with D=1)
Running time
(with D=2)
Source code of the
 translated program
Dekker  7 sec  Dekker  6 sec 72 sec Dekker
Lamport 26 sec Lamport 110 sec 1608 sec Lamport
Peterson 5 sec Peterson 6 sec 47 sec Peterson
Szymanski 8 sec Szymanski
6 sec 978 sec Szymanski
                                                                               



 ESBMC 
Version with no fences
(Buggy for TSO)
Version with fences
(Correct for TSO)
Running time
(with L=2, C=3)
Source code of the
 translated program
Running time
(with L=3, C=4)
Source code of the
 translated program
Dekker  -  Dekker  - Dekker
Lamport 1 sec Lamport 7 sec Lamport
Peterson 1 sec Peterson 1 sec Peterson
Szymanski 1 sec Szymanski
6 sec Szymanski