--- layout: plugin title: Mthread description: Analyzes concurrent C programs, taking into account all possible thread interactions. Provides precise information about shared variables, which mutex protects a part of the code, etc. key: concurrent ---
Overview

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[at]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 .