Define Preemptable Interrupts and Nonpreemptable Tasks

Bug Finder detects data races between concurrent tasks. Using Bug Finder analysis options, you can fix data race detection 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):

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:

  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.

  • Enable the checker Data race including atomic operations (Polyspace Bug Finder Access) (not enabled by default). Use the option Find defects (-checkers).

    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.

See Also

Polyspace Analysis Options

Polyspace Results

Related Topics