Защиты для общих переменных в многозадачном коде

Если ваш код предназначен для многозадачности, задачи в вашем коде могут получить доступ к общей общей переменной. Чтобы предотвратить гонки данных, можно защитить операции чтения и записи переменной. В этой теме показаны различные механизмы защиты, которые Polyspace^® может распознать.

Обнаружение незащищенного доступа

Обнаружить незащищенный доступ можно с помощью Bug Finder или Code Prover. Code Prover является более исчерпывающим и доказывает, защищена ли общая переменная от параллельного доступа.

Bug Finder обнаруживает незащищенный доступ с помощью результирующего Data race. См. Data race.
Code Prover обнаруживает незащищенный доступ с помощью результирующего Shared unprotected global variable. См. Potentially unprotected variable (Polyspace Code Prover).

Предположим, вы анализируете этот код, определяя signal_handler_1 и signal_handler_2 как циклические задачи. Используйте опцию анализа 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 показывает гонку данных на shared_var. Code Prover показывает, что shared_var является потенциально незащищенной общей переменной. Code Prover также показывает, что операция shared_var += 2 может переполниться. Переполнение происходит, если вызов inc в signal_handler_1 немедленно следует операции shared_var = INT_MAX в signal_handler_2.

Защита с использованием критических сечений

Одним из возможных решений является защита операций с общими переменными с помощью критических разделов.

В предыдущем примере измените код так, чтобы операции на shared_var находятся в одном и том же критическом разделе. Используйте функции take_semaphore и give_semaphore чтобы начать и завершить критические участки. Чтобы задать эти функции, которые начинают и заканчивают критические сечения, используйте опции анализа 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() {
}

Вы не видите гонки данных в Bug Finder. Code Prover доказывает, что общая переменная защищена. Вы также не видите переполнение, потому что вызов reset() в signal_handler_1 всегда предшествует вызовам в inc().

Можно также использовать примитивы, такие как POSIX^® функции pthread_mutex_lock и pthread_mutex_unlock чтобы начать и закончить критические участки. Список примитивов, которые Polyspace может обнаружить автоматически, см. в разделах Автоматическое обнаружение создания потоков и Критическое сечение в Polyspace.

Защита с использованием временно эксклюзивных задач

Другое возможное решение - задать группу задач как временно эксклюзивную. Временные исключающие задачи не могут прерывать друг друга.

В предыдущем примере задайте, что signal_handler_1 и signal_handler_2 являются временными исключительными. Используйте опцию Temporally exclusive tasks (-temporal-exclusions-file).

Защита с использованием приоритетов

Другое возможное решение состоит в том, чтобы указать, что одна задача имеет более высокий приоритет над другой.

В предыдущем примере задайте, что signal_handler_1 является прерыванием. Сохраните signal_handler_2 как циклическая задача. Используйте опции Cyclic tasks (-cyclic-tasks) и Interrupts (-interrupts).

Bug Finder больше не показывает дефект гонки данных. Причина в следующем:

Область операции shared_var = INT_MAX в signal_handler_2 является атомарным. Поэтому операции в signal_handler_1 невозможно прервать его.
Операции в signal_handler_1 не может быть прервана операцией в signal_handler_2 потому что signal_handler_1 имеет более высокий приоритет.

Вы можете задать до четырех различных приоритетов с этими опциями (с наивысшим приоритетом, перечисленным первым):

Задача с более высоким приоритетом является атомарной относительно задачи с более низким приоритетом. Обратите внимание, что шашка Data race including atomic operations игнорирует различия в приоритетах и продолжает показывать гонку данных. Смотрите также «Определение предопределяемых прерываний и незапускаемых задач».

Code Prover не рассматривает приоритеты задач. Поэтому Code Prover все еще показывает shared_var как потенциально незащищенная глобальная переменная.

Защита путем отключения прерываний

При анализе Bug Finder можно защитить группу операций, отключив все прерывания. Используйте опцию Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts).

После того, как вы вызываете стандартную программу, чтобы отключить прерывания, все последующие операции являются атомарными, пока вы не вызываете другую стандартную программу, чтобы возобновить прерывания. Операции являются атомарными в отношении операций во всех других задачах.

Документация