int var;
void begin_critical_section(void);
void end_critical_section(void);

void increment(void) {
    var++; 
}

void task1(void)  { 
      increment();
}

void task2(void)  { 
      increment();
}

void task3(void)  { 
     begin_critical_section();
     increment();
     end_critical_section();
}

В этом примере, чтобы эмулировать поведение в многозадачном режиме, задайте следующие опции:

Опция	Спецификация
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

В командной строке можно использовать следующее:

 polyspace-bug-finder 
   -entry-points task1,task2,task3
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1

В этом примере задачи task1, task2, и task3 вызвать функцию increment. increment содержит операцию var++ который может включать несколько машинных команд, включая:

Эти машинные инструкции, при выполнении из task1 и task2, может происходить одновременно в непредсказуемой последовательности. Для примера, чтения var от task1 может произойти либо до, либо после записи в var от task2. Поэтому значение var может быть непредсказуемым.

Хотя task3 вызывает increment внутри критического раздела другие задачи не используют тот же критический раздел. Операции в критическом разделе task3 не являются взаимоисключающими с операциями в других задачах.

Поэтому три задачи работают с общей переменной без общей защиты. В подробных данных результата вы видите каждую пару конфликтующих вызовов функций.

Если вы кликните значок, вы увидите последовательность вызова функции, начиная с точки входа и заканчивая операцией чтения или записи. Вы также видите, что операция, начиная с task3 находится в критическом разделе. Запись Access Protections показывает функцию блокировки и разблокировки, которая начинает и заканчивает критический раздел. В этом примере вы видите функции begin_critical_section и end_critical_section.

 polyspace-bug-finder 
     -temporal-exclusions-file "C:\exclusions_file.txt"

task1 task2 task3

#include <pthread.h>

pthread_mutex_t count_mutex;
long long count;


void* increment_count(void* args)
{
    count = count + 1;
    return NULL;
}

void* set_count(void *args)
{
    long long c;
    c = count;
    return NULL;
}

int main(void)
{
    pthread_t thread_increment;
    pthread_t thread_get;

    pthread_create(&thread_increment, NULL, increment_count, NULL);
    pthread_create(&thread_get, NULL, set_count, NULL);
    
    pthread_join(thread_get, NULL);
    pthread_join(thread_increment, NULL);

    return 1;
}

В этом примере Bug Finder обнаруживает создание отдельных потоков с pthread_create. Дефект Data race возникает из-за операции count = count + 1 в нити с идентификатором thread_increment конфликтует с операцией c = count в нити с идентификатором thread_get. Переменная count доступ к нему осуществляется в нескольких потоках без общей защиты.

Две конфликтующие операции неатомны. Область операции c = count является неатомным для 32-битных целевых объектов. См. «Определение атомарных операций в многозадачном коде».

#include <pthread.h>

pthread_mutex_t count_mutex;
long long count;


void* increment_count(void* args)
{
    pthread_mutex_lock(&count_mutex);
    count = count + 1;
    pthread_mutex_unlock(&count_mutex);
    return NULL;        
}

void* set_count(void *args)
{
    long long c;
    pthread_mutex_lock(&count_mutex);
    c = count;
    pthread_mutex_unlock(&count_mutex);
    return NULL;
}

int main(void)
{
    pthread_t thread_increment;
    pthread_t thread_get;

    pthread_create(&thread_increment, NULL, increment_count, NULL);
    pthread_create(&thread_get, NULL, set_count, NULL);

    pthread_join(thread_get, NULL);
    pthread_join(thread_increment, NULL);

    return 1;
}