-detect-atomic-data-race

Description

-detect-atomic-data-race specifies that the analysis must check for data races in atomic operations.

By default, Polyspace does not check for data races in atomic operations. Bug Finder considers an operation as atomic if it can be performed in one machine instruction. For instance:

See Define Atomic Operations in Multitasking Code. If you do not want to use this definition of atomic operations and want to check every operation for data races, specify the option -detect-atomic-data-race.

If you run verification from the user interface (desktop products only), specify the option in the Other field. See Other.

Examples

In the code example, the write operation var=1; in task task1 executes concurrently with the read operation local_var=var; in task task2. By default, Polyspace^® assumes that the write operation is atomic. Based on your environment, you might want to extend the data race checker to include the write operation.

 Code Example

#include<stdio.h>

int var;

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

void task1(void) {
    var = 1;
}

void task2(void) {
    int local_var;
    local_var = var;
    printf("%d", local_var);
}

void task3(void) {
    begin_critical_section();
    /* Operations in task3 */
    end_critical_section();
}

To check the atomic operations in this example for data races, at the command line, specify these options:

 polyspace-bug-finder -sources SRC -checkers DATA_RACE
   -entry-points task1,task2,task3
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1
   -detect-atomic-data-race

Option	Specification
Other	-detect-atomic-data-race
Configure multitasking manually
Tasks (-entry-points)	task1 task2 task3
Critical section details (-critical-section-begin -critical-section-end)	Starting routine	Ending routine
	begin_critical_section	end_critical_section