CAV'19 Project Page

Aalto University Fortiss TU Braunschweig University of Helsinki

BMC for Weak Memory Models

Relation Analysis for Compact SMT Encodings

Natalia Gavrilenko, Hernan Ponce de Leon, Florian Furbach, Keijo Heljanko and Roland Meyer

Abstract. We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT- compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.


Keywords: WeakMemoryModel · CAT · ConcurrentPrograms ·Bounded Model Checking · SMT.


Reproducing results


Download the Virtual Machine Snapshot created with Virtual Box and login using the following creadentials username: mbse, password: mbse. The artifact is located under ~/Desktop/Dat3M.

The rest of this page describes how to reproduce the results shown in the paper. If you encounter an error when running the scripts, execute

			
	export LD_LIBRARY_PATH=~/Desktop/Dat3M/lib:~/Desktop/Dat3M-FMCAD/import
			
		

Alias analysis


Replicate data for alias benchmark plot (Figure 1 left) with the whole data set used in the paper. The script will generate a file ~/Desktop/Dat3M/alias.csv. Expected running time: ~2-3 days.

			
	cd ~/Desktop/Dat3M
	python3 python/alias.py -p litmus/C -c cat/linux-kernel.cat -s 1800 -v -d alias.csv
			
		

Replicate the alias benchmark plot (Figure 1 left) with a subset of tests. The script will generate a file ~/Desktop/Dat3M/alias.csv. Expected running time: ~3 hours.

			
	cd ~/Desktop/Dat3M
	python3 python/alias.py -p cav/alias -c cat/linux-kernel.cat -s 1800 -v -d alias.csv
			
		

Obtain running time of individual tests (with alias analysis).

			
	cd ~/Desktop/Dat3M/
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/linux-kernel.cat -m knastertarski -a anderson -i litmus/C/path/to/file.litmus
			
		

Obtain running time of individual tests (without alias analysis).

			
	cd ~/Desktop/Dat3M/
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/linux-kernel.cat -m knastertarski -a none -i litmus/C/path/to/file.litmus
			
		

Linux benchmarks


Replicate Dartagnan vs Herd benchmark plot (Figure 1 right) with whole dataset used in the paper. The script will generate a file ~/Desktop/Dat3M/linux.csv. Expected running time: ~30-40 hours.

			
	cd ~/Desktop/Dat3M
	python3 python/linux.py -p litmus/C -c cat/linux-kernel.cat -s 1800 -v -d linux.csv
			
		

Replicate Dartagnan vs Herd benchmark plot (Figure 1 right) with a subset of tests. The script will generate a file ~/Desktop/Dat3M/linux.csv. Expected running time: ~3 hours.

			
	cd ~/Desktop/Dat3M
	python3 python/linux.py -p cav/linux -c cat/linux-kernel.cat -s 1800 -v -d linux.csv
			
		

Generate plots at ~/Desktop/Dat3M/Plots.pdf.

			
	cd ~/Desktop/Dat3M/
	make
			
		

Obtain running time of individual tests (Dartagnan).

			
	cd ~/Desktop/Dat3M/
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/linux-kernel.cat -m knastertarski -a anderson -i litmus/C/path/to/file.litmus
			
		

Obtain running time of individual tests (Herd).

			
	cd ~/Desktop/Dat3M/
	time timeout 1800 herd7 -I cat -model cat/linux-kernel.cat -bell cat/linux-kernel.bell -macros cat/linux-kernel.def litmus/C/path/to/file.litmus
			
		

Mutual exclusion benchmarks


The commands below can be used to obtain execution time for individual test cases. Replace bound with an integer value of an unroll option that should be tested. Note that values of timeouts below are equivalent to the ones used in the original experiments.


Dartagnan-ARM benchmarks

			
	cd ~/Desktop/Dat3M/
	time timeout 300  java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Parker.pts -unroll bound
	time timeout 300  java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Peterson.pts -unroll bound
	time timeout 300  java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Dekker.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Burns.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Bakery.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Lamport.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/arm.cat -t arm -i benchmarks/Szymanski.pts -unroll bound
			
		

Dartagnan-TSO benchmarks

			
	cd ~/Desktop/Dat3M/
	time timeout 300  java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Parker.pts -unroll bound
	time timeout 300  java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Peterson.pts -unroll bound
	time timeout 300  java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Dekker.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Burns.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Bakery.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Lamport.pts -unroll bound
	time timeout 1800 java -jar dartagnan/target/dartagnan-2.0-jar-with-dependencies.jar -cat cat/tso.cat -t tso -i benchmarks/Szymanski.pts -unroll bound
			
		

