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:

Installation

The plug-in is currently available under a proprietary licence. You can contact support@frama-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.

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

-mt-verbose
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.
-mt-print-callstacks
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.
-mt-help
Gives the whole list of options

Ressources

Known Restrictions

Contact

For any questions, remarks or suggestions, please contact .