^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
   ———      |     |   |   |     |   |   ||    |  |         |    |
  —(o)—     |     |   |   |     |   |   |  |  |  |————     '————|
 ———————    |     |   |    |   |    |   |    ||  |              |
—————————   —————'   —'—     '     —'—  '     '  '—————         '

Installation

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:

make prerequisites # this will install prerequisites, sudo required
make divine

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.

Usage

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

divine check --nontermination local program.cpp

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

# check only mutex/lock related resouce sections
divine check --nontermination critical,mutex-wait program.cpp

# check only for termination of annotated functions
divine check --nontermination function-end program.cpp

# check for everything but thread joins
divine check --nontermination local,~thread-join program.cpp

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

#include <rst/termsec.h> // for user-defined resource sections
#include <atomic>

struct SpinLock {
    void lock() {
        termsec::CheckFunction check;
        while ( _flag.test_and_set() ) { }
    }

    void unlock() {
        _flag.clear();
    }

  private:
    std::atomic_flag _flag = ATOMIC_FLAG_INIT;
};

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:

#include <rst/termsec.h> // for user-defined resource sections
#include <atomic>

struct SpinLock {
    void lock() {
        { // define an explicit scope
            termsec::CheckWait check( &_flag );
            while ( _flag.test_and_set() ) { }
        } // end of scope
        termsec_begin_exclusive( &_flag );
    }

    void unlock() {
        termsec_end_exclusive( &_flag );
        _flag.clear();
    }

  private:
    std::atomic_flag _flag = ATOMIC_FLAG_INIT;
};

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:

#include <rst/termsec.h> // for user-defined resource sections
#include <stdatomic.h>

void spin_lock( atomic_flag *flag ) {
    termsec_begin_wait( flag );
    while ( atomic_flag_test_and_set( flag ) ) { }
    termsec_end_wait( flag );
    termsec_begin_exclusive( flag );
}

void spin_unlock( atomic_flag *flag ) {
    termsec_end_exclusive( flag );
    atomic_flag_clear( flag );
}

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:

#include <rst/termsec.h> // for user-defined resource sections

void foo() {
    TermsecFunctionId id = termsec_begin_function();
    // do something
    termsec_end_function( id );
}

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

Benchmarks

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