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 Kstoreage 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 contextswitch 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 contextswitches.
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 