Configuring Polyspace Multitasking Analysis Manually

With Polyspace^®, you can analyze programs where multiple threads run concurrently. In some situations, Polyspace can detect thread creation and critical sections in your code automatically. See Auto-Detection of Thread Creation and Critical Section in Polyspace.

If your code has functions that are intended for concurrent execution, but that cannot be detected automatically, you must specify them before analysis. If these functions operate on a common variable, you must also specify protection mechanisms for those operations.

For the multitasking code analysis workflow, see Analyze Multitasking Programs in Polyspace.

Specify Options for Multitasking Analysis

Use these options to specify cyclic tasks, interrupts and protections for shared variables. In the user interface of the Polyspace desktop products, the options are on the Multitasking node in the Configuration pane. The following options can be used in both a Bug Finder and Code Prover analysis:

Tasks (-entry-points): Specify noncyclic entry point functions.
Do not specify main. Polyspace implicitly considers main as an entry point function.
Critical section details (-critical-section-begin -critical-section-end): Specify functions that begin and end critical sections.
Temporally exclusive tasks (-temporal-exclusions-file): Specify groups of functions that are temporally exclusive.

A Polyspace analysis supports four levels of task priorities. That is, the analysis can take into consideration the fact that certain tasks cannot be interrupted by tasks with lower priorities. You can use these options to indicate task priorities:

Cyclic tasks (-cyclic-tasks): Specify functions that are scheduled at periodic intervals.
Interrupts (-interrupts): Specify functions that can run asynchronously, such as interrupt handlers or signal handlers.
-preemptable-interrupts: Specify functions that have lower priority than interrupts, but higher priority than tasks (preemptable or non-preemptable).
-non-preemptable-tasks: Specify functions that have higher priority than tasks, but lower priority than interrupts (preemptable or non-preemptable).
Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts): Specify functions that disable and reenable interrupts.

For an example of using priorities, see Protections for Shared Variables in Multitasking Code.

Adapt Code for Code Prover Multitasking Analysis

The multitasking analysis in Code Prover is more exhaustive about finding potentially unprotected shared variables and therefore follows a strict model.

Tasks and interrupts must be void(void) functions.

Functions that you specify as tasks and interrupts must have the prototype:

void func(void);

Suppose you want to specify a function func that takes int arguments and has return type int:

int func(int);

Define a wrapper void-void function that calls func with a volatile value. Specify this wrapper function as a task or interrupt.

void func_wrapper() {
  volatile int arg;
  (void)func(arg);
}

You can save the wrapper function definition along with a declaration of the original function in a separate file and add this file to the analysis.

The main function must end.

Code Prover assumes that the main function ends before all tasks and interrupts begin. If the main function contains an infinite loop or run-time error, the tasks and interrupts are not analyzed. If you see that there are no checks in your tasks and interrupts, look for a token underlined in dashed red to identify the issue in the main function. See Reasons for Unchecked Code (Polyspace Code Prover).

Suppose you want to specify the main function as a cyclic task.

void performTask1Cycle(void);
void performTask2Cycle(void);

void main() {
 while(1) {
    performTask1Cycle();
  } 
}

void task2() {
 while(1) {
    performTask2Cycle();
  }
}

Replace the definition of main with:

#ifdef POLYSPACE
void main() {
}
void task1() {
 while(1) {
    performTask1Cycle();
  } 
}

#else
void main() {
 while(1) {
    performTask1Cycle();
  } 
}
#endif

The replacement defines an empty main and places the content of main into another function task1 if a macro POLYSPACE is defined. Define the macro POLYSPACE using the option

Preprocessor
                    definitions (-D)

and specify task1 for the option

Tasks
                    (-entry-points)

This assumption does not apply to automatically detected threads. For instance, a main function can create threads using pthread_create.

The Polyspace multitasking analysis assumes that a task or interrupt cannot interrupt itself.

All tasks and interrupts can run any number of times in any sequence.

The Code Prover analysis considers that all tasks and interrupts can run any number of times in any sequence.

Suppose in this example, you specify reset and inc as cyclic tasks. The analysis shows an overflow on the operation var+=2.

void reset(void) {
 var=0;
}

void inc(void) {
  var+=2;
}

Suppose you want to model a scheduling of tasks such that reset executes after inc has executed five times. Write a wrapper function that implements this sequence. Specify this new function as a cyclic task instead of reset and inc.

void task() {
 volatile int randomValue = 0;
 while(randomValue) {
   inc();
   inc();
   inc();
   inc();
   inc();
   reset();
   }
 }

Suppose you want to model a scheduling of tasks such that reset executes after inc has executed zero to five times. Write a wrapper function that implements this sequence. Specify this new function as a cyclic task instead of reset and inc.

void task() {
 volatile int randomValue = 0;
 while(randomValue) {
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   reset();
   }
 }