Cubicle-W

Overview

Cubicle-W is an extension of the Cubicle model checker that allows to check safety properties of parametrized transition systems under weak memory.

Publications

Parameterized Model Checking on the TSO Weak Memory Model
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In Journal of Automated Reasoning, Volume 64, 2020

Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles
Ph.D. Thesis (in french), Université Paris-Sud, Orsay, September 2018

Cubicle-W: Parameterized Model Checking on Weak Memory
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In Ninth International Joint Conference on Automated Reasoning, Oxford, United Kingdom, July 2018

Parameterized Model Checking Modulo Explicit Weak Memory Models
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In First International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development, Xi'an, China, November 2017

Download

Cubicle-W binary for Mac OSX (Intel 64-bit)
Cubicle-W binary for GNU/Linux (Intel 64-bit)
Cubicle-W binary for GNU/Linux (Intel 32-bit)

GNU/Linux Virtual Machine with Cubicle-W (230 MB)
Login as root, no password, tool is in root home folder
Tested on VirtualBox and VMWare Fusion

Example programs, without the tool
Supplementary litmus tests

Usage

To invoke the tool, simply run the following command:

cubiclew prog.cub

On a correct program, Cubicle-W produces the following output, which just gives some statistics about the analysis:

On an incorrect program, the output also exhibits an execution trace that leads to an incorrect state, as shown below:

Example program: Simple (and naive) Mutual Exclusion for N processes

The following commented example illustrates most of Cubicle-W's input language features.

(* Custom type defining program points *)
type loc = L1 | L2 | L3

(* Program counter for each process - an array indexed by process ids *)
array PC[proc] : loc

(* Global array of booleans, indexed by process ids.
   It will be accessed using a weak semantics. *)
weak array R[proc] : bool

(* The initial state, parameterized by a universally quantified process variable.
   Initially, PC = L1 and R = False for all processes. *)
init (p) { PC[p] = L1 && R[p] = False }

(* The algorithm is unsafe if there exists two process that
   are in the critical section simultaneously (PC = L3) *)
unsafe (p1 p2) { PC[p1] = L3 && PC[p2] = L3 }

(* First transition: if process p is at program point L1,
   then it writes True into R[p] and moves to program point L2.
   The [p] notation in the transition parameters allows to specify
   which process performs the action. *)
transition t1 ([p])
requires { PC[p] = L1 }
{ PC[p] := L2; R[p] := True }

(* Second transition: if process p is at program point L2
   and its previous writes have been comitted, and the value
   of all cells in array R as seen by p is False,
   then process p moves to program point L3. *)
transition t2 ([p])
requires { fence (p) && PC[p] = L2 && forall_other q. R[q] = False }
{ PC[p] := L3 }

(* Third transition: if process p is at program point L3,
   then it writes False into R[p] and moves to program point L1. *)
transition t3 ([p])
requires { PC[p] = L3 }
{ PC[p] := L1; R[p] := False }

Benchmarks

Below are some experimental results comparing Cubicle-W to MEMORAX, Trencher, CBMC and Dual-TSO. The tests were run on a MacBook Pro with an Intel Core i7 CPU @ 2.9Ghz and 8GB of RAM, under OSX 10.11.6. The timeout (TO) was set to 15 minutes. X indicates that the tool gave a wrong answer. KO signifies that the tool crashed. S / US in the second column indicates whether the program is safe (S) or unsafe (US). For parameterized benchmarks, the number between square brackets indicates the number of processes of the instance (N indicates the parametric case). -- indicates parameterized benchmarks that have no counterpart in non-parameterized tools. NT means the benchmark can not be translated because the input language is too restrictive (lacking unbounded arrays or process identifiers).

		Cubicle-W	MEMORAX SB	MEMORAX PB	Trencher	CBMC Unwind 2	CBMC Unwind 3	Dual-TSO
