Mthread

Overview

The Mthread plug-in automatically analyzes concurrent C programs, using the techniques used by Eva. At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the information delivered by the plug-in takes into account all the possible concurrent behaviors of the program.

The results of Mthread are many-fold:

For each thread, all possible instructions that can lead to a run-time error. As explained above, this information takes into account all possible interleavings between all threads.
An over-approximation of the memory zones that are accessed concurrently by more than one thread. For each zone and thread, Mthread also returns the program points at which the zone is accessed, whether the zone is read or written, and the callstack that leads to the statement.
At each program point, the list of mutexes that can be locked by the current thread. This information is used to identify shared memory zones on which race conditions may occur.
An over-approximation of the messages exchanged by all threads through explicit message-passing, along with the emission and reception points.
For each thread, a slicing of all the statements it can execute, in which only the statements related to concurrency are kept. See for example this graph.
For each program point of each thread, an over-approximation of the possible values.

Usage

The plug-in is activated with the following command line:

frama-c -mthread file1.c file2.c ... concurrent_library.c

Notice that you must explicitly pass a stubbed version of your concurrency library on the command-line. Support for the often used pthread primitives is included in the plug-in. Preliminary support for the VxWorks and Win32 libraries also exist.

The main options are:

-mt-verbose: Gives some additional information during computation.
-mt-shared-zones *n*: Shows the values written in all shared zones at level 1, and with the calling contexts in which they are written at level 2.
-mt-print-callstacks: Prints the calling context at which the concurrent operations occur.
-mt-extract html: Generates an HTML summary of the results, as well as the concurrent (sliced) graphs of each thread.

Technical Notes

The detection of race condition supposes that shared zones are protected by mutexes. Lock-free algorithms are not detected as such.
Using the plug-in requires stubbing the concurrency library, if it is not amongst of the available ones (currently pthread, VxWorks and Win32).

Dependencies

This plug-in depends on results of the Eva plug-in.

Contact

The plug-in is currently available under a proprietary licence. For any questions, remarks or suggestions, please contact Tristan Le Gall.