В коде с несколькими потоками можно использовать Polyspace® Bug Finder™, чтобы обнаружить гонки данных или Polyspace Code Prover™ чтобы отобразить потенциально незащищенные общие переменные.
Чтобы определить, защищена ли переменная, разделяемая несколькими потоками, от параллельного доступа, Polyspace проверяет, являются ли операции с переменной атомарными.
Если операция неатомна, Polyspace считает, что операция включает несколько шагов. Эти шаги не должны происходить вместе и могут быть прерваны операциями в других потоках.
Например, рассмотрим эти две операции в двух разных потоках:
Поток 1: var++;
Эта операция неатомна, потому что она происходит в три этапа: чтение var, увеличение varи запись назад var.
Поток 2: var = 0;
Эта операция является атомарной, если размер var меньше, чем размер слова на целевом объекте. Подробнее о том, как Polyspace определяет размер слова, см. ниже.
Если две операции не защищены (при помощи, для образца, критических секций), операция во втором потоке может прервать операцию в первом потоке. Если прерывание происходит после var увеличивается в первом потоке, но перед тем, как пошаговое значение будет записано назад, можно увидеть неожиданные результаты.
Code Prover рассматривает все операции как неатомные, если вы не защищаете их, например, с помощью критических разделов. Смотрите Определение конкретных операций как Atomic.
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)
Защитите группу операций, указав, что определенные задачи имеют более высокие приоритеты. Для образца прерывания имеют более высокие приоритеты по сравнению с циклическими задачами.
Вы можете задать до четырех различных приоритетов с этими опциями (с наивысшим приоритетом, перечисленным первым):
Все операции в задаче с более высоким приоритетом являются атомарными по отношению к операциям в задачах с более низкими приоритетами. Смотрите также «Определение предопределяемых прерываний и незапускаемых задач».
Рутинное отключение прерываний (только для 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)