Main Content

Temporally exclusive tasks (-temporal-exclusions-file)

Specify entry point functions that cannot execute concurrently

Description

This option is not available for code generated from MATLAB® code or Simulink® models.

Specify entry point functions that cannot execute concurrently. The execution of the functions cannot overlap with each other.

Set Option

User interface (desktop products only): In your project configuration, the option is available on the Multitasking node. See Dependencies for other options you must also enable.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Multitasking node. See Dependencies for other options you must also enable.

Command line and options file: Use the option -temporal-exclusions-file. See Command-Line Information.

Why Use This Option

Use this option to implement temporal exclusion in multitasking code.

A Code Prover verification checks if specifying certain tasks as temporally exclusive protects all shared variables from concurrent access. When determining possible values of those shared variables, the verification accounts for the fact that temporally exclusive tasks do not interrupt each other. See Global Variables.

A Bug Finder analysis uses the temporal exclusion information to look for concurrency defects such as data race. See Concurrency Defects.

Settings

No Default

Click to add a field. In each field, enter a space-separated list of functions. Polyspace® considers that the functions in the list cannot execute concurrently.

Enter the function names manually or choose from a list.

  • Click to add a field and enter the function names.

  • Click to list functions in your code. Choose functions from the list.

Dependencies

To enable this option in the user interface of the desktop products:

You can then specify some of these functions as temporally exclusive tasks. Alternatively, if you specify your multitasking configuration using external files with the option External multitasking configuration, some of the functions from your external files can be specified as temporally exclusive.

The ability to specify temporally exclusive tasks is not supported for automatically detected thread creation routines such as pthread_create. These routines can be invoked at different points in the code to create separate threads. However, the temporal exclusion option does not support specifying two separate invocations of the same routine at different points in the code.

Tips

When considering possible values of shared variables, a Code Prover verification takes into account your specifications for temporally exclusive tasks.

However, if the shared variable is a pointer or array, the software uses the specifications only to determine if the variable is a shared protected global variable. For run-time error checking in Code Prover, the software does not take your specifications into account and considers that the variable can be concurrently accessed.

Command-Line Information

For the command-line option, create a temporal exclusions file in the following format:

  • On each line, enter one group of temporally excluded tasks.

  • Within a line, the tasks are separated by spaces.

To enter comments, begin with #. For an example, see the file polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt. Here, polyspaceroot is the Polyspace installation folder, for example C:\Program Files\Polyspace\R2019a.

Parameter: -temporal-exclusions-file
No Default
Value: Name of temporal exclusions file
Example (Bug Finder): polyspace-bug-finder -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"
Example (Code Prover): polyspace-code-prover -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"
Example (Bug Finder Server): polyspace-bug-finder-server -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -temporal-exclusions-file "C:\exclusions_file.txt"

See Also

| | | | |

Topics