Bug Finder обнаруживает гонки данных между параллельными задачами. Используя опции анализа Bug Finder, можно исправить обнаружение гонки данных, указав, что определенные задачи имеют более высокие приоритеты по сравнению с другими. Задача с более высоким приоритетом является атомарной относительно задач с более низким приоритетом и не может быть прервана этими задачами.
Вы можете задать до четырех различных приоритетов с этими опциями (с наивысшим приоритетом, перечисленным первым):
Прерывания (незапускаемые): Используйте опцию Interrupts (-interrupts).
Прерывания (предварительно): Используйте опции Interrupts (-interrupts) и -preemptable-interrupts.
Циклические задачи (незапускаемые): Используйте опции Cyclic tasks (-cyclic-tasks) (Polyspace Bug Finder Server) и -non-preemptable-tasks (Polyspace Bug Finder Server).
Можно также задать предпусковые нециклические задачи с помощью опции Entry points (-entry-points) и -non-preemptable-tasks (Polyspace Bug Finder Server).
Циклические задачи (предварительно): Используйте опцию Cyclic tasks (-cyclic-tasks) (Polyspace Bug Finder Server).
Можно также задать нециклические задачи с помощью опции Entry points (-entry-points).
Для образца прерывания имеют наивысший приоритет и не могут быть вытеснены другими задачами. Чтобы определить класс прерываний, которые могут быть упреждены, уменьшите их приоритет, сделав их предопущенными.
Рассмотрим этот пример с тремя задачами. Переменная var совместно используется между этими двумя задачами task1 и task2 без какой-либо защиты, такой как критический раздел. В зависимости от приоритетов task1 и task2, Bug Finder показывает гонку данных. Третья задача не релевантна для примера (и добавляется только для включения критического раздела, в противном случае обнаружение гонки данных отключено).
int var;
void begin_critical_section(void);
void end_critical_section(void);
void task1(void) {
var++;
}
void task2(void) {
var=0;
}
void task3(void){
begin_critical_section();
/* Some atomic operation */
end_critical_section();
}Скорректируйте приоритеты task1 и task2 и увидеть, обнаружена ли гонка данных. Для образца:
Сконфигурируйте следующие опции многозадачности:
Interrupts (-interrupts): Задайте task1 и task2 как прерывания.
Cyclic tasks (-cyclic-tasks) (Polyspace Bug Finder Server): Укажите task3 как циклическая задача.
Critical section details (-critical-section-begin -critical-section-end): Задайте begin_critical_section как функция, начинающаяся с критического сечения и end_critical_section как функция, заканчивающая критический раздел.
Запустите Bug Finder.
Вы не видите гонки данных. Начиная с task1 и task2 являются прерываниями без предварительной очистки, доступ к общей переменной невозможен одновременно.
Изменение task1 на предпусконаладочное прерывание при помощи опции -preemptable-interrupts.
Еще раз запустите Bug Finder. Теперь вы видите гонку данных на общей переменной var.
Измените этот пример следующими способами и увидите эффект изменения:
Изменение приоритетов task1 и task2.
Например, можно уйти task1 как непередаваемое прерывание, но изменение task2 на предпусконаладочное прерывание при помощи опции -preemptable-interrupts.
Гонка данных исчезает. Причина в следующем:
task1 имеет более высокий приоритет и не может быть прерван task2.
Операция в task2 является атомарным и не может быть прерван task1.
Включите шашку Data race including atomic operations (не включен по умолчанию). Используйте опцию Find defects (-checkers).
Вы снова видите гонку данных. Шашка рассматривает все операции как потенциально неатомные и операцию в task2 теперь можно прервать из-за операции с более высоким приоритетом в task1.
Попробуйте другие изменения опций анализа и посмотрите результат проверки.
-preemptable-interrupts | Interrupts (-interrupts) | -non-preemptable-tasks (Polyspace Bug Finder Server) | Cyclic tasks (-cyclic-tasks) (Polyspace Bug Finder Server)