In this work, we present an extension of the DIVINE model checker that allows for analysis of C and C++ programs under the x86-TSO relaxed memory model. We use an approach in which the program to be verified is first transformed, so that it itself encodes the relaxed memory behavior, and after that it is verified by an explicit-state model checker supporting only the standard sequentially consistent memory. The novelty of our approach is in a careful design of an encoding of x86-TSO operations so that the nondeterminism introduced by the relaxed memory simulation is minimized. In particular, we allow for nondeterminism only in connection with memory fences and load operations of those memory addresses that were written to by a preceding store. We evaluate and compare our approach with the state-of-the-art bounded model checker CBMC and stateless model checker Nidhugg. For the comparison we employ SV-COMP concurrency benchmarks that do not exhibit data nondeterminism, and we show that our solution built on top of the explicit-state model checker outperforms both of the other tools. The implementation is publicly available as an open source software.
Installation
The easiest way to try DIVINE is to use the pre-build static binary. This binary should work on any Linux distribution which is not too old (tested on Archlinux, Red Hat Entrerprise Linux 6.9 and 7.5, and Ubuntu 16.04). It should also work on Windows Subsystem for Linux. There is also a source tarball available. For 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:
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 you want to run verification with memory failure simulation enabled, use divine verify instead of divine check. If the --relaxed-memory tso option is omitted, DIVINE will not use relaxed memory semantic (the memory will be sequentially consistent).
The bound on the store buffer size can be configured by an --relaxed-memory tso:N option. If N is 0, the store buffers are unbounded. If it is a positive number, the store buffer bound is set to this number.
For further details on usage of DIVINE, please refer to the manual.
Examples
We include four examples on which demonstrate use of DIVINE.
- Store buffering example
This is the example of x86-TSO from the paper (figure 1).
- Linux spinlock
This is an example from the paper “x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors” by Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. It shows an implementation of Linux kernel spinlock inplemented using atomic intrinsics.
- Peterson’s algorithm in C99 (with TSO bug)
This is an implementation of Peterson’s mutual exclusion algorithm in C99 which demonstrates that this algorithm is not correct under x86-TSO.
- Peterson’s algorithm in C11 with atomics
This is a C11 version of the same mutual exclusion algorithm which uses C11 atomic variables.
Analyzing Store Buffering Example
Let us analyze the store buffering example.
This command should run for some time and then finish with an output similar to the following:
compiling buffering.c
loading bitcode … LART … RR … constants … done
booting … done
states per second: 47.4629
state count: 275
mips: 0.73
relaxed memory: tso
error found: yes
error trace: |
(0) Assertion failed: a != 0 || b != 0, file buffering.c, line 29.
[0] FATAL: assertion failure in userspace
[0] a = 0, b = 0, c = 1, d = 1
active stack:
- symbol: void __dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > >::handler<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > > > > >(_VM_Fault, _VM_Frame*, void (*)())
location: /dios/include/dios/sys/fault.hpp:193
- symbol: __dios_fault
location: /dios/src/libc/sys/fault.c:12
- symbol: __assert_fail
location: /dios/src/libc/_PDCLIB/assert.c:19
- symbol: main
location: buffering.c:29
- symbol: _start
location: /dios/src/libc/sys/start.cpp:80
a report was written to buffering.reportDIVINE reports that it found an error, more presicely an assertion on line 29 had failed. It shows the assertion, and it also shows the output of the program, in this case a = 0, b = 0, c = 1, d = 1. Apart from this, there is a backtrace, which is mostly useful for larger programs.