При проверке многозадачного кода 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-с. В сложение предоставьте декларацию для новых функций.
Для образца в предыдущем примере используйте эти #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)