В коде с несколькими потоками можно использовать Polyspace® Bug Finder™, чтобы обнаружить гонки данных или Polyspace Code Prover™, чтобы перечислить потенциально незащищенные совместно используемые переменные.
Определить, защищена ли переменная, совместно использованная несколькими потоками, от параллельного доступа, проверки Polyspace, если операции на переменной являются атомарными.
Если операция является неатомарной, Polyspace полагает, что операция включает несколько шагов. Эти шаги не должны происходить вместе и могут быть прерваны операциями в других потоках.
Например, рассмотрите эти две операции в двух различных потоках:
Распараллельте 1: var++;
Эта операция является неатомарной, потому что она происходит на трех шагах: чтение var, постепенное увеличение var, и обратная запись var.
Распараллельте 2: var = 0;
Эта операция является атомарной если размер var меньше размера слова на цели. Смотрите детали ниже для того, как Polyspace определяет размер слова.
Если эти две операции не защищены (при помощи, например, критические разделы), операция во втором потоке может прервать операцию в первом потоке. Если прерывание происходит после var постепенно увеличивается в первом потоке, но прежде чем постепенно увеличенное значение записывается обратно, вы видите неожиданные результаты.
Программа автоматического доказательства кода рассматривает все операции как неатомарные, если вы не защищаете их, например, при помощи критических разделов. Смотрите Задают Определенные Операции как Атомарные.
Bug Finder рассматривает операцию как неатомарную, если он может перевести больше чем в одну машинную команду. Например:
Операция может включить и операцию чтения и операцию записи. Например, var++ включает чтение значения var, увеличение значения одним и обратной записью увеличенного значения к var.
Операция может включить 64-битную переменную на 32-битной цели. Например, операция
long long var1, var2; var1=var2;
var2 к var1 на определенных целях.Polyspace использует размер Pointer для вашего Target processor type как порог, чтобы вычислить атомарность. Например, если вы используете i386 как ваш Target processor type, размер Pointer составляет 32 бита и Long long, и размеры Double - оба 64 бита. Поэтому Polyspace считает копирование того long long или double переменная другому как неатомарный.
См. также Target processor type (-target).
Операция может включить запись возвращаемого значения вызова функции к совместно используемой переменной. Например, операция x=func() включает вызов func и запись возвращаемого значения func к x.
Обнаружить данные мчится, где по крайней мере одна из двух операций прерывания является неатомарной, включите средству проверки Bug Finder Data race. Чтобы удалить это ограничение на средство проверки, включите Data race including atomic operations.
Вы можете хотеть задать группу операций как атомарную. Эта группа операций не может быть прервана операциями в другом потоке или задаче.
Используйте один из этих методов:
Критические разделы
Защитите группу операций с критическими разделами.
Критический раздел начинается и заканчивается вызовами определенных функций. Можно использовать предопределенный набор примитивов, чтобы начать или закончить критические разделы или использовать собственные функции.
Группа операций в критическом разделе является атомарной относительно другой группы операций, которые находятся в том же критическом разделе (то есть, имея то же начало и окончание функции).
Задайте критические разделы с помощью опции Critical section details (-critical-section-begin -critical-section-end) (Polyspace Code Prover).
Временно исключительные задачи
Защитите группу операций путем определения определенных задач как временно исключительный.
Если группа задач временно исключительна, все операции в одной задаче являются атомарными относительно операций в других задачах.
Задайте временное исключение с помощью опции Temporally exclusive tasks (-temporal-exclusions-file).
Приоритеты задач (только Bug Finder)
Защитите группу операций путем указывания, что определенные задачи имеют более высокие приоритеты. Например, прерывания имеют более высокие приоритеты над циклическими задачами.
Можно задать до четырех различных приоритетов с этими опциями (с самым высоким приоритетом, перечисленным сначала):
Все операции в задаче с более высоким приоритетом являются атомарными относительно операций в задачах с более низкими приоритетами. См. также Задают Прерывания Preemptable и Задачи Nonpreemptable.
Прерывания отключения стандартной программы (только Bug Finder)
Защитите группу операций путем отключения всех прерываний. Используйте опцию Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts).
После того, как вы вызываете стандартную программу, чтобы отключить прерывания, все последующие операции являются атомарными, пока вы не вызываете другую стандартную программу, чтобы повторно включить прерывания. Операции являются атомарными относительно операций во всех других задачах.
Для примера смотрите Меры защиты для Совместно используемых переменных в Многозадачном Коде.
Cyclic tasks (-cyclic-tasks) | Interrupts (-interrupts) | Temporally exclusive tasks (-temporal-exclusions-file) | Critical section details (-critical-section-begin -critical-section-end) (Polyspace Code Prover)