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)	Запуск подпрограммы	Завершение процедуры
	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. Дефект гонки данных возникает из-за операции 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;
}