Bug Finder обнаруживает гонки данных между параллельными задачами. С помощью опций анализа Bug Finder можно исправить обнаружение гонки данных, указав, что некоторые задачи имеют более высокие приоритеты по сравнению с другими. Задача с более высоким приоритетом является атомной по отношению к задачам с более низким приоритетом и не может быть прервана этими задачами.
С помощью этих опций можно указать до четырех различных приоритетов (с первым перечисленным наивысшим приоритетом):
Прерывания (неразрушаемые): параметр «Использовать» Interrupts (-interrupts).
Прерывания (вытесняемые): Использовать параметры Interrupts (-interrupts) и -preemptable-interrupts.
Циклические задачи (неразрешимые): Использовать параметры Cyclic tasks (-cyclic-tasks)(сервер поиска ошибок Polyspace) и -non-preemptable-tasks(Сервер поиска ошибок Polyspace).
С помощью опции можно также определить вытесняемые нециклические задачи. Entry points (-entry-points) и -non-preemptable-tasks(Сервер поиска ошибок Polyspace).
Циклические задачи (вытесняемые): параметр «Использовать» Cyclic tasks (-cyclic-tasks)(Сервер поиска ошибок Polyspace).
С помощью опции можно также определить нециклические задачи. 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): Укажите task3 как циклическая задача.
Critical section details (-critical-section-begin -critical-section-end): Указать begin_critical_section как функция, начинающаяся с критического раздела и end_critical_section как функция, заканчивающая критическое сечение.
Запустить поиск ошибок.
Вы не видите гонки данных. С тех пор 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) | Cyclic tasks (-cyclic-tasks)(Сервер поиска ошибок Polyspace)