Bug Finder обнаруживает гонки данных между параллельными задачами. Используя опции анализа Bug Finder, можно зафиксировать обнаружение гонки данных путем указывания, что определенные задачи имеют более высокие приоритеты над другими. Задача с более высоким приоритетом является атомарной относительно задач с более низким приоритетом и не может быть прервана теми задачами.
Можно задать до четырех различных приоритетов с этими опциями (с самым высоким приоритетом, перечисленным сначала):
(nonpreemptable) прерывания: Используйте опцию Interrupts (-interrupts).
(Выгружаемые) прерывания: Используйте опции Interrupts (-interrupts) и -preemptable-interrupts.
Циклические (nonpreemptable) задачи: Используйте опции 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 nonpreemptable прерывания, к совместно используемой переменной нельзя получить доступ одновременно.
Измените task1 к выгружаемому прерыванию при помощи опции -preemptable-interrupts.
Запустите Bug Finder снова. Вы теперь видите, что данные мчатся на совместно используемой переменной var.
Измените этот пример следующими способами и смотрите эффект модификации:
Измените приоритеты task1 и task2.
Например, можно оставить task1 как nonpreemptable прерывание, но изменение 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)