Local Nontermination Detection for Parallel C++ Programs

Authors: Vladimír Štill, Jiří Barnat

One of the key problems with parallel programs is ensuring that they do not hang or wait indefinitely – i.e. there are no deadlocks, livelocks and the program proceeds towards its goals. In this work, we present a practical approach to detection of nonterminating sections of programs written in C or C++, and its implementation into the model checker. This complements the existing techniques for finding safety violations such as assertion failures and memory errors. Our approach makes it possible to detect partial deadlocks and livelocks, i.e. those situations in which some of the threads are progressing normally while the others are waiting indefinitely. The approach is also applicable to programs that do not terminate (such as daemons with infinite control loops) as it can be configured to check only for termination of selected sections of the program. The termination criteria can be user-provided, however, comes with the set of built-in termination criteria suited for the analysis of programs with mutexes and other common synchronisation primitives.


The source code for the version of DIVINE describe in this paper is available. DIVINE supports Linux, it might also work on various UNIX systems, including macOS. To build DIVINE, you will need a C++11 compatible compiler, and make. The rest can be installed automatically, starting from the directory with DIVINE sources:

After the build, DIVINE will be available as ./_build.release/tools/divine.

For more information on building and installing DIVINE from the tarball please refer to the manual.


Once you have obtained DIVINE binary and a suitable program in C or C++, verification can be started:

The divine check command runs the program analysis, any options passed to it before the program name will be used for configuration of the verification, any options after the program name are forwarded to program’s main function. If the --nontermination local option is omitted, DIVINE will only check for safety, not for nonterminating resource sections.

It is also possible to specify which types of nonterminating resource sections should be considered for the analysis (or start with all of them and disable some):

For further details on usage of DIVINE, please refer to the manual.

User-Defined Resource Sections

To define custom resource sections, you have to include <rst/termsec.h>:

This is a simple example of a spinlock which defines function-based resource section to check that the waiting in lock ends. Please note that the resource section starts with declaration of check and ends at the end of its scope, it this case at the end of lock function. While this solution is simple, it has two downsides: it abuses function-based resource sections to check for waiting, and it does not define resource section for the critical section guarded by the mutex.

A better solution would be:

Here, for the definition of resource section corresponding to the critical section, we cannot use the scope-based API as there is no corresponding scope.

The C API is the same as the non-scoped C++ API:

The available scoped sections are CheckExclusive, CheckWait, and CheckFunction, which correspond to user-exclusive, user-wait, and function-end options to --nontermination. The unscoped versions are termsec_begin_exclusive / termsec_end_exclusive, termsec_begin_wait / termsec_end_wait, and termsec_begin_fuction / termsec_end_function respectively.

For the exclusive and wait cases, the argument is the resource that the resource section works with (for example the atomic flag which implements the spinlock in our case). For the function resource section, the scoped version has no arguments, and for the unscoped the begin takes no arguments, but it returns an identifier of the function which has to be passed to the corresponding end:

Please note that all the code snippets on this page which use atomics use C++11 (or C11 for C examples).


Benchmarks used for evaluation can be found in the test/termination subdirectory of DIVINE tarball, or they can be explored directly.