Расширение проверки дефектов параллелизма до неподдерживаемых многопоточных окружений

В этом разделе показано, как адаптировать проверки дефектов параллелизма к неподдерживаемым многопоточным окружениям, например, когда создание нового потока не обнаруживается автоматически.

Идентифицируйте необходимость расширения средства проверки

По умолчанию 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);
}

Bug Finder не обнаруживает вызов 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.

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

Шашки, которые могут быть расширены

Проверяющие дефекты параллелизма, которые могут быть расширены таким образом:

См. также

-code-behavior-specifications

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