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

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

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

По умолчанию Средство поиска Ошибки может обнаружить примитивы параллелизма в определенных семействах только (в Программе автоматического доказательства Кода, то же автоматическое обнаружение доступно на опции). Смотрите Автоматическое обнаружение Создания Потока и Критического Раздела в 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.

Если вы не можете выполнить отображение с одним из поддерживаемых семейств примитивов параллелизма, необходимо настроить многозадачный анализ вручную. Смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.

Средства проверки, которые могут быть расширены

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

Смотрите также

-code-behavior-specifications

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