Overview
Cubicle is an open source model checker for verifying safety properties of array-based systems. This is a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems.
Cubicle model-checks by a symbolic backward reachability analysis on infinite sets of states represented by specific simple formulas, called cubes. Cubicle is based on ideas introduced by MCMT from which, in addition to revealing the implementation details, it differs in a more friendly input language and a concurrent architecture. Cubicle is written in OCaml. Its SMT solver is a tightly integrated, lightweight and enhanced version of Alt-Ergo; and its parallel implementation relies on the Functory library.
Download
Sources
Cubicle is distributed under
the Apache
licence.
You can download the sources of the latest version of
Cubicle here.
Installation instructions
To compile Cubicle you will need OCaml version 3.11 (or newer) and the Ocaml Functory library version 0.5 (or newer) which can be downloaded here.
Note: You can still compile Cubile without Functory but you will not be able to use its parallel features.
Uncompress the archive and do:
$ cd cubicle-0.5b
$ ./configure
$ make
then with superuser rigths:
# make install
to run Cubicle on a file file.cub
simply do:
$ cubicle file.cub
Publications
| [1] | Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems. In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 718-724, Berkeley, California, USA, July 2012. Springer Verlag. |
Experiments
We have experimented Cubicle on classical and challenging problems (mutual exclusion algorithms and cache coherence protocols) from the literature.
All the following benchmarks have been executed on a 64 bits machine with a quad-core Intel ® Xeon ® processor @ 3.2 GHz and 24 GB of memory. These results were obtained whith version 0.2.5 and the default settings excepted for times followed by * that were obtained with the -geninv option to synthetize invariants. Note that the parallel version of Cubicle was run on 4 cores and that we only give its results for significantly time consuming problems.
| sequential | 4 cores | |
|---|---|---|
| bakery | 0.01s | - |
| Dijkstra | 0.24s | - |
| Distributed Lamport | 3.53s* | - |
| Java-Mlock | 0.04s | - |
| Ricart Agrawala | 4.25s* | - |
| Szymanski_at | 0.12s* | - |
| Berkeley | 0.01s | - |
| flash_aggregated | 0.01s | - |
| German_Baukus | 25.0s | 17.1s |
| German_pfs | 6m23s* | 3m8s* |
| German_undip | 0.17s | - |
| Illinois | 0.02s | - |
| Mesi | 0.01s | - |
| Moesi | 0.01s | - |
| synapse | 0.01s | - |
| Xerox Dragon | 0.01s | - |
Manual
Description language
Cubicle's input language contains some conventional programming constructs (arrays, enumerated and abstract types etc.). However, since we have designed our language with a particular set of protocols in mind, some of its aspects would need to be improved for describing other classes of algorithms.
In Cubicle, array-based systems are described by a set of type declarations, a set of array declarations, an initial configuration, and a transition relation given as a set of parameterized transitions.
The language has four built-in data types: integers
(int),
reals (real), boolean
(bool) and the type of process
identifiers (proc). It also supports
user-defined abstract
and enumerated data types. For instance,
type data
type msg = Empty | Req | Ack
defines an abstract type data, and an enumeration type
msg with the three given values.
The state of a system is described by a set of global variables and
arrays indexed by process identifiers. Thus,
var Memory : data
var Counter : int
array Channel[proc] : msg
describe the state consisting of two global
variables Memory
and Counter, respectively of
type data and
int, and an
array Channel containing values of
type msg.
The initial state is defined by a universal conjunction of
literals characterizing the values for some variables and arrays. For
example, the configuration
where Counter initially equals to
1 and Channel[z]
contains the value Empty
for any process z is expressed by:
init (z) { Counter = 1 && Channel[z] = Empty }
The execution of a parameterized system is defined by a set of
guarded transitions and consists of an infinite loop which
non-deterministically triggers at each iteration a transition whose
guard is true and whose action is to update state variables. Each
transition can take one or several process identifiers as arguments. A
guard is a conjunction of literals (equations, disequations or
inequations) and universal formulas. These formulas must be in
disjunctive normal form and are universally quantified by processes
different from the transition's arguments. Assignments of variables
can possibly be non-deterministic (denoted by := .). Arrays
updates are realized through a case-defined construct where each
condition is expressed as a conjunction of literals and the default
case is denoted by _.
transition send_req(i)
requires
{ Channel[i] = Empty && Counter < 10 &&
forall_other j. (j < i || Channel[j] <> Req) }
{
Counter := Counter + 1 ;
Memory := . ;
Channel[j] := case
| j = i : Req
| _ : Channel[j];
}
The safety property to be verified is expressed in its negated form as
a cube, existentially quantified by distinct processes, and
characterizes unsafe states. The user also has an option to
specify invariants of the system. For instance, the following formula
expresses that a state is unsafe when there exists two distinct
processes z1
and z2 such
that Channel
contains Req for both.
unsafe (z1 z2)
{ Channel[z1] = Req && Channel[z2] = Req }
Options
Cubicle can be run with different options that are shown below:
| -version | Print the version number on stdout and exit. |
| -quiet | Prevent Cubicle from printing the search trace while it performs backward reachability. |
| -depth n | Limit the depth of the search tree to n at maximum. If this limit si excedeed Cubicle will print reach bound on stderr. This value is set to 100 by default. |
| -nodes n | Limit the number of nodes to explore to n at maximum. If this limit si excedeed Cubicle will print reach bound on stderr. This value is set to 100000 by default. |
| -search s | Set the search strategy to s. s can be either breadth-first search (bfs) or depth-first search (dfs) or a variant of DFS (dfsl, dfsh, dfshl). By default, Cubicle explores the search space breadth-first (bfs). |
| -debug | When this flag is present, Cubicle will output cubes that were computed during the pre, and that are being explored. |
| -v | When this flag is present together with -debug, Cubicle will output the result of the pre. |
| -profiling | Tells cubicle to output profiling informations at the end of the search. Such as the time that was spent in computing pre-images, in the fixpoint checks, in computing relevant permutations, in applying substitutions, in the solver, etc. |
| -geninv | Activate invariant discovery during the search. If this flag is present, Cubicle will attempt to synthesize invariants with candidates being subsets of visited nodes that only contain predicates over a unique process variable. Each of these subsets is checked for safety by starting a new resource limited backward reachability analysis. |
| -postpone n | Select the strategy to postpone
nodes. Values for n can be:
|
| -nodelete | Deactivate a posteriori deletion of nodes that become subsumed. |
| -j n | Run Cubicle in parallel on n cores. This option can only be used with the search strategy set to BFS. |
| -h, --help | Display a message with usage and the list of options. |
When running, Cubicle will produce traces on stdout for each
node that is explored. For example, a node with the following
trace
inv_2(#2) -> gnt_shared(#1) -> unsafe
will represent states that can reach the unsafe state by
first applying transistion inv_2 in
process #2 and then applying
transition gnt_shared in
process #1.
If a system is proved unsafe, Cubicle will say so and output a couterexample trace from the inital state to the unsafe state in the same format.
Examples
Below is an example of a simple mutal exclustion algorithm
Mutex:
var Turn : proc
array Want[proc] : bool
array Crit[proc] : bool
init (z) {
Want[z] = False && Crit[z] = False
}
unsafe (x y) {
Crit[x] = True && Crit[y] = True
}
transition req (i)
requires { Want[i] = False }
{
Want[j] := case
| i = j : True
| _ : Want[j]
}
transition enter (i)
requires {
Want[i] = True
&& Crit[i] = False
&& Turn = i }
{
Crit[j] := case
| i = j : True
| _ : Crit[j]
}
transition exit (i)
requires { Crit[i] = True }
{
Turn := . ;
Crit[j] := case
| i = j : False
| _ : Crit[j] ;
Want[j] := case
| i = j : False
| _ : Want[j]
}
Contact
You can contact us at our respective email addresses.