В этом разделе показано, как адаптировать проверки дефектов параллелизма к неподдерживаемым многопоточным средам, например, когда создание нового потока не обнаруживается автоматически.
По умолчанию Bug Finder может обнаруживать примитивы параллелизма только в некоторых семействах (в Code Prover для опции доступно то же самое автоматическое обнаружение). См. раздел Автоматическое обнаружение создания резьбы и критического сечения в Polyspace. Если используются примитивы, которые не принадлежат к одному из поддерживаемых семейств, но имеют сходные синтаксисы, можно сопоставить создание потока и другие связанные с параллелизмом функции с поддерживаемыми функциями.
Например, в следующем примере используется:
Функция createTask для создания нового потока.
Функция takeLock для начала критического раздела.
Функция releaseLock для завершения критического сечения.
typedef void* (*FUNT) (void*);
extern int takeLock(int* t);
extern int releaseLock(int* t);
// First argument is the function, second the id
extern int createTask(FUNT,int*,int*,void*);
int t_id1,t_id2;
int lock;
int var1;
int var2;
void* task1(void* a) {
takeLock(&lock);
var1++;
var2++;
releaseLock(&lock);
return 0;
}
void* task2(void* a) {
takeLock(&lock);
var1++;
releaseLock(&lock);
var2++;
return 0;
}
void main() {
createTask(task1,&t_id1,0,0);
createTask(task2,&t_id2,0,0);
}
Средство поиска ошибок не обнаруживает вызов createTask как создание нового потока, где поток управления переходит к функции запуска потока (первый аргумент createTask). Неправильное размещение функции releaseLock в task2 и возможность гонки данных по незащищенной совместно используемой переменной var2 остается необнаруженным.
Однако подпись createTask, takeLock и releaseLock аналогичны соответствующим функциям POSIX ® ,pthread_create, pthread_mutex_lock и pthread_mutex_unlock. Порядок аргументов этих функций может отличаться от их эквивалентов POSIX.
Поскольку создание потока POSIX может быть обнаружено автоматически, сопоставьте создание потока и другие связанные с параллелизмом функции с их эквивалентами POSIX. Например, в предыдущем примере выполните следующее сопоставление:
createTask → pthread_create
takeLock → pthread_mutex_lock
releaseLock → pthread_mutex_unlock
Для выполнения сопоставления:
Перечисление каждого сопоставления в XML-файле в определенном синтаксисе.
Копирование файла шаблона code-behavior-specifications-template.xml из папки polyspaceroot\polyspace\verifier\cxx
<function name="createTask" std="pthread_create" >
<mapping std_arg="1" arg="2"></mapping>
<mapping std_arg="3" arg="1"></mapping>
<mapping std_arg="2" arg="3"></mapping>
<mapping std_arg="4" arg="4"></mapping>
</function>
<function name="takeLock" std="pthread_mutex_lock" >
</function>
<function name="releaseLock" std="pthread_mutex_unlock" >
</function>createTask кому pthread_create, требуется переотображение аргументов, поскольку аргументы не соответствуют точно. Например, процедура запуска потока является третьим аргументом pthread_create но первый аргумент createTask.Удалите ранее существующие записи в файле, чтобы избежать предупреждений.
Укажите этот XML-файл в качестве аргумента для параметра -code-behavior-specifications.
Если невозможно выполнить сопоставление с одним из поддерживаемых семейств примитивов параллелизма, необходимо настроить многозадачный анализ вручную. См. раздел Настройка многозадачного анализа в многозадачном пространстве вручную.
Проверки дефектов параллелизма, которые могут быть расширены таким образом: