DIVINE: The Parallel & Distributed Model Checker

1 Introduction

The DIVINE project aims to develop a general-purpose, fast, reliable and easy-to-use model checker. The roots of the project go back to a special-purpose, explicit-state, asynchronous system model checking tool for LTL properties. However, the landscape of software development is changing, and rigorous, inflexible development processes are in a steady decline, being displaced by more agile, flexible and dynamic methods. In the agile world, there is little place for large-scale, long-term planning and pondering on “paper only” designs, which would favour the use of a traditional model checker.

A new incarnation of DIVINE strives to keep up with this dynamic world, bringing “heavy-duty” model checking technology much closer to daily programming routine. However, DIVINE is not abandoning traditional modelling formalisms; in fact, our support for dedicated modelling languages is better and broader than ever. Nevertheless, our major goal is to express model checking problems in a language which every developer is fluent with: the programming language of their own project. Even if you don’t apply model checking to your resulting program directly, writing throwaway models makes much more sense in a language you understand well and use daily.

Current versions of DIVINE provide out-of-the box support for the C programming language (C99), including most of the standard library, and for C++ (C++11). Additionally, users can compile and use other libraries, including the standard C++ library.

2 Installation

If you are using the Windows installer, just execute the downloaded file and follow the installation wizard. Consult your distribution’s manual for instructions on installing binary packages. The rest of this section is only relevant when you are installing from source.

We will assume that you have obtained a source tarball from http://divine.fi.muni.cz, eg. divine-3.0.tar.gz.

2.1 Prerequisites

2.2 Instructions

First, unzip the distribution tarball and enter the newly created directory

$ tar xvzf divine-3.0.tar.gz
$ cd divine-3.0

2.2.1 Configuration

$ ./configure

The configure script will tell you what options you have available and what external packages you may be missing. To inspect configuration variables in more detail, you can use ccmake:

$ (cd _build ; ccmake .)

Edit the variable content to your liking and use c and g keys to re-run configuration and re-generate makefiles, respectively.

2.2.2 External Programs

Some parts of DIVINE, especially the compile and combine sub-commands will need to run external tools. By default, DIVINE will expect to find these commands in your PATH under their common names. Please pay close attention to the CMD_ variables, as they are not checked at configure time, especially if your system provides multiple versions of LLVM. While you can override the commands to use on DIVINE’s command-line later (using --cmd-xxx=yyy switches), this may be inconvenient.

NB. Please take extra care that the “GNU gold” linker you are providing to DIVINE has plugin support, and that you provide correct path to the LLVMgold.so plugin. A working installation of both is mandatory for divine compile --llvm. Moreover, you must provide matching versions of clang, the llvm tools and the LLVMgold.so plugin (most importantly, they must all be based on the same LLVM version as your DIVINE build!). Version mismatches will lead to bitcode linking or loading failures. Finally, versions of clang prior to 3.2 will fail to correctly compile the C standard library provided by DIVINE.

Alternatively, you can use --cmd-* options to divine compile --llvm at runtime to specify the correct tools to use.

2.2.3 Build and Installation

When you are satisfied with the configuration options, start the build with:

$ make

and relax, this is going to take a while. When the build is done, you should check that your installation is working as expected:

$ cd _build/tools
$ ./divine help
$ ./divine verify ../../examples/dve/shuffle.dve
$ ./divine verify -p LTL ../../examples/dve/peterson-liveness.dve
$ ./divine verify -p LTL ../../examples/dve/peterson-naive.dve

You can also run the test-suites, to ensure that DIVINE is working properly on your system and with your versions of libraries and tools:

$ make check

While there is no need to install the binary (it is self-contained and you can move or copy it to a location of your choice), you can easily install DIVINE system-wide for convenient access:

# make install

3 Using the DIVINE commandline interface

The main interface to DIVINE is the command-line tool simply called divine. Additionally, some of the functionality is also available via divine.ide which is documented separately. DIVINE supports a number of input languages and not all features are available with all input languages. These limitations are documented here. Additionally, since DIVINE has many build dependencies and needs substantial amount of RAM and disk space to compile, many features can be disabled at compile time to reduce some of these requirements. The binary will normally give you an explanation if you request an operation that has been disabled at compile time. To get a list of options your divine binary has been compiled with, simply issue

$ divine --version
DIVINE version 3.0
Version: 3.0
Build-Date: 2013-10-17, 13:17 UTC
Pointer-Width: 64
Debug: enabled
Compile-Flags: POSIX DVE HASH_COMPACTION COIN LLVM
MPI-Version: n/a
Architecture: Intel(R) Core(TM) i7-3520M CPU @ 2.90GHz

3.1 Synopsis

divine info <model file>
divine combine [-f <formula file>] <model file>
divine compile [--cesmi|--llvm] <model file>
divine draw [...] <model file>
divine metrics [...] <model file>
divine verify [...] <model file>
divine simulate [...] <model file>

3.2 Printing Model Metadata

divine info {model}

To obtain basic data about a model, use divine info. The key part of the information provided is the list of properties available in the model, and the name of a property that needs to be passed to the --property option of draw, metrics or verify subcommands:

$ divine info examples/dve/peterson-liveness.dve
Available properties:
 * deadlock: deadlock freedom
 * assert: assertion safety
 * LTL: Büchi neverclaim property

In this case, the model has three properties, deadlock, assert and LTL (the last being a neverclaim property generated from an LTL formula, see the section on divine combine below).

3.3 Using LTL Properties

divine combine [-f formula.ltl] [-p N] [-o] [-q] model.dve
divine combine [-f ...] [...] model.mdve [P1=VAL] [P2=VAL] ...

Some of the input languages have intrinsic support for specifying LTL properties. In these cases, all suitable LTL properties are automatically made available for model checking via the --property switch to divine verify (see below). However, since the DVE language currently lacks support for specifying LTL directly, the formulas need to be provided in a separate file with an .ltl suffix. The combine subcommand can be used to translate the LTL formula into an Büchi automaton which is then included in the DVE file. One DVE file is generated for each LTL formula found in the .ltl file. The .ltl file would look, for example, like this:

#define a_0 (active == 0)
#define a_1 (active == 1)

#define w_0 (waiting[0] == 1)
#define w_1 (waiting[1] == 1)

#define c_0 (P_0.CS)
#define c_1 (P_1.CS)

#property G(F(c_0)) && G(F(c_1))
#property ((GF(a_0 && w_0)) -> GF(c_0)) && ((GF(a_1 && w_1)) -> GF(c_1))

Each #define gives a symbolic name for an atomic proposition, and each #property specifies a single LTL formula. Without the -p (--property) and -o (--stdout) options, the output of divine combine looks like this:

$ divine combine peterson.dve -f peterson.ltl
peterson.prop1.dve: G(p0cs->F(!p0cs))
peterson.prop2.dve: G((!p0cs)->Fp0cs)
peterson.prop3.dve: GFsomeoneincs

$ divine verify peterson.prop1.dve
...

