Manual

I. Overview of the tool

The tool instruments programs such that they can be verified for different weak memory models (WMMs) with a model-checker verifying sequentially consistent (SC) programs. It also provides some visualisations of the WMM violation cycles the program might encounter, a list of them and their references, and a list of idioms to relate the program to some simpler, already known examples.

The objectives of this tool are manyfold:

• given a WMM, instrumenting efficiently a program, to detect some bugs related to WMM with an SC model-cheker;
• supporting real C code, and instrumenting for several architectures (currently, TSO, PSO, RMO, a fragment of Power);
• helping the debugging with the support of several fences in the instrumentation;
• assisting the debugger, by providing a clear visualisation of the potentially unsafe events on shared variables (and their locations in the code);
• providing a list of small concurrent idioms corresponding to the detected cycles, and their fixes.

II. How to install it?

You can download x86_64 binaries of goto-cc and the modified goto-instrument, and the Perl script for detecting matching idioms below:

You can download a model-checker for concurrent programs from its link:

The source of goto-cc and goto-instrument can be found below:

To compile goto-instrument, you will need glpk (for the computation of pairs to instrument with minimum interference), pthreads (for the parallel computation of cycles in the SCCs), and optionally a SAT/SMT solver for the cycle reduction option (see CBMC documentation). In the src folder, once config.inc is edited, use make cbmc.dir; make goto-cc.dir; make goto-instrument.dir to compile the binaries.

III. How to use it?

The tool is built with the CProver framework (http://www.cprover.org/). The C program is first turned into a goto-program using goto-cc -- a representation of the program common to the tools of this framework. It is then instrumented by goto-instrument, by adding some instructions to relevant places to simulate the WMM. A model-checker can finally check the program, directly from the goto-program (Satabs, CBMC-MT), or after having dumped C code from the instrumented goto-program with goto-instrument --dump-c (ESBMC, Threader, Poirot, MMChecker, Checkfence).

1) goto-cc

This program turns a program C into a goto-program. For additional information, please read the goto-cc's website.

2) goto-instrument

goto-instrument instruments a goto-program. It also generates three files:

(a) cycles.dot, a visual representation of the potentially dangerous cycles in the program. You can convert it to a picture, using for instance dot (e.g., dot -Tpng < cycles.dot > cycles.png). The graph obtained should look like the one below.

The red boxes represent the variables instrumented. A vertex is an event for a variable at a given line of the original code, and an edge between two vertices an order between those two events. The first number is the identifier of the events, that you can use when targetting specifically some events for instrumenting.

(b) ref.txt, the list of cycles instrumented. This file lists the names of all the cycles detected in the program, with the Diy notation:


(c) output.txt, the list of cycles with their locations in the code.



Here are the options that we have implemented for the instrumentation:

2.1) detection option

--wmm arch: instruments an SC program so that it behaves on SC as if it were executed on the architecture arch (among tso, pso, rmo and power)

2.2) instrumentation options

By default, the tool instruments all the unsafe pairs in the critical cycles.

(e) --one-event-per-cycle: only instruments one (arbitrary) pair per cycle (sound)

(f) --minimum-interference: only instruments one pair per cycle, choosing them with minimising a cost function (sound)

(g) --my-events: only instruments the events whose identifiers appear in inst.evt (potentially unsound). The identifiers are the integers appearing in the vertices on the dot graph. The inst.evt file is taking a first integer, the number of events to instrument, and the identifiers of the events to instrument.
For instance, on the graph above, I just want to instrument the write to y in thread 8 (id: 6) and the write to x in thread 4 (id 1). inst.evt would be:


Note that if you want to instrument an Rfe pair, you need to instrument both events.

2.3) computation options

(h) --no-dependencies: disables the dependencies analysis

(i) --scc: detection of cycles in parallel -- one SCC per thread

Note that if goto-instrument is not compiled with #define DISTRIBUTED, the --scc option treats the SCCs sequentially.

(j) --cfg-kill: enables symbolic execution used to reduce spurious cycles

(k) --max-var <n>: maximum number of shared variables appearing in a cycle. Default value is the maximum number of interferring threads (upperbound, sound).

