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