Protections for Shared Variables in Multitasking Code

If your code is intended for multitasking, tasks in your code can access a common shared variable. To prevent data races, you can protect read and write operations on the variable. This topic shows the various protection mechanisms that Polyspace^® can recognize.

Detect Unprotected Access

You can detect an unprotected access using either Bug Finder or Code Prover. Code Prover is more exhaustive and proves if a shared variable is protected from concurrent access.

Bug Finder detects an unprotected access using the result Data race. See Data race.
Code Prover detects an unprotected access using the result Shared unprotected global variable. See Potentially unprotected variable (Polyspace Code Prover).

Suppose you analyze this code, specifying signal_handler_1 and signal_handler_2 as cyclic tasks. Use the analysis option Cyclic tasks (-cyclic-tasks).

#include <limits.h>
int shared_var;

void inc() {
     shared_var+=2;
}

void reset() {
     shared_var = 0;
}

void signal_handler_1(void) {
    reset();
    inc();
    inc();
}

void signal_handler_2(void) {
    shared_var = INT_MAX;
}

 void main() {
}

Bug Finder shows a data race on shared_var. Code Prover shows that shared_var is a potentially unprotected shared variable. Code Prover also shows that the operation shared_var += 2 can overflow. The overflow occurs if the call to inc in signal_handler_1 immediately follows the operation shared_var = INT_MAX in signal_handler_2.

Protect Using Critical Sections

One possible solution is to protect operations on shared variables using critical sections.

In the preceding example, modify your code so that operations on shared_var are in the same critical section. Use the functions take_semaphore and give_semaphore to begin and end the critical sections. To specify these functions that begin and end critical sections, use the analysis options Critical section details (-critical-section-begin -critical-section-end).

#include <limits.h>
int shared_var;

void inc() {
 shared_var+=2;
}

void reset() {
 shared_var = 0;
}

/* Declare lock and unlock functions */
void take_semaphore(void);
void give_semaphore(void);

void signal_handler_1() {
    /* Begin critical section */
    take_semaphore();
    reset();
    inc();
    inc();
    /* End critical section */
    give_semaphore();
    
}

void signal_handler_2() {
   /* Begin critical section */
   take_semaphore();
   shared_var = INT_MAX;
   /* End critical section */
   give_semaphore();
   
}

void main() {
}

You do not see the data race in Bug Finder. Code Prover proves that the shared variable is protected. You also do not see the overflow because the call to reset() in signal_handler_1 always precedes calls to inc().

You can also use primitives such as the POSIX^® functions pthread_mutex_lock and pthread_mutex_unlock to begin and end critical sections. For a list of primitives that Polyspace can detect automatically, see Auto-Detection of Thread Creation and Critical Section in Polyspace.

Protect Using Temporally Exclusive Tasks

Another possible solution is to specify a group of tasks as temporally exclusive. Temporally exclusive tasks cannot interrupt each other.

In the preceding example, specify that signal_handler_1 and signal_handler_2 are temporally exclusive. Use the option Temporally exclusive tasks (-temporal-exclusions-file).

Protect Using Priorities

Another possible solution is to specify that one task has higher priority over another.

In the preceding example, specify that signal_handler_1 is an interrupt. Retain signal_handler_2 as a cyclic task. Use the options Cyclic tasks (-cyclic-tasks) and Interrupts (-interrupts).

Bug Finder does not show the data race defect anymore. The reason is this:

The operation shared_var = INT_MAX in signal_handler_2 is atomic. Therefore, the operations in signal_handler_1 cannot interrupt it.
The operations in signal_handler_1 cannot be interrupted by the operation in signal_handler_2 because signal_handler_1 has higher priority.

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

A task with higher priority is atomic with respect to a task with lower priority. Note that if you use the option -detect-atomic-data-race, the analysis ignores the difference in priorities and continues to show the data race. See also Define Task Priorities for Data Race Detection in Polyspace.

Code Prover does not consider atomicity of operations, so it continues to show shared_var as a potentially unprotected variable (the operations in signal_handler_1 can still interrupt the operations in signal_handler_2). Code Prover shows shared_var as protected only when you specify both signal_handler_1 and signal_handler_2 as interrupts.

Protect By Disabling Interrupts

In a Bug Finder analysis, you can protect a group of operations by disabling all tasks and interrupts other than the current one.

Use the option Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts) to specify a routine that disables all interruption when called, and a routine that reenables them. The disabling routine disables preemption by all:

Non-cyclic tasks.
See Tasks (-entry-points).
Cyclic tasks.
See Cyclic tasks (-cyclic-tasks).
Interrupts.
See Interrupts (-interrupts).

In other words, the analysis considers that the body of operations between the disabling routine and the enabling routine is atomic and not interruptible at all.

After you call a routine to disable interrupts, all subsequent operations are atomic until you call the other routine to reenable interrupts. The operations are atomic with respect to operations in all other tasks.