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