Main Content

Multitasking

Task entry points, critical sections, exclusive tasks

To set up verification of multiple tasks or threads that run concurrently, use the multitasking options. Polyspace® interprets certain families of multitasking functions. Unless you use these functions, you must explicitly specify which functions in your code indicate entry points, cyclic tasks, or interrupts. You must also specify the protection mechanisms for shared variables.

Polyspace Options

Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)Automatically detect certain families of multithreading functions
External multitasking configurationEnable setup of multitasking configuration from external file definitions
OIL files selection (-osek-multitasking)Set up multitasking configuration from OIL file definition
ARXML files selection (-autosar-multitasking)Set up multitasking configuration from ARXML file definitions
Configure multitasking manuallyConsider that code is intended for multitasking
Tasks (-entry-points)Specify functions that serve as tasks to your multitasking application
Cyclic tasks (-cyclic-tasks)Specify functions that represent cyclic tasks
Interrupts (-interrupts)Specify functions that represent nonpreemptable interrupts
Critical section details (-critical-section-begin -critical-section-end)Specify functions that begin and end critical sections
Temporally exclusive tasks (-temporal-exclusions-file)Specify entry point functions that cannot execute concurrently

Topics

Related Information