С Polyspace®можно анализировать программы, где несколько потоков (задач) выполняются одновременно.
В дополнение к регулярным проверкам во время выполнения анализ ищет проблемы, характерные для параллельного выполнения:
Гонки данных, тупики, последовательные или отсутствующие блокировки и разблокировки (Bug Finder)
Незащищенные общие переменные (Code Prover)
Если ваш код использует примитивы многозадачности из определенных семейств, например pthread_create для создания потоков:
В Bug Finder анализ обнаруживает их и извлекает вашу модель многозадачности из кода.
В Code Prover это автоматическое обнаружение необходимо включить явным образом.
Смотрите раздел «Автоматическое обнаружение создания резьбы и критического сечения» в Polyspace.
Кроме того, определите свою модель многозадачности через опции анализа. В пользовательском интерфейсе опции находятся на узле Multitasking в панели Configuration. Для получения дополнительной информации смотрите Настройка многозадачного анализа Polyspace вручную.
Анализ Bug Finder показывает дефекты параллелизма, такие как гонки данных и тупики. См. «Дефекты параллелизма».
Анализ Code Prover полностью проверяет, защищены ли общие глобальные переменные от параллельного доступа. См. «Глобальные переменные» (Polyspace Code Prover).
Просмотрите результаты с помощью сообщения на панели Result Details. Смотрите визуальное представление конфликтующих операций с помощью
значка ( графиков).
