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

Note: The binaries for version 1.0 will be updated soon.

The following are obsolete binaries of version 0.5 for other architectures:

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.0
$ ./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

  1. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières (in French)

    Sylvain Conchon, David Declerck, Luc Maranget and Alain Mebsout.
    In Vingt-Cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014.

    PDF BibTeX
  2. Invariants for Finite Instances and Beyond

    Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi.
    To appear in FMCAD 2013

    PDF BibTeX
  3. Vérification de systèmes paramétrés avec Cubicle (in French)

    Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi.
    In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013.

    PDF BibTeX
  4. Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems

    Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi.
    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.

    PDF BibTeX

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
# procsdepth lim. # statestime # 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:
  • 0: Nodes will not be postponed
  • 1: Postpone nodes that add another process variable (default for BFS)
  • 2: Postpone nodes that do not contribute new information on arrays (default for DFS and variants)
-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.
-v Increases verbosity of debugging information.
-dot Displays search graph (dot must be installed).
Use in conjuction with -v to increase details of the graph (maximum detail at -v -v -v).

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.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.