-non-preemptable-tasks

Specify functions that represent nonpreemptable tasks

Syntax

-non-preemptable-tasks function1[,function2[,...]]

Description

-non-preemptable-tasks function1[,function2[,...]] specifies functions that represent nonpreemptable tasks.

The functions cannot be interrupted by other noncyclic tasks and cyclic tasks but can be interrupted by interrupts, preemptable or nonpreemptable. Noncyclic tasks are specified with the option Tasks (-entry-points), cyclic tasks with the option Cyclic tasks (-cyclic-tasks) and interrupts with the option Interrupts (-interrupts). For examples, see Define Task Priorities for Data Race Detection in Polyspace.

To specify a function as a nonpreemptable cyclic task, you must first specify the function as a cyclic or noncyclic task. The functions that you specify must have the prototype:

void function_name(void);

If you are running an analysis from the user interface (Polyspace^® desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other.

Examples

Consider the following program. Suppose that functions task1 and task2 represent tasks that can run concurrently.

int x;
void task1() {
    x++;
}
void task2() {
    x = 0;
}
void main() {
}

To specify that task1 and task2 are cyclic tasks, enter the following:

polyspace-bug-finder -sources filename -cyclic-tasks task1,task2

You see a Data race defect because the tasks attempt to concurrently access shared variable x.

Specify task1 as nonpreemptable.

polyspace-bug-finder -sources multi.c -cyclic-tasks task1,task2 -non-preemptable-tasks task1

The Data race disappears because the operation x++ in task1 cannot be interrupted anymore.

Tips

This option is not useful in a Polyspace as You Code analysis.
Code Prover interprets this option with some limitations. The reason is that Code Prover considers all operations as potentially non-atomic and interruptible. This overapproximation leads to situations where the option might appear to be ignored. For an example, see Effect of Task Priorities in Code Prover (Polyspace Code Prover).

Version History

Introduced in R2016b