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.