При проверке многозадачного кода Polyspace ® считает, что критический раздел лежит между вызовами функции блокировки и разблокировки.
lock(); /* Critical section code */ unlock();
Группа операций в критической секции является атомной по отношению к другой группе операций, которые находятся в той же критической секции (то есть имеют ту же функцию блокировки и разблокировки). См. также раздел Определение атомных операций в многозадачном коде.
Polyspace игнорирует аргументы для функций, начинающих и заканчивающих критические разделы.
Например, если указать, Polyspace рассматривает два приведенных ниже раздела кода как один и тот же критический раздел. my_task_1 и my_task_2 в качестве точек входа, my_lock в качестве функции блокировки и my_unlock в качестве функции разблокировки.
int shared_var;
void my_lock(int);
void my_unlock(int);
void my_task_1() {
my_lock(1);
/* Critical section code */
shared_var=0;
my_unlock(1);
}
void my_task_2() {
my_lock(2);
/* Critical section code */
shared_var++;
my_unlock(2);
}В результате анализ считает, что эти две секции защищены от прерывания друг друга, даже если они не могут быть защищены. Например, Bug Finder не обнаруживает гонки данных на shared_var.
Часто аргументы функции могут быть определены только во время выполнения. Поскольку Polyspace моделирует критические разделы до фазы статического анализа и проверки ошибок во время выполнения, анализ не может определить, отличаются ли аргументы функции, и игнорирует аргументы.
Когда аргументами к функциям, определяющим критические сечения, являются константы времени компиляции, можно адаптировать анализ для работы с предположением Polyspace.
Например, можно использовать опции анализа Polyspace, чтобы код в предыдущем примере отображался в Polyspace, как показано здесь.
int shared_var;
void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);
void my_task_1() {
my_lock_1();
/* Critical section code */
shared_var=0;
my_unlock_1();
}
void my_task_2() {
my_lock_2();
/* Critical section code */
shared_var++;
my_unlock_2();
}Если затем указать my_lock_1 и my_lock_2 в качестве функций блокировки и my_unlock_1 и my_unlock_2 как функция разблокировки, анализ распознает два раздела кода как часть различных критических разделов. Например, Bug Finder обнаруживает гонку данных на shared_var.
Чтобы адаптировать анализ для функций блокировки и разблокировки, которые принимают константы времени компиляции в качестве аргументов:
В файле заголовка common_polyspace_include.h, преобразовать аргументы функции в расширения имени функции с помощью #define-s. Кроме того, предоставьте объявление для новых функций.
Например, для предыдущего примера используйте эти #define-s и объявления:
#define my_lock(X) my_lock_##X() #define my_unlock(X) my_unlock_##X() void my_lock_1(void); void my_lock_2(void); void my_unlock_1(void); void my_unlock_2(void);
Укажите имя файла common_polyspace_include.h в качестве аргумента для опции Include (-include).
Анализ рассматривает этот файл заголовка как #include-d во всех исходных файлах, которые анализируются.
Укажите новые имена функций в качестве начальных и конечных критических разделов. Использовать опции Critical section details (-critical-section-begin -critical-section-end).
Critical section details (-critical-section-begin -critical-section-end)