The roadmap was last updated in November 2017.

Short-Term Goals: Q4 2017

This section documents specific short-term development goals, approximately a quarter into the future.

Medium-Term Goals: 2018

This section outlines the research and development plan of DIVINE for approximately a year ahead. Those goals approximately align with the long-term goals outlined in the next section (please read the long-term goals first if you are not yet familiar with them).

Additionally, we have a few medium-term goals that do not neatly fit any of the long-term categories, because they either span the entire project or in which multiple sub-projects interact:

Symbolic 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:

The other two goals are generally useful with all abstractions:

Toolchain

Together, those two goals should allow building of most small and medium-sized software packages written in C. In this stage, the resulting executable binary will use the native C library, while the bitcode will be linked with the DIVINE version of libc and building C++ programs will only work when the system C++ library matches the C++ library used in DIVINE. Lifting both these limitations is a long-term goal.

Runtime Verification

Relaxed Memory

Long-Term Goals

This section describes the various long-term sub-projects that drive the development of DIVINE as a tool. The typical timeline is 2-3 years. Each sub-project has an owner, who is responsible for the project as a whole and coordinates the work on the particular sub-project, as well as its interaction with the rest of the team.

Symbolic Model Checking [H. Lauko]

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.

Runtime Verification [K. Kejstová]

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 [V. Štill]

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.

With DIVINE, we work on support for analysis of parallel programs with takes these effects into account and can therefore discover these hard-to-find bugs. Such an analysis adds further complexity to the already hard problem of analysis of parallel programs. Therefore, we will first focus on techniques to tackle this complexity for the relatively simple memory model (Partial Store Order, PSO), which allows more reordering than the memory model of Intel x86 processors (and can be easily restricted to match it) and under-approximates the ARM memory model. To this end, we have devised a way to analyse execution of program under PSO 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 PSO (up to some bound on the distance of reordered operations).

Based on the results of this initial implementation, we will either first focus on extending DIVINE toward memory models which allow more reordering (such as the ARM memory model and the memory model specified in the C11 and C++11 programming language standards), or first seek further improvements in performance of our analysis. The end goal of the work is to have analysis capable of discovering a wide range of errors exhibited by C/C++ programs running on modern processors, which can be applied to unit tests for parallel data structures and algorithms.

Toolchain [Z. Baranová]

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.