To pick a specific formula, use -p N (with N being the sequence number of a #property in the .ltl file, in this case 1 or 2). When -p is in effect, -o can be used to direct the generated DVE file to standard output.

Syntax of LTL formulas as accepted by DIVINE is as follows:

F :== un_op F | F bin_op F | (F) | term
un_op :== '!' (logical negation)
    :== 'X' | 'O' (next)
    :== 'F' | '<>' (future)
    :== 'G' | '[]' (globally)
bin_op :== '&&' | '*' (and)
    :== '||' | '+' (or)
    :== '->' (implication)
    :== '<->' (equivalence)
    :== '^' (xor)
    :== 'U' (until)
    :== 'V' | 'R' (release)
    :== 'W' (weak until)
term :== 'true' | 'false'
    :== {_a-z}[_0-9a-z]*  (name of an atomic proposition)

3.4 Configuring the Parallel Model Checking Engine

Many of the algorithms DIVINE can use are parallel and optionally distributed. Both metrics and in common cases the verify subcommand will use a parallel algorithm to explore the state space of the system. All the parallel algorithms have a number of parameters in common, and we will discuss them in this section.

divine {metrics|verify} [--statistics [--curses]]
                        [-w N|--workers=N]
                        [--max-memory=N]
                        [--max-time=N]
                        [--disk-fifo=N]
                        [--seed=N]
                        [-i N|--initial-table=N]
                        [--hash-compaction]
                        [--compression]
-w N | --workers=N
The number of threads to use for verification. The default is 2. For optimal performance, each thread should get one otherwise mostly idle CPU core. Your mileage may vary with hyper-threading (it is best to run a few benchmarks on your system to find the best configuration).
--max-memory=N
Limit the amount of memory divine is allowed to allocate. This is mainly useful to limit swapping. When the verification exceeds available RAM, it will usually take extremely long time to finish and put prohibitive strain on the IO subsystem. It is recommended that you do not allow divine to swap excessively, either using this option or by other means.
--max-time=N
Put a limit of N seconds on the maximal running time.
--disk-fifo
Most of the memory used by the verifier is split between hash tables and queues. This option tells divine to use disk storage for long queues, since the impact of high latency is much smaller for queues than it is for hash tables. This allows more of RAM to be used for hash tables, improving overall performance for large models. Location of temporary files can be changed by setting TMPDIR, TEMP or TMP environment variables.
--statistics [--curses]
Print realtime statistics during verification, optionally using curses for neater output. Useful as entertainment, for diagnosing performance issues and to impress laymen.
--compression
Use lossless compression of state space to reduce memory consumption of verification. The default compression method is tree compression. See state space compression on details of compression.
--shared
This option switches between two graph traversal algorithms. Use this switch to turn on Shared algorithm instead of Partitioned algorithm. Default option is to use Partitioned algorithm. See graph traversal algorithms on details.

3.5 Distributed Execution

DIVINE can be built with support for MPI-based distributed verification. To execute DIVINE across multiple machines, you should use mpiexec or mpirun from your MPI distribution (consult your MPI manual for details and exact invocation parameters you need). An usual invocation will look like this:

$ mpiexec -H hostname1,hostname2 divine -w 4 model.dve

This command will execute DIVINE on 2 machines specified with -H, using 4 worker threads on each (for a total of 8 threads). You should make sure that your DIVINE binary is available on $PATH for non-interactive ssh commands (try running ssh hostname1 divine). Alternatively, you can specify an absolute path to your DIVINE binary, assuming it lives in the same place across all machines. Finally, input file(s) to DIVINE need to be available on each machine as well, using the same path used in your invocation.

3.6 State Space Metrics, Visualisation & Exploration

divine metrics [--reduce=R] [--no-reduce] [--fair]
               [--report[=<report format>] | -r]
               [--property=N] [--fair]
               [engine options]
               <model file>

The metrics sub-command runs a simple reachability on the entire state space of a system, reporting summary statistics. This is the most efficient algorithm in DIVINE that explores the state space, both in terms of memory and CPU, although only by a slight margin. See next section on details of the model-related switches and reporting.

divine draw [--distance=N] [--trace=N,N,N...]
            [-l|--labels|--trace-labels]
            [--bfs-layout]
            [--reduce=R] [--no-reduce] [-f|--fair]
            [--render=<cmd>|-r <cmd>]
            [--compression]

To visualise (a part of) the state space, you can use divine draw, which creates a graphviz-compatible representation. By default, it will run “dot -Tx11” to display the resulting graph. You can override the drawing command to run by using the -r/--render switch. The command will get the dot-formatted graph description on its standard input.

Additionally to displaying the graph itself, draw can be instructed to visualise a (presumably counter-example) trace in the graph. Use the --trace switch to supply a trace, in the same format as the verify command uses for counter-examples in the report, using its --report option (you can cut&paste the CE-Init line from the report, to which you can optionally append the CE-Cycle list, separated by a comma, to obtain the full lasso-shape counterexample when working with LTL/neverclaim properties).

divine simulate [--distance=N] [--trace=N,N,N...]
                [--reduce=R] [--no-reduce] [-f|--fair]

The simulate sub-command is used to interactively explore a state space in a terminal. Use ? in the interactive prompt to obtain help on available commands. You can also use simulate non-interactively, supplying a succession of numbers (using the --trace switch analogous to that of draw, see above).

3.7 Model Checking

divine verify [--reachability|--owcty|--map|--nested-dfs]
              [--property=<name> | -p <name>]
              [--fair]
              [--reduce=<reduction>]
              [--report[=<report format>] | -r]
              [--no-counterexample | -n]
              [--display-counterexample | -d]
              [engine options]
              <model file>

This command is the main workhorse of model checking. It automatically selects an appropriate algorithm for model checking based on the property type, and an appropriate model loader / state space generation backend according to the input file.

$ divine verify examples/dve/peterson-liveness.dve --property=deadlock --no-reduce
  searching...  736677 states, 2848427 edges
 =====================================
           The property HOLDS
 =====================================

3.7.1 Options

--reachability, --owcty, --map, --nested-dfs
Override the algorithm to use.
--property=name | -p name
Select which property to model-check. Use divine info to obtain a list of properties available in any given model. Defaults to deadlock.
--fair
Only consider runs that are weakly fair. This option is only currently available for DVE models and is mainly useful when checking LTL properties. This avoids counterexamples which rely on one of the processes of the system never making any progress even though it is not blocked. For timed models, this option excludes Zeno runs when verifying LTL properties.
--reduce=X, --no-reduce
This option directs the model checker to use heuristics which usually make the process faster and/or use less memory. Not all reductions are available with all model types. The default is to enable all reductions, namely tau+,taustore,heap,por. To disable state space reductions, specify --no-reduce. In addition, tau is available as a weaker alternative to tau+. The tau, taustore and heap reductions are only available with the LLVM backend. The por reduction is available with CoIn and DVE inputs and may be available with some CESMI models. To specify multiple reductions, provide them as a comma-separated list.
--no-counterexample | -n
Disable generation of counterexamples. This is mainly useful for benchmarking verification speed.
--report[=<report format>] | -r

At the end of a verification run, produce a comprehensive, machine-readable report.

There are several formats of reports supported by DIVINE. Also it is possible to specify --report option repeatedly to get multiple reports (for example to file and on console).

The value of <report format> can be one of:

text
Report good for both machine and human readability, produced on standard output.
text:file
Same as text but output is saved to given file (which is overwritten if already present).
plain
Similar to text but optimized for machine readability, without empty lines.
plain:file
plain into file.
sql:table:ODBC connection string

Report is saved into given table of database, ODBC with given connection string is used to connect to database. This feature requires DIVINE compiled with ODBC support.

The report is saves as follows: for every line of report (in text format) the table column name is derived from value name (which is converted to lowercase and all non alphanumeric characters are converted to underscode). Then table is queried for available column names and columns which are both in table and in report are saved (as text).

If table is not present DIVINE will attempt to create it. Automatically created table will contain all collumns of report.

3.8 DIVINE Explicit State Space Generator

divine gen-explicit [--fair] [--reduce=<reduction>]
                    [--report[=<report format>]]
                    [engine options]
                    [--no-save-states]
                    [-o <file> | --output=<file>]

The gen-explicit subcommand can be used to generate the entire state-space of a model into file which can then be processed either by DIVINE or any other tool capable of loading DIVINE Explicit State Space Format.

The output file contains both forward and backward edges of the state space and may contain the memory associated with each node of the state space. Please note that the size of the output file approximately corresponds to the amount of memory required for verification (it is smaller if state memory is omitted, though).

The gen-explicit command can run in parallel and can use MPI, but it is not yet available in conjunction with the --shared option. If gen-explicit is used with MPI, it expects that the output file is located on a shared filesystem (for example NFS).

3.9 State Space Compression

DIVINE supports lossless state space compression based on tree compression. This compression mechanism is particularly efficient on large models with relatively large state vectors (individual states). Therefore LLVM and timed automata verification benefits the most from state space compression – the compression can often reduce large state spaces (several gigabytes and more) to less than one tenth of their original size. Also, for these modelling formalisms, the time overhead from compression is usually negligible.

The compression is supported by all verification algorithms and can be enabled by supplying the --compression switch (alternatively, --compression=tree). The following DIVINE commands allow compression option: metrics, verify, gen-explicit, draw.

There are no limitations on other options implied by use of compression, it is supported with parallel verification (including MPI); however, to achieve best compression ratio it is recommended to use shared-memory verification (--shared), if possible.

3.10 DIVINE Graph Traversal Algorithms

DIVINE implements two different graph traversal algorithms. Both of them are designed to run in parallel environment and they implements pseudo BFS. However, each of them has different pros and cons and is suitable for different situations.

3.10.1 Partitioned

The main idea of this algorithm is that a graph is partitioned into parts where each part is assigned to exactly one working thread (and vice versa, every thread has exactly one part of a graph). DIVINE generates a graph “on the fly” so it is not possible to anyhow analyse the particular graph in advance, in order to optimize the partitioning. That is the reason why the partitioning is done via hashing nodes of a graph, which may cause imbalanced and heavy communication workload.

Every working thread has an independent store (simple hash table) for already visited nodes of the graph and a queue of nodes to-be-processed. Due to the independence of partitioning no synchronizations are required for standard operations. This is not the case with Shared algorithm (see below), therefore the performance of single threaded run of DIVINE is better if Partitioned algorithm is used. However, the independence implies worse efficiency of the tree compression, in other respects this algorithm can run in distributed environment without any penalty (except network cost).

3.10.2 Shared

When using Shared algorithm, no partitioning is done. Two main data structures – the store and queue – are shared among all working threads. A working thread pushes already processed nodes of a graph into the store, and takes to-be-processed nodes from the queue. Shared algorithm is significantly better than the previous one when is DIVINE is supposed to be run on a multi-core machine with high amount of memory.

The store is a hash table that allows for parallel access. This data structure is limited to only three operations – insert, find, and grow. Our implementation in DIVINE does not use explicit locks, although it contains a few global implicit locks (or better atomic flags) to ensure correctness.

The grow operation can also be done in parallel with a support of independent participating working threads (besides the thread that called grow). Anyway, more participating workers may improve the time needed for rehashing the old table into the new one.

The usage of the tree compression together with Shared algorithm significantly decreases amount of memory needed by DIVINE. However, Shared algorithm is not the best choice for single threaded run due to a small performance penalty caused by synchronizations inside the hash table.

As of time of this writing Shared algorithm cannot run in a distributed memory.

3.11 Compiling

The command divine compile can be used to compile either CESMI module or DVE model into native code or C/C++ code into LLVM bitcode. See model checking C and C++ code for more details. The mode of compilation is recognized by an extension of name of input file in some cases – .dve for DVE models, .m for MURPHI models. The default mode of compilation is to compile C/C++ program via clang into LLVM bitcode. The selection of compilation CESMI module may be done by specifying -c or --cesmi option.

divine compile [-j N|--jobs=N]
               [-l|--llvm]
               [-c|--cesmi]
               [--keep-build-directory]
               [--cflags=<flags>|-f <flags>]
               [--libraries-only]
               [--precompiled=<path>]
               [-o <name>|--output-file=<name>]
               [--cmd-clang=<value>]
               [--dont-link]
               [--no-modeline]
               [-D <definition> | --definition=<definition>]
               [--snapshot=<path>]
               [--stdin=<path>]
               <file input>
-j N | --jobs=N
Enable parallel build. If not specified, N is assumed to be 1.
-l | --llvm
Set compilation mode explicitly to build an LLVM bitcode. This option is suppressed when extension of the input file is .dve or .m. Without this option a warning is emitted if compilation mode defaulted.
-c | --cesmi
Set compilation mode to build a CESMI module.
--keep-build-directory
This option prevents from deletion of a temporary build directory.
-f <flags> | --cflags=<flags>
This option is used to pass additional arguments to a compiler.
--libraries-only
By specifying this option DIVINE compiles only libraries such as libc++, PDCLib, and virtual file system. The compiled libraries may be later used repeatedly. This option is recognized only when LLVM bitcode is compiled. This option does not use any other file input.
--precompiled=<path>
Path to a directory where pre-compiled libraries are placed. The libraries are to be linked with the verified program. This option is recognized only when LLVM bitcode is compiled.
-o <name> | --output-file=<name>
Specify a name of a product of the compilation.
--cmd-clang=<value>
Set how to run clang. Useful when default path is not correct.
--dont-link
Compile the source files, but do not link. This option is recognized only when LLVM bitcode is compiled.
--no-modeline
Disable DIVINE modeline parsing. Modelines are used in examples of C/C++ programs to automatically set --cflags.
-D <definition> | --definition=<definition>
Add definition for generator, can be specified multiple times. This option is recognized only when DVE model is compiled.
--snapshot=<path>
DIVINE takes a snapshot of the specified directory which becomes a root of the virtual file system. This option is recognized only when LLVM bitcode is compiled.
--stdin=<path>
DIVINE uses the specified file to be the standard input for the verified program (file descriptor 0, therefore stdin and std::cin). This option is recognized only when LLVM bitcode is compiled.

4 An Introduction to Using DIVINE

In this section, we will give a short example on how to invoke DIVINE and its various functions. First of all, we need a “model” or “system” to work on. This is the main input file to DIVINE, and can come in a few different formats. It could be a LLVM bitcode file, a CESMI shared object, a DVE model or a UPPAAL model. The workflow is very similar for all input languages, although the details vary. We will use a C program as an example “system” in this section, along with a few simple properties. You may have noticed that “C program” was not listed as an input option above – this is because DIVINE does not directly understand C programs. They first need to be translated into LLVM bitcode, and DIVINE can work with that.

4.1 System Modelling Basics

We will start with a simple C program with 2 threads and a single shared variable:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
#include <pthread.h>

int i = 33;

void* thread( void *x ) {
    i ++;
    return NULL;
}

int main() {
    pthread_t tid;
    pthread_create( &tid, NULL, thread, NULL );

    i ++;

    pthread_join( tid, NULL );
    assert( i == 35 );
    return i;
}

(Yes, this program clearly has a bug in it, a race condition on the update of i. We will deal with that later.)

The program as it is can be compiled using your system’s C compiler just fine (assuming access to pthread.h) and you can try running it. To use DIVINE, we will need to compile it a little differently:

$ divine compile --llvm program.c

This command will take a while, as it builds an entire runtime environment for our small program. Nevertheless, after a while, it will produce a file, program.bc. This file contains LLVM bitcode of our program, and of the runtime environment. We can learn a little more about the program using divine info:

$ divine info program.bc
Available properties:
 * deadlock: deadlock freedom
 * assert: assertion safety

We can analyse the bitcode file a little more, actually exploring its entire state space, measuring it (we won’t be asking about any properties of the program yet):

$ divine metrics program.bc
 input: program.bc
 property deadlock: deadlock freedom
 ------------------ Metrics ------------------
  exploring...           done
 =============================================
          25 states
          42 transitions
           0 accepting
           2 deadlocks
 =============================================

One thing you might notice off-hand is that DIVINE said that there are deadlocks in the program. This sounds strange at first, but the notion of a “deadlock” in DIVINE is not the same as you would expect in a C program. In many other formalisms out of the spectrum supported by DIVINE, any system state for which there are no legal successor states is considered a deadlock. For our C program, this is what happens when the program exits. Hence, terminating C programs will always have some “deadlocks” in them – this is no reason for concern. Moreover, a real deadlock in a C program will appear as a loop in the state space, and we will need a different approach for detection of such deadlocks.

Anyhow, we have learned that our program has 25 unique states and there are 42 transitions between these states. By default, DIVINE tries to use the most efficient reduction available which is still exact (i.e. it will not use hash-compaction or other approximation techniques unless explicitly enabled). We can try turning off those reductions to see what happens:

$ divine metrics program.bc --no-reduce
 input: program.bc
 property deadlock: deadlock freedom
 ------------------ Metrics ------------------
  exploring...           done
 =============================================
         531 states
        1019 transitions
           0 accepting
           2 deadlocks
 =============================================

With the LLVM backend, this basically means that a new state is generated after each instruction in any of the threads. The difference may be far less dramatic with different input languages though. One thing to keep in mind is that state-space reductions can be expensive to compute, even if they save memory. Especially for DVE models, if verification seems slow, you can try disabling reductions.

4.2 Property Verification & Counter-Example Analysis

Now let’s turn to some more interesting properties. With the above program, the first thing that comes to mind is asking DIVINE whether the assertion in the program can ever be violated:

$ divine verify program.bc -p assert
 input: program.bc
 property assert: assertion safety
 ---------------- Reachability ----------------
  searching...  20 states, 32 edges, GOAL
 =============================================
           The property DOES NOT hold
 =============================================

Here, as we have anticipated, DIVINE tells us that in fact, the assertion can be violated. However, in itself, this is not extremely helpful: we would also like to know why this is so. Let’s try to get a counterexample:

$ divine verify program.bc -p assert -d
 input: program.bc
 property assert: assertion safety
 ---------------- Reachability ----------------
  searching...  20 states, 32 edges, GOAL
 =============================================
           The property DOES NOT hold
 =============================================

===== Trace from initial =====

global: [ i = 33 ]
0: <main> << %tid = alloca i32, align 4 >> [ tid = 0 ]

global: [ i = 33 ]
0: <pthread_create> [ pthread.cpp:328 ] (internal)

global: [ i = 33 ]
0: <pthread_create> [ pthread.cpp:354 ] (internal)
1: <_Z14_pthread_entryPv> << %1 = alloca i8*, align 8 >> (internal)

global: [ i = 33 ]
0: <pthread_create> [ pthread.cpp:354 ] (internal)
1: <thread> [ ../program.c:6 ] [ x = 0 ]

global: [ i = 33 ]
0: <main> [ ../program.c:14 ] [ tid = @(3:0| 65537) ]
1: <thread> [ ../program.c:6 ] [ x = 0 ]

global: [ i = 34 ]
0: <pthread_join> [ pthread.cpp:392 ] (internal)
1: <thread> [ ../program.c:6 ] [ x = 0 ]

global: [ i = 34 ]
0: <pthread_join> [ pthread.cpp:392 ] (internal)
1: <_Z14_pthread_entryPv> [ pthread.cpp:289 ] (internal)

global: [ i = 34 ]
0: <pthread_join> [ pthread.cpp:392 ] (internal)
1: <_Z14_pthread_entryPv> [ pthread.cpp:319 ] (internal)

===== The goal =====

global: [ i = 34 ]
0: <null> []
1: <_Z14_pthread_entryPv> [ pthread.cpp:319 ] (internal)
ASSERTION FAILED (thread 0): <main> [ ../program.c:17 ]

First, we notice the “goal” state (the one that violates the property, in this case assertion safety) near the end of the output. It shows that thread 0 has terminated, thread 1 is in an internal pthread routine and that it passed through a failing assertion at line 17 of our program.c.

Indeed, line 17 is our assert( i == 35 ). Now let’s walk through the trace from the beginning to understand what is going on. Each block (delimited by blank lines) in the counterexample represents a single state of the system. We see a single global variable, i and its value (which is 33 in the first state). Each further line in a block describes a single thread. At the beginning there is only one thread, executing our main function (shown in angle brackets), and the value of our local variable tid is 0 (shown in square brackets).

The program proceeds to call pthread_create, and in the following state, we notice that a new thread has appeared (for now, executing an internal routine). It immediately jumps into thread, the function we provided to pthread_create as an entry point. We quickly reach a point where both threads are executing their respective i ++ statements at once (program.c:6 and program.c:14 respectively). This is where the problem happens, and we see that both threads eventually pass the statement, but value of i remains at 34.

Please note that the exact format of a state description depends on the input language. However, the gist is always the same.

5 Model Checking C and C++ Code via LLVM Bitcode

The traditional “explicit-state” model checking practice is not widely adopted in the programming community, and vice-versa, use of mainstream programming languages is not a common practice in the model checking community. Hence, model checking of systems expressed as C programs comes with some novelties for both kinds of users.

First of all, the current main application of DIVINE is verification of safety (and some liveness) properties of asynchronous, shared-memory programs. The typical realisation of such asynchronous parallelism is programming with threads and shared memory. Often for performance and/or familiarity reasons, programming with threads, shared memory and locking is the only viable alternative, even though the approach is fraught with difficulties and presents many pitfalls that can catch even expert programmers unaware – not to say novices. Sadly, resource locking is inherently non-compositional, hence there is virtually no way to provide a reliable yet powerful abstraction, all that while retaining any semblance of speed and scalability.

Despite all its shortcomings, lock-based (or alternatively atomics-based, which is yet more difficult) programming is on a rise. Model checking provides a powerful tool to ascertain correctness of programs written with locks around concurrent access to shared memory. Most programmers will agree that bugs that show up rarely and are nearly impossible to reproduce are the worst kind to deal with. Sadly, most concurrency bugs are of this nature, since they arise from subtle interactions of nondeterministically scheduled threads of execution. A test-case may work 99 times out of 100, yet the 100th time die due to an unfathomable invalid memory access. Even sophisticated modern debugging tools like valgrind are often powerless in this situation.

This is where DIVINE can help, since it systematically and efficiently explores all relevant execution orderings, discovering even the subtlest race conditions, restoring a crucially important property of bugs: reproducibility. If you have ever changed a program and watched the test-case run in a loop for hundreds of iterations, wondering if the bug is really fixed, or it just stubbornly refuses to crash the program… well, DIVINE is the tool you have been waiting for.

Of course there are some catches. Model checking is computationally intensive and memory-hungry. While this is usually not a problem with comparably small unit tests, applying model checking to large programs may not be feasible – depending on your use-case, and on the amount of memory and time that you have.

With the universal LLVM backend, DIVINE can support a wide range of compiled programming languages. However, language-specific support is only provided for C and C++. A fairly complete ISO C runtime library is provided as part of DIVINE, with appropriate hooks into DIVINE, as well as an implementation of the pthread specification, i.e. the POSIX threading interface. Additionally, an implementation of the standard C++ library is bundled with DIVINE. Besides the standard library, DIVINE also provides an adapted version of the runtime library required by C++ programs to implement runtime type identification and exception handling; both are fully supported by DIVINE.

If your language interfaces with the C library, the libc part of language support can be re-used transparently. However, currently no other platform glue is provided for other languages. Your mileage may vary. Data structure and algorithmic code can be very likely processed with at most trivial additions to the support code, in any language that can be compiled into LLVM bitcode.

5.1 Compiling Programs

The first step to take when you want to use DIVINE for C/C++ verification is to compile your program into LLVM bitcode and link it against the DIVINE-provided runtime libraries. When you issue divine compile --llvm program.c, divine will compile the runtime support and your program and link them together automatically, using clang. You can use --libraries-only (without a program) to pre-build the bitcode library which includes the C and C++ libraries and platform glue: libdivinert.bc. When you have this files in the correct data layout (basically, on common x86 platforms, this boils down to whether your clang is configured to use 32b or 64b pointers), you can re-use them with later divine compile --llvm invocations by adding the --precompiled=/path/to/the/libraries switch. Please be sure that you always use libraries built by a matching version of DIVINE. To change the switches passed to clang when you compile your program, use --cflags.

Alternatively, you can compile your program manually (possibly to use gcc/dragonegg instead of clang) and link the resulting bitcode with DIVINE’s runtime libraries mentioned above. You can pass the bitcode file corresponding to the library to divine compile --llvm as an additional input. Assuming that you now have a program.bc file, you should proceed to check that DIVINE can load it, by issuing divine info program.bc. Your program might be missing some symbols, as the LLVM linkers currently fail to report when this happens, in which case DIVINE will report the problem upon loading the file.

5.2 Limitations

When DIVINE interprets your program, it does so in a very strictly controlled environment, so that every step is fully reproducible. Hence, no real IO is allowed; the program can only see its own memory. DIVINE can simulate IO by using virtual file system, which is done by implementation of subset of POSIX interface; see Virtual File System.

While the pthread interface is fully supported, the fork system call is not: DIVINE cannot verify multi-process systems at this time. Likewise, C++ exceptions are well-supported but the C functions setjmp and longjmp are not yet implemented.

The interpreter simulates an “in order” architecture, hence any possible detrimental effects of instruction and memory access reordering won’t be detected. Again, an improvement in this area is planned for a future release.

5.3 Virtual File System

The virtual file system can create a snapshot of a directory tree by --shapshot=path/to/the/directory and/or a snapshot of a file by --stdin=path/to/the/file which will be used as a keyboard (file descriptor 0, therefore as stdin and std::cin). Both options are recognized during compilation of the bitcode library so snapshots can be pre-compiled, however any change in snapshots requires recompilation of the bitcode library.

Functions handle errors during their execution by returning an error value and setting errno to a value specified by the documentation. Variadic functions (open, openat) are also checked whether correct number of arguments is passed, if not, the verification is stopped and the problem is reported to the user. Wrong usage of pipes (i.e. closed reader when writing, opening pipe both for reading and writing) also causes stopping the verification and making the report.

The virtual file system currently implements following header files and functions:

sys/stat.h:
fstat, stat, lstat, fstatat, chmod, fchmod, fchmodat, umask, mkdir, mkdirat, mkfifo, mkfifoat

sys/types.h

dirent.h:
closedir, dirfd, fdopendir, opendir, readdir, readdir_r, rewinddir, scandir, seekdir, telldir
fcntl.h:
creat, open, openat
unistd.h:
close, read, write, pread, pwrite, pipe, lseek, dup, dup2, ftruncate, truncate, unlink, rmdir, unlinkat, link, linkat, symlink, symlinkat, readlink, readlinkat, access, faccessat, chdir, fchdir, fsync, fdatasync, isatty, ttyname, ttyname_r, swab, sync, syncfs

See examples/llvm/ipc_emulation.c and examples/llvm/simple_io.cpp for details how to use the virtual file system.

5.4 State Space of a Program

Internally, DIVINE constructs the state space of your program – an oriented graph, whose vertices represent various states your program can reach, i.e. the values of all its mapped memory locations, the values in all machine registers, etc. DIVINE normally doesn’t store, or even construct, all the possible states – only a relevant subset. In a multi-threaded program, it often happens that more than one thread can run at once, i.e. if your program is in a given state, the next state it will get into is determined by chance – it all hinges on which thread gets to run. Hence, some (in fact, most) states in a parallel program can proceed to multiple different configurations, depending on a scheduling choice. In such cases, DIVINE has to explore both such “variant” successors to determine the behaviour of the program in all possible scenarios.

You can visualise the state space DIVINE explores by using divine draw – this will show how the “future” of your program branches through various configurations, and how it converges back into a common point – or, if its behaviour had changed depending on scheduling, diverges into multiple different outcomes.

5.5 Non-Deterministic Choice

Scheduling is not the only source of non-determinism in typical programs. Interactions with the environment can have different outcomes, even if the internal state of the program is identical. A typical example would be memory allocation: the same call in the same context could either succeed or fail, depending on the conditions outside the control of the program. In addition to failures, the normal input of the program (files, network, user input on the terminal) are all instances of non-determinism due to external influences. The sum of all such external behaviours that affect the outcome of the program is called the environment (this includes the scheduling of threads done by the operating system and/or CPU). When testing, the environment is controlled to some degree: the inputs are usually fixed, but eg. thread scheduling is (basically) random – it changes with every test execution. Resource exhaustion can be simulated in a test environment to some degree. In a model checker, the environment is controlled much more strictly: when a test case is run through a model checker, it will come out the same every time.

6 The DVE Specification Language

DVE specification language has been created as a language that is both easy to interpret and sufficiently powerful to express interesting problems for the purpose of model checking.

A set of case studies is available, in the form of DVE source code, in the examples subdirectory of the DIVINE distribution.

6.1 Philosophy of DVE language

The basic modelling unit in DVE is a system that is composed of processes. Processes can go from one process state to another through transitions, which can be guarded by a condition – this condition, also called a “guard”, determines whether the transition can be activated.

Transitions can be synchronised through (named) channels. Only exactly 2 processes can be synchronised in one “moment” (in a single step). When more than 2 processes would be able to synchronise at the same time on a single channel, any combination of pairs can be picked at that time nondeterministically, however always just 2 of them in one moment. Through the synchronisation on a channel, a value can be optionally transmitted from one process to the other.

The transitions have so-called “effects”. Effects are generally assignments to local or global variables. Two processes undergoing a synchronisation should not be able to assign to the same variable – that would be a modelling error.

A system may be synchronous or asynchronous.

6.2 Uniqueness of identifiers

There is a single common namespace for channels, variables, processes and states. Identifiers have to be unique in any given scope of visibility. It means that e.g. when variable A is declared in the process P1, then there cannot be another variable A, a state A in that process or a global variable A, nor a channel or a process A The only other variable A may occur in a different process, e.g. P2.

6.3 Syntax elements

6.3.1 Processes

Declaration – short example:

    process My_really_nice_process
    { <code of a process> }

6.3.2 Variables

Variables can be global (declared at the beginning of DVE source) or local (declared at the beginning of a process). These can be of either byte or int type. E.g.:

    byte A[9];
    int i,j;

6.3.3 Constants

Constants can be declared identically to variables using the keyword const:

    const byte k = 3;

As of yet, the constants cannot be used as parameters in declarations of arrays. For example, this construct is erroneous:

    byte field[k];

6.3.4 Process states

Declared after the declaration of variables. You also have to write which of the declared process states is the initial one. You can also optionally specify some of them as accepting (but you probably do not need this feature at this moment). E.g.:

    state start, run, reading_input, writing_output;
    init start;
    accept reading_input, writing_output;

For purposes of modelling atomic actions, there are so called committed states.

Committed state of a process = state declared as committed – e.g. in the following code states reading_input and writing_output are committed:

    state start, run, reading_input, writing_output;
    init start;
    commit reading_input, writing_output;

Committed state of a system = state of a system, where at least one process is in a committed state. If the system is in a committed state, then only processes in committed states can transit to another state. It means that the sequence of transitions beginning with a transition leading to a committed state and ending with a transition leading to a non-committed state cannot be interlaced with other transitions leading from non-committed states.

Synchronisation between processes in committed states and non-committed states is ignored. Synchronisation between processes (both) in committed states is permitted (but it is probably very rare).

6.3.5 Transitions

Transitions are written as arrows going from one process state to another (e.g. run -> writing_output). The transition can be executed only if the process is in the source process state of a transition (in the above mentioned example in the state run). You should also define an additional condition when the transition can be executed (using the keyword guard) and sometimes also a channel to synchronise through (using the keyword sync followed by the channel name and ! or ?). Only transitions with the same channel name and opposite operators ! and ? can synchronise. When you want to transmit a value through the channel, you can write the value after ! and a variable that will receive the transmitted value after ?. The last but not least element of transitions are effects – they are simple assignments to the variables.

Example:

    process Sender {
      byte value, sab, retry;
      state ready, sending, wait_ack, failed;
      init ready;
      trans
        ready -> sending {sync send?value; effect sab = 1 -sab; },
        sending -> wait_ack {sync toK!(value*2+sab); effect retry = 1;},
        wait_ack -> wait_ack { guard retry <2;
                               sync toK!(value*2+sab);
                               effect retry = retry+1; },
        wait_ack -> ready {sync fromL?;},
        wait_ack -> failed { guard retry == 2;};
    }

6.3.6 Expressions

In assignments, guards and synchronisation values you can write arithmetic expressions. They may contain:

6.3.7 Channels

Declarations of channels follow declarations of global variables. For example:

    byte i_am_a_variable;
    // untyped unbuffered channels
    channel send, receive, toK, fromK, toL, fromL;

    // typed unbuffered channels
    channel {byte} b_send[0], b_receive[0];

    // typed unbuffered channels (transmitting 2 values simultaneously)
    channel {byte,int} bi_send[0], bi_receive[0];

    // typed buffered channels
    channel {byte,int} buf_bi_send[4], buf_bi_receive[1];

There is a big difference between buffered and unbuffered channels:

Be aware: channel xxx and channel {byte} xxx[0] are both unbuffered channels and they behave almost the same way, but the second declaration is typed and the transmitted value is type casted (in this case to byte) before its transmission.

6.3.8 Type of a system

Synchronous:

    system sync;

or asynchronous

    system async;

This declaration should be written at the end of a DVE source.

6.3.9 Assertions

Assertions can be written in every process just before transitions definitions. Assertion can be understood as an expression, which should be valid (evaluated to non-zero value) in a given process state. Example:

    process My_really_nice_process
    {
        byte hello = 1;
        state one, two, three;
        init one;
        assert one: hello >= 1,
               two: hello <  1,
               one: hello <  6;
        trans
            ...
        ;
    }

7 DVE Modelling Tutorial

This tutorial will guide you through the creation of a model of the Peterson’s mutual exclusion algorithm for n processes. This will help you understand the following concepts:

7.1 The Peterson’s algorithm

First, let us show you the algorithm itself as a C code snippet:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
volatile int q[n] = { 0 };
volatile int turn[n] = { 0 };

void enter_critical_section(int i) {
    int j, k;

    for (j = 1; j < n; j++) {
        q[i] = j;
        turn[j] = i;

        for (k = 0; k < n; k++)
            while (k != i && (q[k] >= j && turn[j] == i));
    }

    q[i] = n;
}

void leave_critical_section(int i) {
    q[i] = 0;
}

void process(int process_id) {
    for (;;) {
        enter_critical_section(process_id);
        /* do work */
        leave_critical_section(process_id);
    }
}

We will create a model of the process procedure and, using the m4 macro language, make the model parametric.

7.2 Model, Processes, Transitions

A model in DVE consists of several processes, each of which is an extended finite state automaton. These are (usually) asynchronously composed to become an automaton of the model. The last line of an asynchronous model in DVE reads:

    system async;

Let’s just put this line at the end of each model, for now. Synchronous models aren’t well supported yet.

A process declaration looks like this (the order of things is important):

    process P1 {
        variables
        states
        assertions
        transitions
    }

As an example, we declare a process which alternates between two states: inside a critical section, and outside it.

    process P1 {
        state outCS, inCS;
        init outCS;
        trans
            outCS -> inCS {},
            inCS -> outCS {};
    }

The process starts in state outCS and there’s one transition from outCS to inCS and one from inCS to outCS, neither of them having any guards or effects. Indeed, performing a reachability analysis using DIVINE tells us that two states are reachable.

If we omit one of the transitions, we create a deadlock state – the automaton is stuck in it, not able to proceed. DIVINE is able to detect and describe such states.

Next, we’d like to have multiple similar processes, all described by one automaton but each having a different name and, possibly, some process number constant. In order to do this, we use the m4 macro language like this:

    define(P, `process P_$1 {
        state outCS, inCS;
        init outCS;
        trans
            outCS -> inCS {},
            inCS -> outCS {};
    } ')

    P(0)
    P(1)
    P(2)

If we process this definition with the m4 command, we get a model with three processes. Reachability analysis would tell us that we have 8 states, by the way.

To make the model parametric, we shall use some predefined m4 macros. Filename of the source of such model should end with the .mdve extension; usage of such files is described in the [Tool guide][toolguide]. Finally, we get this parametric source:

    default(N,3)

    define(P, `process P_$1 {
        state outCS, inCS;
        init outCS;
        trans
            outCS -> inCS {},
            inCS -> outCS {};
    } ')

    forloop(i,0,N - 1, `P(i)')

    system async;

7.3 Variables, Guards, Effects

In DVE, you may define global and process-local variables. There are two types: byte and int, and you may define one-dimensional arrays using the C syntax. These variables can be modified using transition effects and transitions are enabled/disabled based on variable values using guards.

The variable declarations are similar to the C syntax, you’ll easily understand that from the following examples. We’ve already shown where process-local variable declarations go. Global variables are declared at the beginning of a DVE source.

Guards and effects go into the curly braces after a transition, like this:

    trans
        q0 -> q1 { guard (x == 1) && (y == 2);
                   effect x = x + 1, y = y - 1; };

For a quick overview, let’s say the two functions are a bit simpler (and wrong indeed):

    volatile int mutex = 0;

    void enter_critical_section(int i) {
        while (lock == 1) /* wait */;
        lock = 1;
    }

    void leave_critical_section(int i) {
        lock = 0;
    }

We shall declare a global variable mutex in the model as well (a byte type is enough, though).

    byte lock = 0;

The leave_critical_section function is simple, it just resets the lock variable when leaving the critical section. We’ll model this as an effect on the inCS -> outCS edge:

    trans
        ...
        inCS -> outCS { effect lock = 0; };

To model the enter_critical_section function, we’ll have to add a couple of states: a “waiting for lock becoming 0” state and a “lock has just become 0” state. We’ll model the while loop as a cycle around the waiting state, and the assignment as a transition from the other state to inCS. It is very important to distinguish these two states since two processes may both reach the “lock = 1” line at the same time; if we modelled the assignment as a transition from the waiting state, the model would not allow such behaviour.

The whole model of this faulty lock looks like this:

    default(N,3)

    byte lock = 0;

    define(P, `process P_$1 {
        state outCS, inCS, waiting, lockit;
        init outCS;
        trans
            outCS -> waiting {},
            waiting -> waiting { guard lock == 1; },
            waiting -> lockit { guard lock == 0; },
            lockit -> inCS { effect lock = 1; },
            inCS -> outCS { effect lock = 0; };
    } ')

    forloop(i,0,N - 1, `P(i)')

    system async;

Now, you may want DIVINE to tell you if it is possible to get to a state where two processes are both in a critical section. An LTL property claiming that it is not is this:

    #define c0 (P_0.inCS)
    #define c1 (P_1.inCS)
    #property !F (c0 && c1)

If we find a counterexample to this property then it is possible to reach such state and the lock is faulty. DIVINE finds such counterexample indeed. For information about using divine combine and divine verify to perform the check, please see the [Tool guide][toolguide].

7.4 Arrays, back to Peterson

We’ve shown how to create a DVE model of a simple lock in C. Let’s go back to our example model of Peterson’s algorithm now. You already know the needed syntax; let me repeat the way we transform a C source into a DVE model:

Now we will carefully rewrite the C source to DVE. Let’s start by defining the global variables:

    byte q[N];
    byte turn[N];

These arrays contain zeros in the initial state, you may count on that. To start with simple things, we shall model the leave_critical_section function:

    define(P, `process P_$1 {
        state outCS, inCS;
        init outCS;
        trans
            inCS -> outCS { effect q[$1] = 0; };
    } ')

Next, we’ll create an outline of the enter_critical_section. We will need to add some local variables as well.

    byte j, k;
    ...
    trans
        outCS -> for_j { effect j = 1; },
        for_j -> inCS { guard j == N; effect q[$1] = N; },
        ...

We have just modelled the initialisation of the outer for loop, the end of it and the locking itself (q[i] = n means that process i is in the critical section). Let’s go to the inside of the loop:

    trans
        ...
        for_j -> j1 { guard j < N; effect q[$1] = j; },
        j1 -> for_k { effect turn[j] = $1, k = 0; },
        /* for_k ... */
        for_k -> for_j { guard k == N; effect j = j + 1; };

We combined two memory writes into one transition: turn[j] = $1 and k = 0 even though we said we should not. It’s ok here because the k variable is not shared. Okay, let’s finish it by defining the for_k transitions as well:

    trans
        ...
        for_k -> while { guard k < N; },
        while -> while { guard k != $1 && q[k] >= j && turn[j] == $1; },
        while -> for_k { guard k == $1 || q[k] <  j || turn[j] != $1;
                         effect k = k + 1; };

Note that there are two transitions going from a loop state, the guards of which are negations of each other (in a for loop with +1 increments, we usually have j < N and j == N, since that works too).

Okay, we have completed the model. Let me repeat the whole thing for you:

    default(N,3)

    byte q[N];
    byte turn[N];

    define(P, `process P_$1 {
        byte j, k;
        state outCS, inCS, for_j, j1, for_k, while;
        init outCS;

        trans
            /* enter_critical_section */
            outCS -> for_j { effect j = 1; },
            for_j -> j1 { guard j < N; effect q[$1] = j; },
            j1 -> for_k { effect turn[j] = $1, k = 0; },
            for_k -> while { guard k < N; },
            while -> while { guard k != $1 && q[k] >= j && turn[j] == $1; },
            while -> for_k { guard k == $1 || q[k] <  j || turn[j] != $1;
                             effect k = k + 1; },
            for_k -> for_j { guard k == N; effect j = j + 1; },
            for_j -> inCS { guard j == N; effect q[$1] = N; },
            /* leave_critical_section: */
            inCS -> outCS { effect q[$1] = 0; };
    } ')

    forloop(i,0,N - 1, `P(i)')

    system async;

This model satisfies the aforementioned property indeed. That means a state where two processes are both in a critical section is not reachable. See section Using LTL Properties to see how to combine the model with the property.

8 Untimed LTL Model Checking of Timed Automata

Uppaal Timed Automata has become the standard modelling language for real-time systems. For such systems, DIVINE can verify the presence of time deadlock or validity of an LTL specification. DIVINE has support for most of this modelling formalism, though, some features are still left unimplemented. These are as follows:

On the other hand, DIVINE offers an important feature that is not available in Uppaal — the generation of error states. If an error occurs during the verification, DIVINE generates an error state corresponding to the type of the error and continues with the verification. These error states are found automatically during the reachability analysis and full trace from the initial state is generated to one of them if required.

To run DIVINE on a Uppaal model, DIVINE should be applied directly onto a Uppaal XML file with the model.

$ divine verify model.xml

DIVINE runs the reachability analysis to find an error state or a time deadlock. By default, the LU extrapolation is in use, so the time-lock detection is disabled (see Havlicek, 2013: Untimed LTL Model Checking of Timed Automata, Chapter 2). However, the --no-reduce option can be used to force the maximal bounds extrapolation, thus allowing the time-lock detection.

To check for validity of LTL properties, a file with a suffix .ltl and the same base name as the model file has to be created. This file can contain one or more LTL properties constructed using LTL specification language (see LTL specification format above). Due to limitations of the tool that DIVINE uses to transform LTL formulae to corresponding Büchi automata, atomic propositions can contain only lower case letters, digits, underscore and must not begin with a digit. For this reason, C-like defines can be used before property declarations to name any boolean expression in the Uppaal modelling language with a suitable name. The only additional limitation is that all clock constrains have to be defined as separate atomic propositions. All lines in the LTL file that do not begin with #define or #property are ignored and can be used for comments. An example of a valid LTL file is given below, other ones are shipped with DIVINE.

#define time1 (time <= 60)
#define time2 (time < 70)
#define safe1 (V1.safe)
#define safeall (V1.safe && V2.safe && V3.safe && V4.safe)
#property !F(time1 && safeall)
#property !((!safe1) U (time2 && safeall))

Verification of the first property in the corresponding LTL file is run using the following command:

$ divine verify -p 0 model.xml

To exclude all Zeno runs during the LTL verification, we can use the option -f, similarly to obtain a full report of the verification including an error trace, we can use -r.

The LTL specification language differs from subset of CTL used by Uppaal, but all properties that may be used in Uppaal may be verified by DIVINE as well. In CTL you may qualify your formula as existential (E…) or universal (A…). DIVINE does universal verification only, i.e. it decides whether all runs meets given conditions. However, negation of existential formula is a universal formula. Therefore, if your desired CTL specification is in the form A[]p or A<>p, you can directly translate it to equivalent LTL formula Gp or Fp respectively. E<>p can be translated to G!p and E[]p to F!p, but these formulas are not equivalent, in fact, they have exactly opposite meaning; hence when DIVINE says a formula F!p does not hold in some model, Uppaal says that E[]p is satisfied and vice versa. In the case of existential CTL formula that holds, DIVINE reports a counterexample to corresponding LTL formula, which is actually a witness for the original CTL formula. The last class of formulas Uppaal is able to verify are response or leads-to properties; p-->q is equivalent to LTL formula G(p -> Fq).

DIVINE considers only runs where action and delay transitions alternate. This means that DIVINE does not consider runs where the system stays in one location for an infinite amount of time. The temporal operator X considers the next state to be a state that can be reached by performing exactly one action transition followed by an arbitrary delay transition. For the purpose of LTL verification, all runs ending in a deadlock are transformed to infinite ones by adding an artificial loop over the final state. This ensures that the LTL verification is meaningful even on systems, where not all runs are infinite. Without this transformation, the property F(false) would hold on a timed automaton with one state and no transitions, because it does not have any infinite runs, which means it cannot have any infinite runs violating this property. If the LU reduction is not applied, time-locks are also considered for this transformation.

9 Common Explicit-State Model Interface

DIVINE provides an implementation for CESMI, which defines a simple common interface between a model-checking core and a module that generates the state space of the model in a demand-driven fashion.

CESMI does not specifically demand any concrete implementation of the interface. DIVINE provides a C-runtime-compatible ABI conforming to the CESMI specification, as well as C (and C++) and Haskell APIs, which can then be translated to conform to the provided ABI using standard tools. Loading a compiled CESMI module is facilitated by using dynamic (shared) libraries on the target platform: ELF Shared Object files are supported on POSIX platforms, and Dynamically Linked Libraries (DLLs) on Win32 (Win64) platforms.

DIVINE currently provides two compilers to translate models in specific modelling formalisms to CESMI modules: a compiler for the DVE language (which is also supported directly through an interpreter) and a compiler for the MurPHI language, adapted from the original MurPHI model compiler.

9.1 The CESMI Specification

CESMI is a set of APIs (Application Programming Interface) to represent model checking problems in a form independent of a specific model-checker. The API is explicit-state (states of the model are represented discretely) and allows for implicit (on the fly) representation of models – local neighbourhood of a given vertex needs to be provided. The exact semantics of vertices and edges represented by a CESMI model depend on the model checking algorithm in question. Multiple interpretations of a given graph are possible, and will be discussed in detail in the section on semantics.

CESMI defines a notion of a “module” and a “loader”, the role of the module corresponding to the model, or a Kripke structure, to be examined. The “loader” is then a part of a model checking or other model examination tool, which treats the CESMI module as its input data.

9.1.1 The Module

We will lay out the basic requirements for a CESMI module in this section. The C prototypes of the individual calls exposed in the API of the module are as follows:


    void setup             ( cesmi_setup * );
     int get_initial       ( const cesmi_setup *, int,
                             cesmi_node * );
     int get_successor     ( const cesmi_setup *, int,
                             cesmi_node, cesmi_node * );
uint64_t get_flags         ( const cesmi_setup *, cesmi_node );
   char *show_node         ( const cesmi_setup *, cesmi_node );
   char *show_transition   ( const cesmi_setup *, cesmi_node,
                             int );

Only get_initial and get_successor are mandatory, the rest of the functionality is optional, and the loader must substitute suitable defaults.

The setup call may set up per-instance state, however, if it does, it must keep it all through the instance pointer of the cesmi_setup structure, which has the following C definition:


typedef struct {
    void *loader;
    cesmi_node (*make_node)( const cesmi_setup *, int );
    cesmi_node (*clone_node)( const cesmi_setup *, cesmi_node );
    int (*add_property)( cesmi_setup *, char *, char *, int );
    void *instance; // per-instance data; never touched by DIVINE
    int property_count; /* filled in by setup */
    int property; /* filled in by loader */
    int instance_initialised;
    void (*add_flag)( struct cesmi_setup *setup, char *name, int id, int type );
    /* extensions at the end are ABI-compatible */
} cesmi_setup;

For each instance of the CESMI module created by the loader, there is a unique cesmi_setup value which is passed to all calls into the module. At the time of the setup call, the cesmi_setup structure must be initialised by the loader to its default state. The setup implementation of the module may change the field instance, the remainder is for reading only. The setup implementation may also modify the cesmi_setup structure via calls to add_property and add_flag.

Since the model checker might use the CESMI module in multiple threads, the CESMI module must not retain any global state. All instance-specific state must be managed through the instance pointer provided in the cesmi_setup structure. The CESMI loader may call setup multiple times with a different parameter (in the same address space), and the resulting CESMI module instances must be fully isolated.

9.1.2 Handling State

The functions get_initial and get_successor (and by extension, show_transition, see below) need to maintain state between invocations to be able to work with reasonable efficiency. The handle system allows a limited amount of state to be passed around safely (namely a single integer). To obtain all successors of a vertex, the CESMI loader first calls get_successor with handle value 1. The implementation of get_successor then returns the first successor and a handle value to obtain the next successor. When there are no further successors to return, it should give a 0 handle. When a vertex has no successors, the response to get_successor( setup, state, 1, result ) should be 0, and result should be left untouched. The same principle applies to get_initial. An example implementation of get_successor might look like this:


int get_successor( const cesmi_setup *setup, int handle,
                   cesmi_node from, cesmi_node *to )
{
    struct state *in = (struct state *) from.memory;

    if (in->a < 4 && in->b < 4 && handle < 3) {
        *to = setup->make_node( setup, sizeof( struct state ) );
        struct state *out = (struct state *) to->memory;
        *out = *in;
        switch (handle) {
        case 1: out->a ++; return 2;
        case 2: out->b ++; return 3;
        }
    }
    return 0;
}

9.1.3 Memory Management

The module is responsible for allocating memory for new states, and it must use the make_node or clone_node functions provided in the cesmi_setup structure it is given, passing the setup as their first parameter, and either the size of the bit vector it requires (make_node) or a state to be cloned (clone_node). The loader might need to store additional data with the state, hence it returns a structure with two pointers in it.


typedef struct {
    void *handle;
    char *memory;
} cesmi_node;

The memory field of the returned structure is for use by the CESMI module to store state information. The module must not alter the handle – it must be retained in the result of the respective get_initial or get_successor call. The memory pointer must not be passed to free. The module should only call make_node/clone_node at a point where it is known that a state will be generated, along with its size, otherwise it will cause undesirable memory leaks.

9.1.4 Human-readable Labels

To aid in reading counterexamples or when exploring the state space, it is often very useful to have human-readable labels assigned to system states and/or transitions. To this end, CESMI specifies (optional) functions show_node and show_transition. Both should return a heap-allocated (with malloc) string. The case of show_node is straightforward, it only gets the state itself. For show_transition, the origin state of the transition is given, plus a handle. The handle is treated the same way as in get_successor: show_transition must give the description of the first enabled transition in the given origin state, or, if no such transition exists, return a NULL pointer.

9.2 Building CESMI Modules with DIVINE

The CESMI module more or less represents a generic oriented graph. It is intentionally kept as simple as reasonably possible: apart from the graph itself and human-readable descriptions of edges and vertices, the only further information exposed in the interface about the graph is a set of per-state flags, which are used to encode the vertex properties interesting for model checking: whether the state is a goal state, or whether it is an accepting state of a Büchi automaton. This means that for the purpose of LTL model checking, the CESMI module must expose a product automaton of the negative claim Büchi translation of the LTL formula and of the system.

While this makes the specification and the loader much simpler, it also adds substantial amount of work for the module authors. What more, this task is repetitive, since large part of the work is the same from model to model: constructing the Büchi automaton from an LTL formula and synchronising its guards with the system, based on values of atomic propositions of the formula.

To this end, DIVINE provides a small framework to help you build CESMI modules suitable for LTL model checking out of a system description and a set of LTL formulas, exposed via the divine compile --cesmi sub-command.

When using divine compile --cesmi, you should always #include "cesmi.h" – this will allow the C/C++ compiler to check your function prototypes against those mandated by the CESMI specification. It will also give you access to the struct types cesmi_setup and cesmi_node and the cesmi_flags / cesmi_property_type enums.

To add LTL formula(s) to your CESMI module, you should additionally #include "cesmi-ltl.h" which provides a number of helper functions to make your job easier. To get access to cesmi-ltl.h, you must provide a file with LTL formulas on the commandline, say divine compile --cesmi mymodule.c mymodule.ltl. In this case, divine will generate code for traversing the Büchi automaton from each LTL formula and links it to your module. To use this generated code, you should use the following APIs:


uint64_t buchi_flags( cesmi_setup *setup, cesmi_node n );

int buchi_get_initial( const cesmi_setup *setup,
                       int handle, cesmi_node *to,
                       get_initial_t next );
int buchi_get_successor( const cesmi_setup *setup, int handle,
                         cesmi_node from,
                         cesmi_node *to, get_successor_t next );
char *buchi_show_node( const cesmi_setup *setup, cesmi_node from,
                       show_node_t next );
char *buchi_show_transition( const cesmi_setup *setup,
                             cesmi_node from,
                             int handle, show_transition_t next );

void buchi_setup( cesmi_setup *setup );

Each of the buchi_ functions corresponds to one of the CESMI functions: buchi_get_initial to get_initial, etc. When implementing your CESMI module, you should implement a CESMI-compatible function under a different name, say _get_initial and implement the CESMI get_initial like this:


int get_initial( const cesmi_setup *s, int h, cesmi_node *n ) {
    return buchi_get_initial( s, h, n, _get_initial );
}

The buchi_setup is different as it is supposed to be called at the end of the setup function like this:


void setup( cesmi_setup *s ) {
    s->add_property( s, NULL, NULL, cesmi_pt_goal );
    s->add_property( s, NULL, NULL, cesmi_pt_deadlock );
    buchi_setup( s );
}

For a full example, please refer to examples/cesmi/withltl.c shipped in DIVINE source tarballs. Compile and test it like this:

$ divine compile --cesmi examples/cesmi/withltl.c \
                         examples/cesmi/withltl.ltl
$ divine metrics withltl.so --property=p_3

10 DIVINE Explicit State Space Format

The DIVINE Explicit State Space (DESS) format is a format for explicit graph representation which can be generated using the gen-explicit command. It can also be used as an input formalism for DIVINE or as a standardised way to represent models, largely independent of DIVINE.

The DESS file contains a fixed-length header followed by an encoding of the graph, which consists of the following sections (at least one of edges section must be present): forward edges, backward edges, node memory. The edge sections are model-independent, the node memory section depends on the model and DIVINE version.

10.1 Graph encoding

In the DESS format, the graph is encoded as a transition relation on set of sequentially numbered vertices. Since vertices are numbered sequentially is is sufficient to only give their count to describe the set. The transitions (edges) are directed, encoded as a one-to-many mapping of outgoing transitions for each vertex.

The first vertex of the graph has index 1.

10.1.1 Initial states of model

To uniquely represent the initial states of models, independently of their count, an additional virtual vertex with index 0 is included. This vertex has an outgoing edge for each initial vertex of the state space.

10.1.2 Transposed graph

The DESS format may also contain the transposition of the graph, which is then encoded the same way as the original graph and edges the in the transposed graph correspond to the backward edges of the original graph. Notably all initial states of the original graph have an edge to the virtual vertex 0.

10.2 Header format

The header has length of 128B and the following format:

+--------------------------------+--------------------------------+
| DESS identification string (40B)                                |
|                                                                 |
|                                                                 |
|                                                                 |
|                                                                 |
+--------------------------------+--------------------------------+
| byte order check (8B)                                           |
+--------------------------------+--------------------------------+
| DESS version (4B)              | label size (4B)                |
+--------------------------------+--------------------------------+
| supported features (8B)                                         |
+--------------------------------+--------------------------------+
| generator identifier string (24B)                               |
|                                                                 |
|                                                                 |
+--------------------------------+--------------------------------+
| node count (8B)                                                 |
+--------------------------------+--------------------------------+
| data start offset (8B)                                          |
+--------------------------------+--------------------------------+
| forward edges offset (8B)                                       |
+--------------------------------+--------------------------------+
| backward edges offset (8B)                                      |
+--------------------------------+--------------------------------+
| nodes offset (8B)                                               |
+--------------------------------+--------------------------------+

All non-string values are stored as signed integers of a given length, the only exception is the byte order check which is an unsigned integer.

DESS identification string
String allowing to identify the DESS file. It reads “DIVINE COMPACT EXPLICIT STATE SPACE.”
byte order check
This field is used to verify the endianity of the DESS file, it should contain the value 0x0807060504030201.
DESS version
Currently set to 1. In future, it will be changed if a revision of the header format becomes necessary.
label size
Size of edge labels saved with edges, in bytes. Those labels are model specific.
supported features

Bitwise or of flags of supported features, as of DIVINE 3.1, following features can be set (together with their value):

ForwardEdges = 0x1
file contains encoding of forward edges
BackwardEdges = 0x2
file contains encoding of bacward edges
Nodes = 0x4
file constains memory of states
UInt64Labels = 0x100
labels are encoded in unsigned 64 bit integers
Probability = 0x200
labels are probabilities
generator identifier string
String uniquely identifying generator used to create DESS file.
node count
Number of nodes (vertices) of graph. The graph nodes are numbered from 1 to node count with additional virtual vertex 0 used to mart initial vertices.
data start offset
Offset from beginning of file to the beginning of data, in bytes (it equals size of header for files generated by DIVINE 3.1).
forward edges offset
Offset of forward edges data block from data start offset, in bytes.
backward edges offset
Offset of backward edges data block from data start offset, in bytes.
nodes offset
Offset of nodes data block from data start offset, in bytes.

10.3 Data block format

Data block is encoding of array of variable sized data. It consists of two sections: indices and data.

Indices section is fixed size, containing exactly node count 64bit indices to data section. Data section starts at offset 8 * node count bytes. Value on ith position in index section is offset of end of ith data field, measured in bytes from beginning of data section. Therefore ith value begins on offset specified by (i–1)th index or at the beginning of data section for i=0.

The exact meaning of data in data block depends on encoded values, which are either edges or nodes.

10.3.1 Edge data format

In the case of edge data, the value corresponding to ith index encodes edges outgoing from ith vertex, each value being tuple of 64bit vertex index and optional label (of size label size).

10.3.2 Node data format

In the case of node data, the value corresponding to ith index is implementation defined encoding of vertex with index i. There are currently no guarantees on compatibility of node data across different versions of DIVINE.

11 A Hacker’s Guide

This chapter is intended for DIVINE developers, writing algorithms, backends or working on various framework components. Before starting with DIVINE, it is advisable that you first try to compile the tool (see README) and find out how the divine binary and other components work.

The development work is co-ordinated through the divine at fi.muni.cz mailing list, and through a trac instance which has (most importantly) our issue tracker and also a source code browser. We also run a continuous integration server, based on Hydra.

11.1 Using Darcs

The source tree of divine is kept in the darcs revision control system.

You need a darcs 2.x binary (see http://www.darcs.net) to check out the source and to record patches. After installing darcs, there is a single “main” branch, which you should use as a base for your work. Get a copy by issuing:

$ darcs get http://divine.fi.muni.cz/darcs/mainline divine

Now, you should have a directory called divine, which contains a copy of the source code. You can modify a few files in there, and issue

$ darcs whatsnew
$ darcs record

You will notice that, unlike CVS, darcs will ask you which changes to record (or commit, in the CVS vocabulary). Also, darcs will ask you for a short patch name. You are encouraged to only record small changes at once, so that you can describe the change in a single line. Of course, for bigger changes (or those that need more explanation), you can still include a longer description after the short one (darcs will ask). The description should be an English sentence, starting with a capital letter and ending with a period. It should preferably be no longer than 80 characters. We commonly prefix the short description with a single word describing the component it affects.

Now, after you provide this data, darcs will run the testsuite, to ensure you didn’t break anything. However, this is most often something you do not want to happen, and should disable in your personal repo (you can always run the suite with make check). Prevent darcs from running the tests with:

$ echo "ALL no-test" > _darcs/prefs/default

Another important command is:

$ darcs changes -s -i

This will let you browse the recent changes, with summary of changed files in each. You can hit v in the interactive prompt to inspect the change in detail. Use spacebar to advance to the next older patch.

When you record a change you don’t like, you can use darcs unrecord to remove the recorded patch. Note however, that the changes will be kept in the working copy, so you can darcs record them again, or darcs revert them, if you are sure you want to remove them forever.

If you have changes that you would like to have included within the main divine branch, it is probably best to send those changes by mail. They will be reviewed and added to the repository as appropriate.

$ darcs send

Alternatively, you can publish your darcs repository (e.g. using a public http hosting service, or you can try patch-tag or darcsden). Then contact the maintainer and ask them to merge your changes into mainline.

Over time, the mainline will accumulate some changes, and you will probably want to stay in sync with those. It is advisable that before merging from mainline, you record all your unrecorded changes. Then, you may issue:

$ darcs pull

Which will ask you which changes would you like to bring into your branch. Most of the time, you should not see any conflicts, as darcs handles merging automatically (unless there are real conflicts).

If you get spurious conflicts when pulling, it is advisable that you darcs get a new copy of the mainline repository and use darcs pull to move your local changes from your previous copy. This means that some patches have been removed from the mainline, although this happens only very rarely.

You can build divine the same way as you would when using distribution tarballs, although you may need to chmod +x ./configure first. Please see README for further details.

11.2 Source Code Overview

The source code is currently laid out like this:

The following sections talk about various parts of the source code in more detail.

11.2.1 Wibble

DIVINE uses libwibble, a general-purpose utility library for C++ for several things. Most importantly, the threading abstraction is provided by this library and comes with a pthread-based and a win32-based implementation.

11.2.2 The Toolkit

In divine/toolkit, you will find the parts of divine that are most generic. High-performance hash tables, a very simple RPC protocol over MPI, memory allocation, parallel execution and distributed termination detection. This code is not really specific to model checking or graph exploration, but is geared toward high-performance computing.

11.2.3 Graph Traversal

Another set of modules of the divine library implements a graph interface and parallel graph traversal utilities. These live in divine/graph.

11.2.4 Algorithms

The actual model-checking algorithms can be found under divine/algorithm. The common infrastructure is found in common.h, and builds heavily on the parallel primitives from toolkit.

11.2.5 Generators

The state space generators, or system interpreters, are a major part of DIVINE. Each is usually split into two parts, the bulk of the implementation of a given language living under its own subdirectory in divine/, and a comparatively small adaptor – a piece of code that implements a standardised graph-traversal interface on top of the interpreter – found under divine/generator. The adaptor interface is declared in divine/graph.

The currently available generators are:

11.2.6 Instances

The basic components of divine are implemented as C++ templates, for various reasons (performance, static type safety). As such, a “configuration” of divine: the input language interpreter, the model checking algorithm and the state storage subsystem need to be combined at compile time, obtaining a single tight unit with minimal configuration-related branching in the hot code paths. The code in divine/instances takes care of both instructing the compiler to emit code for the sensible combinations of modules, as well as provide the code to translate runtime configuration into the correct entry point of the combined system.

11.2.7 LTL to Büchi translation

In order to perform LTL model checking, DIVINE needs to translate LTL formulas into Büchi automata. There are currently two components which implement this translation, the “traditional” ltl2ba which has been part of DIVINE since forever, found in divine/ltl2ba and a “modern” implementation based on the unrelated external tool called, confusingly, “LTL2BA”. The implementation shipped with DIVINE is however called LTL3BA and is found in external/ltl3ba. There is a compile time option to enable/disable LTL3BA.

11.2.8 Tools

This directory hosts parts of the divine source that comprise the command line interface. These files are not part of the divine library, although certain modules may move to the library over time.

11.2.9 GUI

Finally, the gui directory contains the sources of a graphical user interface for the DIVINE tool, based on Qt 4.x. Comes with a DVE simulator and counterexample browser.

11.3 Debugging

When debugging DIVINE with gdb, no special precautions are usually needed. You however probably want a build with debugging enabled and optimisations disabled: pass -DCMAKE_BUILD_TYPE=Debug to obtain such a build. This also enables assertion checking, which is definitely useful for debugging.

Moreover, when using valgrind to hunt down leaks and/or memory corruption, it is often desirable do disable custom memory management: pass -DTBBMALLOC=OFF (in addition to the above) at configure time to achieve this.