FMCAD-ARM benchmarks

			
	cd ~/Desktop/Dat3M-FMCAD/
	time timeout 300  java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Parker.pts -unroll bound
	time timeout 300  java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Peterson.pts -unroll bound
	time timeout 300  java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Dekker.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Burns.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Bakery.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Lamport.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/arm.cat -t arm -relax -i benchmarks/Szymanski.pts -unroll bound
			
		

FMCAD-TSO benchmarks

			
	cd ~/Desktop/Dat3M-FMCAD/
	time timeout 300  java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Parker.pts -unroll bound
	time timeout 300  java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Peterson.pts -unroll bound
	time timeout 300  java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Dekker.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Burns.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Bakery.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Lamport.pts -unroll bound
	time timeout 1800 java dartagnan/Dartagnan -cat cat/tso.cat -t tso -relax -i benchmarks/Szymanski.pts -unroll bound
			
		

Nidhugg-ARM benchmarks

			
	cd ~/Desktop/Dat3M/

	nidhugg --unroll=bound --transform=benchmarks/ParkerU.ll benchmarks/Parker.ll
	time timeout 300 nidhugg -arm benchmarks/ParkerU.ll

	nidhugg --unroll=bound --transform=benchmarks/PetersonU.ll benchmarks/Peterson.ll
	time timeout 300 nidhugg -arm benchmarks/PetersonU.ll

	nidhugg --unroll=bound --transform=benchmarks/DekkerU.ll benchmarks/Dekker.ll
	time timeout 300 nidhugg -arm benchmarks/DekkerU.ll

	nidhugg --unroll=bound --transform=benchmarks/BurnsU.ll benchmarks/Burns.ll
	time timeout 1800 nidhugg -arm benchmarks/BurnsU.ll

	nidhugg --unroll=bound --transform=benchmarks/BakeryU.ll benchmarks/Bakery.ll
	time timeout 1800 nidhugg -arm benchmarks/BakeryU.ll

	nidhugg --unroll=bound --transform=benchmarks/LamportU.ll benchmarks/Lamport.ll
	time timeout 1800 nidhugg -arm benchmarks/LamportU.ll

	nidhugg --unroll=bound --transform=benchmarks/SzymanskiU.ll benchmarks/Szymanski.ll
	time timeout 1800 nidhugg -arm benchmarks/SzymanskiU.ll
			
		

Nidhugg-TSO benchmarks

			
	cd ~/Desktop/Dat3M/

	nidhugg --unroll=bound --transform=benchmarks/ParkerU.ll benchmarks/Parker.ll
	time timeout 300 nidhugg -tso benchmarks/ParkerU.ll

	nidhugg --unroll=bound --transform=benchmarks/PetersonU.ll benchmarks/Peterson.ll
	time timeout 300 nidhugg -tso benchmarks/PetersonU.ll

	nidhugg --unroll=bound --transform=benchmarks/DekkerU.ll benchmarks/Dekker.ll
	time timeout 300 nidhugg -tso benchmarks/DekkerU.ll

	nidhugg --unroll=bound --transform=benchmarks/BurnsU.ll benchmarks/Burns.ll
	time timeout 1800 nidhugg -tso benchmarks/BurnsU.ll

	nidhugg --unroll=bound --transform=benchmarks/BakeryUbound.ll benchmarks/Bakery.ll
	time timeout 1800 nidhugg -tso benchmarks/BakeryU.ll

	nidhugg --unroll=bound --transform=benchmarks/LamportU.ll benchmarks/Lamport.ll
	time timeout 1800 nidhugg -tso benchmarks/LamportU.ll

	nidhugg --unroll=bound --transform=benchmarks/SzymanskiU.ll benchmarks/Szymanski.ll
	time timeout 1800 nidhugg -tso benchmarks/SzymanskiU.ll
			
		

CBMC-TSO benchmarks

			
	cd ~/Desktop/Dat3M/
	time timeout 300  cbmc --unwind bound -mm tso benchmarks/Parker.pts
	time timeout 300  cbmc --unwind bound -mm tso benchmarks/Peterson.pts
	time timeout 300  cbmc --unwind bound -mm tso benchmarks/Dekker.pts
	time timeout 1800 cbmc --unwind bound -mm tso benchmarks/Burns.pts
	time timeout 1800 cbmc --unwind bound -mm tso benchmarks/Bakery.pts
	time timeout 1800 cbmc --unwind bound -mm tso benchmarks/Lamport.pts
	time timeout 1800 cbmc --unwind bound -mm tso benchmarks/Szymanski.pts
			
		

Contacts

If you have any question regarding the artifact, please contact Natalia Gavrilenko, Hernan Ponce-de-Leon or Florian Furbach