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

![]()
Незащищенный доступ можно обнаружить с помощью средства поиска ошибок или средства проверки кода. Средство проверки кода является более исчерпывающим и доказывает, что общая переменная защищена от параллельного доступа.
Программа Bug Finder обнаруживает незащищенный доступ, используя результат Data race. Посмотрите Data race.
Средство проверки кода обнаруживает незащищенный доступ с помощью глобальной переменной Shared unprotected. Посмотрите 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).
Вы не видите гонки данных в Bug Finder. Средство проверки кода доказывает, что общая переменная защищена. Вы также не видите переполнения, потому что вызов reset() в signal_handler_1 всегда предшествует вызовам inc().
![]()
Другим возможным решением является определение того, что одна задача имеет более высокий приоритет по сравнению с другой.
В предыдущем примере укажите, что 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).
После вызова подпрограммы для отключения прерываний все последующие операции являются атомарными до тех пор, пока не будет вызвана другая подпрограмма для повторного включения прерываний. Операции являются атомарными по отношению к операциям во всех других задачах.
![]()