Меры защиты для совместно используемых переменных в многозадачном коде

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

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

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

Средство поиска ошибки обнаруживает незащищенный доступ с помощью результата Data race. Смотрите Data race.
Программа автоматического доказательства кода обнаруживает незащищенный доступ с помощью результата Shared unprotected global variable. Смотрите Potentially unprotected variable.

Предположим, что вы анализируете этот код, задавая 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() {
}

Средство поиска ошибки показывает гонку данных на shared_var. Программа автоматического доказательства кода показывает, что shared_var является потенциально незащищенной совместно используемой переменной. Программа автоматического доказательства кода также показывает, что операция 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() {
}

Вы не видите, что данные мчатся в Средстве поиска Ошибки. Программа автоматического доказательства кода доказывает, что совместно используемая переменная защищена. Вы также не видите переполнение, потому что вызов 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).

Средство поиска ошибки больше не показывает дефект гонки данных. Причина - это:

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

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

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

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

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

В анализе Средства поиска Ошибки можно защитить группу операций путем отключения всех прерываний. Используйте опцию Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts).

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

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