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.
Documentation and source code can be browsed online.
Binaries
Installation instructions
Opam
If you use the package manager opam, the easiest way to install Cubicle is to do: $ opam install cubicle If you don't (want to) use opam, Cubicle can also be installed manually.
Manual installation
To compile Cubicle you will need OCaml version 4.00.0 (or newer) and the Ocaml Functory library version 0.5 (or newer) which can be downloaded here.
Note: You can still compile Cubicle without Functory but you will not be able to use its parallel features.
Uncompress the archive and do:
$ cd cubicle-1.1.2
$ ./configure
$ make
then with superuser rigths:
# make install
To run Cubicle with the BRAB algorithm on a
file file.cub simply do:
$ cubicle -brab nb file.cub
where nb is the number of different processes that will be
considered for the enumerative forward exploration.
For instance, doing cubicle -brab 2
german.cub will first perform an enumeration of the
states of the German protocol for an instance of the system
with only two processes. The BRAB algorithm will then be
initialized and run with the finite model it just constructed.
Publications
- Inférence d'invariants pour le model checking de systèmes paramétrés (in french)
- Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières (in French)
- Invariants for Finite Instances and Beyond
- Vérification de systèmes paramétrés avec Cubicle (in French)
-
Cubicle: A Parallel SMT-based Model Checker for Parameterized
Systems
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi.
PDF BibTeX
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
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. The first four columns give details on the exploration of the finite instance. The last colum reports the total time of BRAB, i.e. the time needed for the forward exploration plus the time used by backward reachability. You can view more details about each result such as inferred invariants and search graphs by clicking on the name of the benchmark.
| Forward | Backward | Total time | ||||||
|---|---|---|---|---|---|---|---|---|
| # procs | depth lim. | # states | time | # nodes | # inv | # restarts | ||
| German-ish | 2 | ∞ | 23 | 0.01s | 4 | 3 | 0 | 0.03s |
| Szymanski_at | 2 | ∞ | 43 | 0.02s | 31 | 15 | 0 | 0.14s |
| Szymanski_na | 2 | ∞ | 75 | 0.02s | 38 | 16 | 0 | 0.20s |
| German_Baukus | 2 | ∞ | 1497 | 0.02s | 43 | 35 | 0 | 0.25s |
| German.CTC | 2 | ∞ | 1497 | 0.02s | 62 | 27 | 0 | 0.29s |
| German_pfs | 2 | ∞ | 1737 | 0.02s | 49 | 35 | 0 | 0.34s |
| Chandra-Toueg | 2 | ∞ | 148 | 0.02s | 3828 (770 + 1329 + 1729) | 5 | 2 | 2m17s |
| Flash_nodata | 2 | 6 | 439 | 0.02s | 37 | 30 | 0 | 0.36s |
| Flash_buggy | 2 | 6 | 445 | 0.02s | 228 | / | 0 | 2.97s |
| Flash | 3 | 14 | 452,523 | 8.54s | 1047 | 131 | 0 | 5m40s |
Documentation
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. |
| -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. (Do not use in conjunction with -brab.) |
| -h, --help | Display a message with usage and the list of options. |
Options relevant to BRAB
| -brab n | Runs BRAB with a forward exploration with n processes. |
| -forward-depth dmax | Limits the forward exploration to states at depth dmax at maximum. |
| -only-forward | Stops after forward exploration. |
| -candheur nb | Select canditate invariants heuristic with nb (by default nb is the argument of -brab). |
| -v | Increases verbosity of debugging information. |
| -dot level | Displays search graph (dot must be installed) with detail level level (between 0 and 5). |
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 transition 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.
Changelog
1.1.2 2018-01-15
IMPROVEMENTS
* Cubicle Emacs mode on MELPA (package-install cubicle-mode)
BUG FIXES
* Compatibility with OCaml 4.06.0
* Fix arithmetic buc in solver usage (set_cc)
* Configure with OCaml 4.03.0 minimum
* Fix issue with spurious trace replay
1.1.1 2017-06-13
NEW FEATURES
* Option -noqe to disable elimination of constants
BUG FIXES
* Parsing floats and negative reals/integers
* Fix too broad over-approximation with non-deterministic updates
* Fix type bool is now an enumerative data type
1.1 2016-03-17
NEW FEATURES
* Murphi (external tool) as an oracle for performing enumerative forward
(Experimental)
* Macros for predicates/formulas (Experimental)
* Symmetry reduction by normalization in enumerative forward. Can be
disabled with -forward-nosym.
IMPROVEMENTS
* Report solver errors
* Indentation in Why3 certificates
* Stop forward exploration with Ctrl-C and continue with backward
* Sort transitions to not depend on order
BUG FIXES
* Renaming bug in forward
* Certificates: reals/constants and user supplied invariants
* Various fixes in reporting of spurious traces
* Add user supplied invariants in initial formula
* Various fixes in arithmetic
1.0.2 2015-02-09
BUG FIXES
* Create correct actions for preservation of values in Enumerative
* Fix incorrect computation of subtypes in presence of non-deterministic
updates
* Fix replaying of error traces with non-deterministic updates
1.0.1 2014-11-05
NEW FEATURES
* Certificates in Why3 format (Experimental)
* Case constructs for updating global variables
* Disjunctions in transitions' requirements (only dnf for now)
* Option -candheur to (partially) control heuristic for candidate
invarariants extraction
IMPROVEMENTS
* Simplifications in initial formula
BUG FIXES
* Ignore signal USR1 in Windows because it does not exist
1.0 2014-07-21
NEW FEATURES
* New modular architecture with cleaner and more efficient operations
* Code documentation with ocamldoc
* Use of ? instead of . for non-deterministic assignments (conservative
extension: the old syntax is still possible)
IMPROVEMENTS
* More efficient forward (with GC parameters)
* Faster filter when a lot of candidates are not suitable
* New options for controlling candidates generation
* More options for dot search graphs and color by exploration time
* More efficient tries (less allocation)
BUG FIXES
* Report typing errors (at transition level)
* Relevant permutations for multi-dimensional arrays
0.6 2014-01-27
NEW FEATURES
* Refine universal guards by symbolic forward replay to prevent spurious
traces when using BRAB (experimental)
* Certificates (of inductiveness) generation for Alt-Ergo and Why3
* Specify max number of processes with keyword : number_procs
* Show spurious error traces
IMPROVEMENTS
* Use generic parameterized hash functions: faster with OCaml >= 4.00
* Do not add spurious nodes in visited
* More efficient computation of pre-images
* Use ocamlfind for configure
BUG FIXES
* Arithmetic simplifications
0.5 2013-09-04
NEW FEATURES
* BRAB algorithm on top of classical backward reachability
* Generation of search graph in dot (graphviz) format thanks to unsat cores
* Allow non deterministic updates of variables of type other than proc
* Enumerative statefull forward exploration
* Multi-dimensionnal arrays
IMPROVEMENTS
* Copy of cyclic data-structures
* Only use features of the SMT solver that are necessary: congruence
closureand arith are deactivated when not needed
* SAT solver (alt-ergo zero): delay case split once a full propositional
model is found
* Tries for maintaining set of visited nodes (cubes)
* Memoization of (SMT) formula construction
* Check other candidates on faulty traces
BUG FIXES
* SAT solver (alt-ergo zero): Raise sat if full model to avoid vec assert
* Raise error on duplicate updates
0.2.5 2012-04-12
NEW FEATURES
* Complete error traces
BUG FIXES
* Fix bug in initial formula instantiation with global variables
0.2.4 2012-04-11
NEW FEATURES
* Syntactic sugar for simple array updates (A[i] := v)
BUG FIXES
* Pre with correct number of arguments
0.2.3 2012-04-02
BUG FIXES
* Computation of pre for terms of the form A[G]
0.2.2 2012-03-23
NEW FEATURES
* Multiple unsafe properties
* Allow terms of the form A[G] where A is an array and G is a global
variable
0.2.1 2012-01-25
IMPROVEMENTS
* Approximations in arithmetic simplifications
0.2 2012-01-23
* First public release of Cubicle
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.