Concurrency Analysis with Polyspace

This article outlines two improvements in R2018a that make reviewing data races and other multitasking-based results much easier.

Polyspace® has supported concurrency analysis of multitasking and multithreaded code for some time. Polyspace Bug Finder™ includes checkers for common defects such as data race, deadlock, and double lock. (Learn more in documentation.) Polyspace Code Prover™ supports verification of multiple tasks or threads that run concurrently. (Learn how to set this up in documentation.)

Highlighting Critical Data Races

In R2018a, the Polyspace Bug Finder data race checker can distinguish write-write conflicts from the more benign read-write conflicts. You can choose to review only data races that come from conflicts between two write operations. The messaging provided in the Results Details section (the yellow box in the Results Details window as shown below), will include an additional line of text stating, “Variable value may be altered by write-write concurrent access.”

The Results Details window provides write-write conflict information.

As shown in the following figure, in the Results List window, you can use the Detail column to filter data races that have this condition.  Using this filtering, you can focus on conflicts between two write operations in different threads that can lead to corruption of memory and indeterminate results. These write-write conflicts are no longer hidden amidst more benign conflicts between a write and read operation.

In the Results List window, you can use the Detail column to filter data races.

Display of Concurrency Modeling

In R2018a, Polyspace Bug Finder and Polyspace Code Prover give you the ability to view all tasks and interrupts extracted from your code, along with the configuration that you create, in a simple consolidated view. To see this consolidated view, click the Concurrency Modeling link on the dashboard after the Polyspace analysis is complete. This new view of the analysis provides you with two benefits:

  • Easy spot-check for concurrency modeling: You can check that Polyspace correctly detected your multitasking configuration from your code. For instance, if you know a specific function acts as an interrupt, you can confirm Polyspace has detected and configured the function as an interrupt.
  • Determination of priorities: The entry points in this consolidated view are grouped in the order of priorities: interrupts, preemptable interrupts, non-preemptable tasks, and (preemptable) tasks. To understand why a data race does not occur between two entry points (with Polyspace Bug Finder), you can check if one of the entry points has lower priority than the other.

The Concurrency Modeling link gives a consolidated view.

Static Analysis with Polyspace Products