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
distrib_mode:proprietary
manual_pdf:/download/frama-c-mthread-manual.pdf
---
## 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