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