peterson_2	US	0.05s	0.86s	0.25s	0.02s	0.53s	1.02s	0.21s
peterson_2	S	0.06s	0.05s	0.07s	0.01s	1.16s	30.2s	0.29s
dekker_2	US	0.06s	0.08s	0.09s	0.05s	0.95s	5.66s	0.08s
dekker_2	S	0.26s	0.04s	0.08s	0.01s	7.66s	9m07	0.54s
naive mutex	US	0.04s [N]	-- TO [6] 7m54 [5] 13.9s [4]	-- TO [10] 12m02 [9] 1m36 [8]	-- TO [5] 10.1s [4] 0.08s [3]	-- 23.6s [11] 12.7s [10] 10.3s [9]	-- 5m37 [11] 3m39 [10] 2m35 [9]	NT [N] TO [6] 1m12 [5] 2.61s [4]
naive mutex	S	0.30s [N]	-- TO [5] 23.3s [4] 0.16s [3]	-- TO [11] 2m28 [10] 25.2s [9]	-- TO [6] 54.8s [5] 0.31s [4]	-- TO [5] 2m24 [4] 30.3s [3]	-- TO [3] 19.4s [2]	NT [N] TO [5] 35.7s [4] 0.15s [3]
lamport	US	0.10s [N]	-- TO [4] 17.4s [3] 0.23s [2]	-- TO [4] 25.4s [3] 0.16s [2]	-- KO [4] 1.73s [3] 0.05s [2]	-- 7m42 [11] 4m29 [10] 2m23 [9]	-- TO [7] 5m12 [6] 1m21 [5]	NT [N] TO [6] 13m12 [5] 34.6s [4]
lamport	S	0.60s [N]	-- TO [3] 0.14s [2]	-- TO [4] 3m02 [3] 0.21s [2]	-- KO [5] 3.37s [4] 0.08s [3]	-- TO [4] 8m39 [3] 1.71s [2]	-- TO [3] 1m55 [2]	NT [N] TO [4] 9.42s [3] 0.04s [2]
sense_rev	S	0.06s [N]	-- TO [3] 0.34s [2]	-- TO [3] 0.09s [2]	-- X ~~1m58~~ [4] X ~~0.55s~~ [3] X ~~0.01s~~ [2]	-- TO [9] 12m25 [8] 3m34 [7]	-- TO [4] 1m43 [3] 4.97s [2]	NT [N] TO [3] 0.09s [2]
spinlock	S	0.07s [N]	-- TO [5] 8m51 [4] 0.29s [3]	-- TO [7] 9m52 [6] 1.19s [5]	-- TO [7] 21.45s [6] 2.08s [5]	-- TO [3] 19.58s [2]	-- TO [3] 5m08 [2]	TO [N] TO [6] 1m16 [5] 4.08s [4]
arbiter_v1	S	0.18s [N]	-- TO [1+2]	-- TO [1+2]	-- KO [1+5] 4.57s [1+4] 0.54s [1+3]	-- TO [1+6] 12m02 [1+5] 4m14 [1+4]	-- TO [1+3] 44.3s [1+2]	NT [N] TO [1+6] X ~~2m45~~ [1+5] X ~~28.1s~~ [1+4]
arbiter_v2	S	13.5s [N]	-- TO [1+2]	-- TO [1+2]	-- KO [1+4] 1.62s [1+3] 0.09s [1+2]	-- TO [1+4] 2m56 [1+3] 5.84s [1+2]	-- TO [1+2]	NT [N] TO [1+3] 24.2s [1+2]
two_phase	S	54.1s [N]	-- TO [2]	-- TO [4] 39.7s [3] 0.31s [2]	-- TO [4] X ~~7.08s~~ [3] X ~~0.23s~~ [3]	-- TO [11] 12m39 [10] 5m47 [9]	-- TO [11] 13m41 [10] 6m28 [9]	NT [N] TO [3] 12.3s [2]
msi	S	0.05s [N]	-- TO [2]	-- TO [2]	-- 21.2s [6] 3.44s [5] 0.54s [4]	-- TO [2]	-- TO [2]	NT [N] TO [3] 1m41 [2]
moesi	S	0.07s [N]	-- TO [2]	-- TO [2]	-- 12.8s [5] 1.72s [4] 0.24s [3]	-- TO [2]	-- TO [2]	NT [N] TO [2]