-force-data-races

Detect data races involving only atomic operations even when no critical sections are defined

Syntax

-force-data-races


Description

-force-data-races enforces detection of data races involving only atomic operations even when no critical sections are defined.

By default, Bug Finder detects data races only if one or both operations accessing a shared variable is nonatomic. You can explicitly enable detection of data races involving only atomic operations. See Data race including atomic operations. However, if you do not use critical sections at all in your code, to avoid flagging too many operations, this kind of data race detection is still disabled. To force detection of data races involving atomic operations only even in the absence of critical sections, use the option -force-data-races.

Examples

In this example, the variable sharedVar1 is shared between threads with start functions thread1_main and thread2_main but operations on sharedVar1 are not protected against concurrent access. If you run Bug Finder with the option -checkers data_race_all, you do not see a data race because the code does not use critical sections at all. A critical section, for instance, would involve use of a pthread_mutex_lock-pthread_mutex_unlock pair.

You also see a warning in the log:

Warning: Checker 'Data Race' is activated but no protection have been defined
Warning: Checker 'Data Race including atomic operations' is disabled because no critical sections, temporal exclusions or routines to disable/enable all interrupts have been defined.
|        To force activation of this checker use option -force-data-races

 Code Example

#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
#include <pthread.h>

#define MAX_LOOP_THREAD 1000
#define EXIT_CHAR 'c'

uint32_t sharedVar1 = 0;

pthread_mutex_t mtxForShV1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t mtxForShV2 = PTHREAD_MUTEX_INITIALIZER;

void *thread1_main(void *arg)
{
    int32_t loop = 0;
    int32_t tmp = 0;

    while (loop<MAX_LOOP_THREAD)
    {
        sharedVar1 = 11;
        tmp = sharedVar1;

        usleep(50000); //50ms - Assume some operations here

        if (tmp != sharedVar1) {
          printf("thread:%d, sharedVar1= %u and tmp = %d differ\n",
          *(int*)arg, sharedVar1, tmp);
        }
        else {
          printf("thread:%d, sharedVar1= %u, tmp = %d\n",
          *(int*)arg, sharedVar1, tmp);
        }
        
        loop++;
    }

    pthread_exit((void *) 0);

    return NULL;
}

void *thread2_main(void *arg)
{
    int32_t loop = 0;
    int32_t tmp = 0;

    while (loop<MAX_LOOP_THREAD)
    {
        
        sharedVar1 = 21;
        tmp = sharedVar1;

        usleep(50000); //50ms - Assuming some operations here
        
        if (tmp != sharedVar1) {
          printf("thread:%d, sharedVar1= %u and tmp = %d differ\n",
          *(int*)arg, sharedVar1, tmp);
        }
        else {
          printf("thread:%d, sharedVar1= %u, tmp = %d\n",
          *(int*)arg, sharedVar1, tmp);
        }

        loop++;
    }

    pthread_exit((void *) 0);

    return NULL;
}


int main(void)
{
    int32_t status, errorStatus;
    static int32_t data1 = 1, data2 = 2, data3 = 3;
    pthread_t thread1, thread2, thread3;
	
    errorStatus = pthread_create(&thread1, NULL, &thread1_main, &data1);
    if (0 != errorStatus) {
        printf("thread1: pthread_create return errno : %d\n", errorStatus);
        exit(0);
    }

    errorStatus = pthread_create(&thread2, NULL, &thread2_main, &data2);
    if (0 != errorStatus) {
        printf("thread2: pthread_create return errno : %d\n", errorStatus);
        exit(0);
    }

    else {
        
        errorStatus = pthread_join(thread2, (void**)&status);
        if (0 != errorStatus) {
            printf("thread2: pthread_join return errno : %d\n", errorStatus);
            exit(0);
        }

        errorStatus = pthread_join(thread1, (void**)&status);
        if (0 != errorStatus) {
            printf("thread1: pthread_join return errno : %d\n", errorStatus);
            exit(0);
        }
    }

	return 0;
}

To see data races despite the absence of critical sections, use the option -force-data-races.

• Bug Finder:

  polyspace-bug-finder -checkers data_race_all -force-data-races

• Bug Finder Server:

  polyspace-bug-finder-server -checkers data_race_all -force-data-races

Tips

This option is not useful in a Polyspace as You Code analysis.