This document outlines the major areas of development in DIVINE and their goals for the nearest minor and major version. A more detailed plan is kept in our issue tracker's planning view.

There are 3 types of DIVINE releases: major, minor and patchlevel. A patchlevel release is made every two weeks, always on 1st and 15th of any given month. There are 3 minor releases a year (one every 4 months) and those are the primary planning vehicle. A major release is made every few years. Features are merged and released as they become ready (i.e. in patchlevel versions), so a feature planned for e.g. 4.5 will most likely become available at some point in the 4.4 series, say in version 4.4.8.

Core Components

Those include the virtual machine DiVM and the (explicit-state) model checker.

Version 4.4 (September 2019)

Work is currently ongoing on a major rewrite of the model-checking components of DIVINE and we expect this work to be finalized and merged by version 4.4 in early autumn. These changes should enable more efficient exploration of all types of state spaces: those which contain branching due to parallelism but also those where the branching is due to undetermined data in the model checking task. Additionaly, the new approach should substantially reduce memory use.

Version 5 (Long-Term)

In the long term, we would like to explore JIT techniques and better instrumentation / code transformation to substantially speed up DiVM, without compromising any of its robustness.

Abstraction-Based Model Checking

DIVINE currently contains a prototype implementation of a symbolic verification mode, based on program transformations. While the primary motivation is to allow verification of open-ended programs (those with inputs), we would like to also use it to improve verification of closed programs.

People: Henrich Lauko, Adam Matoušek, Petr Ročkai

Version 4.4 (September 2019)

The primary role of pointers in a program is to reference memory. They are, however, sometimes used as keys in data structures such as binary search trees or hash tables. In those cases, the behaviour of the program may depend on the exact numeric value of the pointer. DIVINE currently neglects this fact. Our goal is to implement a suitable abstract domain which would allow DIVINE to analyse behaviours of programs that depend on the numeric values of pointers. [H. Lauko]

In addition to full-blown model checking, we would like to provide a more lightweight tool based on symbolic execution, suitable for test case generation and safety checking of programs with finite execution traces. [A. Matoušek]

Version 5 (Long-Term)

Implement a refinement loop. For instance, the above abstract domain is, in many cases, not needed: some programs do not use numeric pointer comparisons. If we assume that no such comparisons are done, we can verify the program more efficiently, but also need to detect when this assumption is violated and refine it. [H. Lauko]

Motivation

The large number of bugs discovered in almost all software products quite clearly demonstrates that ensuring correctness of software is a very hard problem. Of course, making software more reliable first requires existing bugs to be found and then fixed. Software is routinely tested by the QA departments of software vendors, but even then, bugs often slip into the final product and are later discovered by users.

Part of the problem with software testing is the very large number of scenarios that need to be checked. While it is possible to automate many testing tasks using computers, in many cases, the number of scenarios is too large even for a computer to try.

A different approach is to use reasoning to ensure the behaviour of the program matches expectations. This is the unifying principle behind a number of techniques: static types, contracts, loop invariants, formal correctness proofs and so on. The gist of this high-level approach is that many of the details of how the program exactly works are not important for demonstrating a particular bug, or even proving a particular property of the program. Of course, humans naturally take advantage of this fact in their reasoning.

Automated abstraction and symbolic program representation both apply those principles to automated reasoning procedures. Model checking is one such automated reasoning procedure, and can greatly benefit from abstraction. The goal of this sub-project is, therefore, to design program transformations that remove unnecessary detail from programs before using the model checker.

C/C++ Toolchain

To analyse programs using DIVINE, they first need to be translated into LLVM bitcode, linked to bitcode versions of libraries and to DiOS versions of the basic system-level (platform-specific) libraries, especially libc. The job of the toolchain is making compilation of such programs as easy and transparent for the user as possible. The main component of the toolchain is divcc.

People: Zuzana Baranová, Petr Ročkai

