^ —————. —.— . . —.— . . .————— . . ——— | | | | | | || | | | | —(o)— | | | | | | | | | |———— '————| ——————— | | | | | | | || | | ————————— —————' —'— ' —'— ' ' '————— '
HOME MANUAL STATUS PAPERS DOWNLOAD
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, rigorous 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.
The current version of DIVINE strives to keep up with this dynamic world, bringing “heavy-duty” model checking technology much closer to daily programming routine. 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 (C99) and C++ (C++14) programming languages, including their respective standard libraries. Addtional libraries may be rebuilt for use with DIVINE by the user.
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.
To build DIVINE from source, you will need the following:
Additionally, DIVINE can make use of the following optional components:
First, unzip the distribution tarball and enter the newly created directory
$ tar xvzf divine-4.0.tar.gz $ cd divine-4.0
The build is driven by a Makefile, and should be fully automatic. You only need to run:
This will first build a C++14 toolchain and a runtime required to build DIVINE itself, then proceed to compile DIVINE. After a while, you should obtain the main DIVINE binary. You can check that this is indeed the case by running:
$ ./_build.release/tools/divine help
You can now run DIVINE from its build directory, or you can optionally install it by issuing
$ make install
You can also run the test-suite if you like:
$ make check
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.
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 20
(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 cc program.c
After a short 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 program.bc (TODO: divine info is not yet implemented in <span class='divine'>DIVINE</span> 4)
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 (TODO: divine metrics is not yet implemented in <span class='divine'>DIVINE</span> 4)
We have learned that our program has NN unique states and there are NN 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 (TODO: divine metrics is not yet implemented in <span class='divine'>DIVINE</span> 4)
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 loading /lib/libc.bc... linking... done loading /lib/libcxxabi.bc... linking... done loading /lib/libcxx.bc... linking... done loading /lib/libdios.bc... linking... done compiling manual.c annotating bitcode... done computing RR... constants... done found 181 states and 314 edges in 0:00, averaging inf states/s found an error: Dios started! Pthread_join FAULT: __vm_fault called VM Fault Backtrace: 1: main 2: __dios_main choices made: 0 0 0 1 1 0 0 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0 backtraces in the error state: @address: heap* 902b4 0+0 @pc: code* 1d4 4f @location: /divine/src/dios/fault.cpp:34 @symbol: __dios::Fault::handler(_VM_Fault, _VM_Frame*, void (*)()) @address: heap* 901e1 0+0 @pc: code* 234 11 @location: manual.c:18 @symbol: main @address: heap* 901bb 0+0 @pc: code* 1de 26 @location: /divine/src/dios/main.cpp:111 @symbol: __dios_main
Here, as we have anticipated, DIVINE tells us that in fact, the assertion can be violated and gave us an indication of what exactly went wrong. In particular, the backtrace reveals that
manual.c:18 was active during the fault, which is exactly our assertion.
To understand what led to the assertion failure, however, we will need to analyse the counterexample in more detail. For this purpose, DIVINE provides an interactive debugger, available as
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 speed and scalability.
Despite all its shortcomings, lock-based programming (or alternatively, lock-free shared memory programming, which is yet more difficult) is becoming more prevalent. 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 is a catch. 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, out of the box, 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.
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 cc program.c,
divine will compile the runtime support and your program and link them together automatically, using a builtin clang-based compiler. The
cc subcommand accepts a wide array of traditional C compiler flags like
-W and so on.
Alternatively, you can pass a single-file C or C++ program directly to other
divine commands, like
sim, in which case the program will be compiled and linked transparently.
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.
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
longjmp are not yet implemented.
The interpreter simulates an “in order” CPU 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.
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, and so on. DIVINE normally doesn’t store (or 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.
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.