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

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

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

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

Bug Finder обнаруживает незащищенный доступ с помощью результата 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() {
}

Bug Finder показывает гонку данных на 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() {
}

Вы не видите, что данные мчатся в Bug Finder. Программа автоматического доказательства кода доказывает, что совместно используемая переменная защищена. Вы также не видите переполнение потому что вызов 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 игнорирует различие в приоритетах и продолжает показывать гонку данных. См. также Задают Прерывания Preemptable и Задачи Nonpreemptable.

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

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

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

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

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