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

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

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

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

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

Предположим, что вы анализируете этот код, указывая 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 игнорирует разницу в приоритетах и продолжает показывать гонку данных. См. также раздел Определение прерываемых прерываний и неуполномоченных задач.

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

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

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

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

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