(l) --max-po-trans <n>: maximum number of transitions by po (in the computation of an edge in po+) allowed. By default, there is no maximum (sound).

2.4) rendering options

(m) --no-po-rendering: abstract events on the same thread are represented on the same row. Dot cannot always handle very large graph with these constraints; this option relaxes them.

(n) --render-cluster-file: clusters nodes in the graph per files. Not compatible with --render-cluster-function

(o) --render-cluster-function: clusters nodes in the graph per functions. Not compatible with --render-cluster-file

3) model-checkers

3.1) directly reading from goto-programs

We directly apply the model-checker to the instrumented goto-program. Goto-instrument adds additional assertions in the program to ensure the buffers are never overflowed. If CBMC/Satabs returns a counter-example violating one of these assertions, you can look at the assertions you want to reach (use cbmc-mt/satabs --show-claims my_prog_instr.goto), and target them specifically (cbmc-mt/satabs --claim thr1.1 my_prog.goto, for instance).

CBMC-MT:
Satabs: Use Satabs with the concurrency option and the maximum number of threads N in the program. Please use the last version of Satabs.

3.2) reading from C sources

We first dump the instrumented program into a C program, and then apply a model-checker.

Checkfence:
ESBMC:
MMChecker: Use the script in the same folder as Threader's binary, or modify the path path in the script. Update the path path_ildasm with the path of ildasm.exe.
Poirot: Use the script in the Poirot's folder, or modify the path POIROT_ROOT in the script. If you use the Microsoft Visual Studio prompt, uncomment the lines in the script as explained in the file.
Threader: Use the script in the same folder as Threader's binary, or modify the path check_path in the script.
To experiment the different modes of Threader, add in the last line one of the next options:

4) cycle-matcher

This script relates detected cycles to existing WMM idioms. Cycles are presented as follows:

5) example 1: checking a program for a given architecture

We want to check that a program (derived from this Litmus test) is safe for PSO (and then safe for TSO), but not for RMO (and for Power, by inclusion). We first convert the program into a goto-program:


Then we instrument it for PSO:


We check it with Satabs:


And Satabs returns that the program is validated after 1.64 sec:


We have indeed two RW pairs, which cannot be reordered on PSO. We now investigate for RMO. We instrument with this weaker architecture, and check again with Satabs


The model-checker returns after 7.14 sec this counter-example and a failure message below.


The two RW pairs can indeed be reordered under RMO, and the assertion can be violated.

6) example 2: identifying statically some potential WMM-related bugs in a program

Let us consider the same problem, that is, checking the validity of a program for PSO and stronger, but not for RMO and weaker. But, this time, we assume that we cannot use the model-checker. This happens often when the code to check is too large. goto-instrument can provide anyway some information and visualisations to help the debugger finding the risk/bug.

We turn the program into a goto-program, and instrument it for PSO:


goto-instrument do not detect any cycle: output.txt (list of cycles in the program), ref.txt (names of the cycles), cycles.dot (graph of the cycles and the instrumented events). There is nothing to instrument. Here, if the program is safe for SC, then it is safe for the weaker architecture as well.

We do the same for RMO:


goto-instrument detects one potentially violating cycle: the PodRW Rfe PodRW Rfe (output.txt, ref.txt, cycles.dot). The picture reveals that both of the RW pairs are to be instrumented, since potentially unsafe. For large program, we may want to relate the cycles detected to some small, already known Litmus examples. We apply the script which tries to find some idioms in the detected cycle:


The cycle matcher finds one idiom already known: the idiom x86/safe006.


We can then access the Litmus file of x86/safe006, and run the example to get a better insight of the bug in the main program.

IV. How does it work?

goto-instrument first generates an abstract event graph from the input (goto-)program. It then launchs a cycle detection, to reveal all the potential violation cycles in the program for the architecture considered. The cycles are analysed, and the pairs to delay, following the chosen instrumentation strategy, marked. The instructions are then instrumented on the basis of this marking, and the model-checker can eventually run the instrumented program. More details can be found in the paper.