Analyze Multitasking Programs in Polyspace

With Polyspace^®, you can analyze programs where multiple threads (tasks) run concurrently.

Diagram of multiple tasks running concurrently with code example.

In addition to regular run-time checks, the analysis looks for issues specific to concurrent execution:

Data races, deadlocks, consecutive or missing locks and unlocks (Bug Finder)
Unprotected shared variables (Code Prover)

Configure Analysis

Example Multitasking Configuration in Polyspace.

If your code uses multitasking primitives from certain families, for instance, pthread_create for thread creation:

In Bug Finder, the analysis detects them and extracts your multitasking model from the code.
In Code Prover, you must enable this automatic detection explicitly. See Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection).

See Auto-Detection of Thread Creation and Critical Section in Polyspace.

Alternatively, define your multitasking model through the analysis options. In the user interface of the Polyspace desktop products, the options are on the Multitasking node in the Configuration pane. Most options are common between Bug Finder and Code Prover. The multitasking analysis in Code Prover is more exhaustive about finding potentially unprotected shared variables and therefore follows a stricter model. Your code must be written in a specific format for Code Prover to successfully complete a multitasking analysis. For instance, the functions that you specify as entry points must be void(void) functions. However, if your code is not already written in this format, you can work around the restrictions. For details, see Configuring Polyspace Multitasking Analysis Manually.

Review Analysis Results

Bug Finder

Example data race defect showing different tasks interfering with one another.

A Bug Finder analysis can find many different kinds of concurrency defects including:

Data races, when operations on a variable from different tasks interfere with each other.
Deadlocks or double locks, because of incorrect placement of lock and unlock functions

For the complete list, see Concurrency Defects. However, the analysis makes certain assumptions to avoid false positives, and might not find all data races. You can perform an initial check for data races with Bug Finder, and make a more exhaustive pass later with Code Prover.

Code Prover

Code Prover analysis example where a potentially unprotected variable finding shows several tasks sharing the same variable.

The Code Prover analysis exhaustively checks if shared global variables are protected from concurrent access. The analysis reports variables that are definitely protected in green and variables that might be unprotected in orange. See Global Variables.

Review the results using the message on the Result Details pane. See a visual representation of conflicting operations using the (graph) icon.

Differences Between Bug Finder and Code Prover

The following table summarizes the differences between the multitasking analysis in Polyspace Bug Finder™ and Polyspace Code Prover™.

Configuration

Bug Finder Code Prover

Auto-detection of concurrency routines Supported by default Supported on option Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)

	Bug Finder	Code Prover
Auto-detection of concurrency routines	Supported by default	Supported on option `Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)`
Constraints on `main` function	None	The `main` function must terminate. It cannot contain an infinite loop or a run-time error. For workarounds if there is an intentional infinite loop in `main`, see Adapt Code for Code Prover Multitasking Analysis.
Atomic operations	Depending on the target size, certain operations are considered as atomic (non-interruptable). To consider all operations as non-atomic, use the option `-detect-atomic-data-race`. See also `Define Atomic Operations in Multitasking Code`.	All operations are considered as non-atomic.

Constraints on main function

None

The main function must terminate. It cannot contain an infinite loop or a run-time error.

For workarounds if there is an intentional infinite loop in main, see Adapt Code for Code Prover Multitasking Analysis.

Atomic operations

Depending on the target size, certain operations are considered as atomic (non-interruptable).

To consider all operations as non-atomic, use the option -detect-atomic-data-race. See also Define Atomic Operations in Multitasking Code.

All operations are considered as non-atomic.

Results

Bug Finder Code Prover

Concurrent unprotected access on shared variables (data races)

	Bug Finder	Code Prover
Concurrent unprotected access on shared variables (data races)	Shown using one of these results: `Data race` `Data race on adjacent bit fields` `Data race through standard library function call`	Shown using the result `Potentially unprotected variable`. Code Prover is more exhaustive when keeping track of control and data flows. Therefore, Code Prover might detect probable data races not detected with Bug Finder.
Issues with concurrency routines besides data race: Deadlocks, double locks, missing unlocks, and so on. Improper thread creation, joining or destruction. Memory escape from threads	Detected	Not detected

Shown using one of these results:

Shown using the result Potentially unprotected variable.

Code Prover is more exhaustive when keeping track of control and data flows. Therefore, Code Prover might detect probable data races not detected with Bug Finder.

Issues with concurrency routines besides data race:

Deadlocks, double locks, missing unlocks, and so on.
Improper thread creation, joining or destruction.
Memory escape from threads

Detected

Not detected