Version 5 (Long-Term)

Current versions of DIVINE and divcc only work with static libraries and static linking, due to limitations in the verification (run-time) environment. In the long run, we would like to lift these limitations and support verification of tasks that involve dynamic linking (including run-time loading of shared objects, i.e. programs which use dlopen).

Motivation

Programs can be automatically analysed at various levels: some tools work directly with the source code, while others load a compiled, executable binary. However, both those approaches have substantial downsides. For complex languages (like C++ or Rust), working with the source code is too difficult. Binary code, on the other hand, is often too hard to analyse because most of the high-level structure of the program has been erased at this point, and is tied to a particular CPU instruction set.

For this reason, many analysis tools opt to instead work with an intermediate representation -- the LLVM IR in the case of DIVINE. However, this means that the software to be analysed must be compiled to this intermediate representation, and this currently needs to be done by hand. The goal of this project is to design and implement an extension to the C and C++ compiler toolchain based on LLVM and CLang, which would store the bitcode along standard machine code in the standard UNIX binary format known as ELF. The extended compiler, linker and related tools should transparently work with existing build systems. The hybrid binaries produced this way should be directly executable, but it should also be possible to load them into the DIVINE model checker (and possibly other LLVM-based tools) for analysis.

Runtime Verification

The runtime verification aspects of DIVINE do not have active developers at the moment. Below are the long-term goals that we would like to pick up if/when our staffing situation improves.

Motivation

When executing (as opposed to model checking) programs, DIVINE can currently record system call traces. During model checking, then, it can load these traces and play them back to the program. However, currently only executions that exactly correspond to the system call trace can be explored by the model checker.

The overall goal of this project is to make the model checker more flexible with respect to the recorded trace. The first possible improvement is that certain system calls commute, that is, the observed effects of two such system calls do not depend on their order. The linear order of the trace can therefore be changed to a partial order, increasing the number of executions available for exploration. A different approach is increasing coverage by introducing non-deterministic mutations into the traces -- an approach similar to fuzzing: an established and successful technique. Finally, it is also possible to use symbolic representation of system call parameters which appear in key locations of the trace, improving the coverage further.

Relaxed Memory

DIVINE currently supports verification of parallel programs under the x86-TSO relaxed memory model, via a combination of runtime support and program transformation.

People: Vladimír Štill

Version 4.3

In the upcoming version of DIVINE we would like to focus on speed improvement of analysis of relaxed behaviour of programs running under memory model of the x86 CPUs.

Motivation

When checking correctness of parallel programs, it is important to consider the behaviour of contemporary hardware. Naturally, one would expect that reads and writes performed by the program are executed in the order in which they are specified in the source code and that they are immediately visible to all CPU cores. However, with modern processors, it can happen, for example, that a value written to memory by one core is not observed by other cores immediately. Indeed, reads can appear to be executed before writes which occur earlier in the program. The specific behaviour of processor and memory is described by a memory model, which specifies how reads and writes performed by one core can be observed by the remaining cores. Different types of processors exhibit different behaviours.

Unfortunately, such effects are often neglected by software analysis tools. For this reason, such tools can miss a large number of errors. To make matters worse, programmers can also easily miss these errors, as the real behaviour of hardware is quite unnatural.

In DIVINE, we support verification of parallel programs which takes these effects into account. However, such analysis adds further complexity to the already hard problem of analysis of parallel programs. Currently we are focusing on the memory model of Intel x86 processors (x86-TSO), which is both relatively simple (and therefore can be analysed more efficiently) and widely used. To this end, we have devised a way to analyse execution of program under x86-TSO with can significantly decrease the number of possible operation reorderings which need to be analysed, while still preserving the ability to find all errors caused by reordering allowed under x86-TSO (up to some bound on the distance of reordered operations). More details about our approach to analysis of x86-TSO can be found in the paper Model Checking of C++ Programs Under the x86-TSO Memory Model.