Взаимоблокировка возникает, когда несколько задач застревают в их критических разделах (CS), потому что:

Polyspace^® ожидает, что критические разделы кода будут соответствовать определенному формату. Критический раздел находится между вызовом функции блокировки и вызовом функции разблокировки. Когда задача my_task вызывает функцию блокировки my_lock, другие задачи, вызывающие my_lock необходимо подождать до my_task вызывает соответствующую функцию разблокировки. Функции блокировки и разблокировки должны иметь форму void func(void).

Чтобы найти этот дефект, перед анализом необходимо задать опции многозадачности. Чтобы задать эти опции, на панели Configuration выберите Multitasking.

Каждая задача ожидает завершения критического раздела в другой задаче и не может продолжить. Программа может замерзнуть на неопределенный срок.

Исправление зависит от первопричины дефекта. Можно попытаться разбить циклический порядок между задачами одним из следующих способов:

Просмотр этого дефекта является возможностью проверить, все ли операции в вашем критическом разделе действительно предназначены для выполнения в качестве атомарного блока. Рекомендуется держать критические сечения на минимальном уровне.

Если вы не хотите устранять проблему, добавьте комментарии к своему результату или коду, чтобы избежать другой проверки. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.

void task1(void);
void task2(void);

int var;
void perform_task_cycle(void) {
 var++;
}

void begin_critical_section_1(void);
void end_critical_section_1(void);

void begin_critical_section_2(void);
void end_critical_section_2(void);

void task1() {
 while(1) {
    begin_critical_section_1();
    begin_critical_section_2();
    perform_task_cycle();
    end_critical_section_2();
    end_critical_section_1();
 } 
}

void task2() {
 while(1) {
    begin_critical_section_2();
    begin_critical_section_1();
    perform_task_cycle();
    end_critical_section_1();
    end_critical_section_2();
 } 
}

В этом примере, чтобы эмулировать поведение в многозадачном режиме, вы должны задать следующие опции:

Опция	Спецификация
Configure multitasking manually
Entry points	task1 task2
Critical section details	Starting routine	Ending routine
	begin_critical_section_1	end_critical_section_1
	begin_critical_section_2	end_critical_section_2

Deadlock происходит, потому что инструкции могут выполняться в следующей последовательности:

Одной из возможных коррекций является следование одной и той же последовательности вызовов для блокировки и разблокировки функций в обоих task1 и task2.

void task1(void);
void task2(void);
void perform_task_cycle(void);

void begin_critical_section_1(void);
void end_critical_section_1(void);

void begin_critical_section_2(void);
void end_critical_section_2(void);

void task1() {
 while(1) {
    begin_critical_section_1();
    begin_critical_section_2();
    perform_task_cycle();
    end_critical_section_2();
    end_critical_section_1();
 } 
}

void task2() {
 while(1) {
    begin_critical_section_1();
    begin_critical_section_2();
    perform_task_cycle();
    end_critical_section_2();
    end_critical_section_1();
 } 
}

int var;
void performTaskCycle() {
 var++;
}

void lock1(void);
void lock2(void);
void lock3(void);


void unlock1(void);
void unlock2(void);
void unlock3(void);

void task1() {
 while(1) {
    lock1();
    lock2();
    performTaskCycle();
    unlock2();
    unlock1();
 } 
}

void task2() {
 while(1) {
    lock2();
    lock3();
    performTaskCycle();
    unlock3();
    unlock2();
 } 
}

void task3() {
 while(1) {
    lock3();
    lock1();
    performTaskCycle();
    unlock1();
    unlock3();
 } 
}

В этом примере, чтобы эмулировать поведение в многозадачном режиме, вы должны задать следующие опции:

Опция	Спецификация
Configure multitasking manually
Entry points	task1 task2 task3
Critical section details	Starting routine	Ending routine
	lock1	unlock1
	lock2	unlock2
	lock3	unlock3

Deadlock происходит, потому что инструкции могут выполняться в следующей последовательности:

Чтобы разбить циклический порядок между критическими разделами, обратите внимание на каждую функцию блокировки в вашем коде в определенной последовательности, например:

Если вы используете в задаче несколько функций блокировки, используйте их в том порядке, в котором они появляются в последовательности. Для примера можно использовать lock1 далее следуют lock2 но не lock2 далее следуют lock1.

int var;
void performTaskCycle() {
 var++;
}

void lock1(void);
void lock2(void);
void lock3(void);

void unlock1(void);
void unlock2(void);
void unlock3(void);

void task1() {
 while(1) {
    lock1();
    lock2();
    performTaskCycle();
    unlock2();
    unlock1();
 } 
}

void task2() {
 while(1) {
    lock2();
    lock3();
    performTaskCycle();
    unlock3();
    unlock2();
 } 
}

void task3() {
 while(1) {
    lock1();
    lock3();
    performTaskCycle();
    unlock3();
    unlock1();
 } 
}