The Mthread plug-in
The Mthread plug-in automatically analyzes concurrent C programs, using the techniques used by the Value analysis. At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the information delivered by the plug-in take 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 is written, and the callstack that lead 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
The plug-in is currently available under a proprietary licence. You can contact supportframa-c.com to obtain such a licence.
Evaluation versions, in the form of pre-compiled binaries compatible with Frama-C Oxygen, are also available for some platforms. Do not hesitate to contact us if you are interested.
The plug-in is activated with the following command line:
frama-c -mthread file1.c file2.c ... concurrent_library.c
Notice that you must explicitely 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:
- Gives some additional information during computation.
- -mt-shared-zones n
- Show the values written in all shared zones at level 1, and with the calling contexts in which they are written at level 2.
- Print the calling context at which the concurrent operations occur.
- -mt-extract html
- Generate an html summary of the results, as well as the concurrent (sliced) graphs of each thread.
- Gives the whole list of options
- 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).
For any questions, remarks or suggestions, please contact Boris Yakobowski.