Define Task Priorities for Data Race Detection in Polyspace

Bug Finder detects data races between concurrent tasks. One of the ways you can fix data races is by specifying that certain tasks have higher priorities over others. A task with higher priority is atomic with respect to tasks with lower priority and cannot be interrupted by those tasks.

Emulating Task Priorities

You can specify up to four different priorities with these options (with highest priority listed first):

• Interrupts (nonpreemptable): Use option Interrupts (-interrupts).

• Interrupts (preemptable): Use options Interrupts (-interrupts) and -preemptable-interrupts.

• Cyclic tasks (nonpreemptable): Use options Cyclic tasks (-cyclic-tasks) and -non-preemptable-tasks.

  You can also define nonpreemptable noncyclic tasks with the option Tasks (-entry-points) and -non-preemptable-tasks.

• Cyclic tasks (preemptable): Use option Cyclic tasks (-cyclic-tasks).

  You can also define noncyclic tasks with the option Tasks (-entry-points).

For instance, interrupts have the highest priority and cannot be preempted by other tasks. To define a class of interrupts that can be preempted, lower their priority by making them preemptable.

Examples of Task Priorities

Consider this example with three tasks. A variable var is shared between the two tasks task1 and task2 without any protection such as a critical section. Depending on the priorities of task1 and task2, Bug Finder shows a data race. The third task is not relevant for the example (and is added only to include a critical section, otherwise data race detection is disabled).

int var;

void begin_critical_section(void);
void end_critical_section(void);

void task1(void)  { 
    var++;
}

void task2(void)  { 
    var = 0;
}

void task3(void){
    begin_critical_section();
    /* Some atomic operation */
    end_critical_section();
}

Adjust the priorities of task1 and task2 and see whether a data race is detected. For instance:

1. Configure these multitasking options:

   • Interrupts (-interrupts): Specify task1 and task2 as interrupts.

   • Cyclic tasks (-cyclic-tasks): Specify task3 as a cyclic task.

   • Critical section details (-critical-section-begin -critical-section-end): Specify begin_critical_section as a function beginning a critical section and end_critical_section as a function ending a critical section.

2. Run Bug Finder.

   You do not see a data race. Since task1 and task2 are nonpreemptable interrupts, the shared variable cannot be accessed concurrently.

3. Change task1 to a preemptable interrupt by using the option -preemptable-interrupts.

4. Run Bug Finder again. You now see a data race on the shared variable var.

Further Explorations

Modify this example in the following ways and see the effect of the modification:

• Change the priorities of task1 and task2.

  For instance, you can leave task1 as a nonpreemptable interrupt but change task2 to a preemptable interrupt by using the option -preemptable-interrupts.

  The data race disappears. The reason is:

  • task1 has higher priority and cannot be interrupted by task2.

  • The operation in task2 is atomic and cannot be interrupted by task1.

• Specify the option -detect-atomic-data-race.

  You see the data race again. The checker considers all operations as potentially nonatomic and the operation in task2 can now be interrupted by the higher priority operation in task1.

Try other modifications to the analysis options and see the result of the checkers.

Effect of Task Priorities in Code Prover

The options to specify task priorities are also accepted in Code Prover. However, Code Prover considers all operations as potentially non-atomic and interruptible. This overapproximation can lead to situations where the task priority specifications appear to be ignored.

For instance, in the preceding example, if you run Code Prover, the overapproximation can lead to false positives.

• If you specify both task1 and task2 as nonpreemptable interrupts, the shared variable var appears as a green Shared protected global variable. This is a sound result since both tasks cannot be interrupted.

• If you specify that task1 has lower priority than task2, the shared variable var appears as an orange Potentially unprotected variable. This is a sound and precise result since the operation var++ in task1 is nonatomic and involves more than one machine instruction. The operation can be interrupted by the operation var = 0 in task2.

• If you specify that task1 has higher priority than task2, the shared variable var still appears as an orange Potentially unprotected variable. This is a sound but imprecise result:

  • The operation var++ in task1 cannot be interrupted because of the higher priority of task1.

  • The operation var = 0 in task2 cannot be interrupted because it is atomic.

  However, because Code Prover considers all operations as potentially non-atomic, it considers var = 0 in task2 as interruptible and therefore continues to show var as potentially unprotected.