Отсутствие блокировки возникает, когда задача вызывает функцию разблокировки перед вызовом соответствующей функции блокировки.

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

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

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

Исправление зависит от первопричины дефекта. Например, если дефект возникает из-за несоответствия между функцией блокировки и функцией разблокировки, проверьте пару функция блокировки-разблокировки в конфигурации анализа Polyspace и исправьте несоответствие.

См. примеры исправлений ниже. Чтобы избежать проблемы, можно следовать практике вызова функций блокировки и разблокировки в одном модуле на одном уровне абстракции. Например, в этом примере func вызывает функцию блокировки и разблокировки на одном уровне, но func2 не делает.

void func() {
  my_lock();
  {
    // ...
  }
  my_unlock();
}

void func2() {
  {
   my_lock();
   // ...
  }
  my_unlock();
}

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

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset(void) 
{
  begin_critical_section();
  global_var = 0;
  end_critical_section();
}

void my_task(void)
{
  global_var += 1;
  end_critical_section();
}

В этом примере для эмуляции многозадачности необходимо указать следующие параметры.

Выбор	Спецификация
Настройка многозадачности вручную
Задачи	my_task, reset
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	begin_critical_section	end_critical_section

В командной строке можно использовать следующее:

polyspace-bug-finder
   -entry-points my_task,reset
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1

Пример имеет две точки входа, my_task и reset. my_task требования end_critical_section перед вызовом begin_critical_section.

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

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset(void) 
{
  begin_critical_section();
  global_var = 0;
  end_critical_section();
}

void my_task(void)
{
    begin_critical_section();
    global_var += 1;
    end_critical_section();
}

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset() {
    begin_critical_section();
    global_var=0;
    end_critical_section();
}

void my_task(void) {
    int index=0;
    volatile int numCycles;
    
    while(numCycles) {
      if(index%10==0) {
        begin_critical_section();
        global_var ++;  
      }
      end_critical_section(); 
      index++;
    }
}

В этом примере для эмуляции многозадачности необходимо указать следующие параметры.

Выбор	Спецификация
Настройка многозадачности вручную
Задачи	my_task, reset
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	begin_critical_section	end_critical_section

В командной строке можно использовать следующее:

polyspace-bug-finder
   -entry-points my_task,reset
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1

Пример имеет две точки входа, my_task и reset.

В while петля, my_task оставляет критический участок через вызов end_critical_section();. В итерации while цикл:

Поскольку numCycles является volatile переменная, она может принимать любое значение. Возможны любые из вышеуказанных случаев. Поэтому при вызове появляются дефект отсутствующей блокировки и дефект двойной разблокировки end_critical_section.

Отсутствие разблокировки происходит в следующих случаях:

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

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

Функция разблокировки заканчивает критический раздел, чтобы другие ожидающие задачи могли войти в критический раздел. Отсутствие функции разблокировки может привести к блокировке задач на ненужный период времени.

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

Могут быть и другие причины и соответствующие исправления дефекта. Возможно, вы назвали неправильную функцию разблокировки. Проверьте пару функций блокировки-разблокировки в конфигурации анализа Polyspace и устраните несоответствие.

См. примеры исправлений ниже. Чтобы избежать проблемы, можно следовать практике вызова функций блокировки и разблокировки в одном модуле на одном уровне абстракции. Например, в этом примере func вызывает функцию блокировки и разблокировки на одном уровне, но func2 не делает.

void func() {
  my_lock();
  {
    // ...
  }
  my_unlock();
}

void func2() {
  {
   my_lock();
   // ...
  }
  my_unlock();
}

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

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset() 
{
    begin_critical_section();
    global_var = 0;
    end_critical_section();
}

void my_task(void)
{
    begin_critical_section(); 
    global_var += 1;
}

В этом примере для эмуляции многозадачности задайте следующие параметры.

Выбор	Спецификация
Настройка многозадачности вручную
Задачи	my_task, reset
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	begin_critical_section	end_critical_section

В командной строке можно использовать следующее:

polyspace-bug-finder
   -entry-points my_task,reset
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1

Пример имеет две точки входа, my_task и reset. my_task входит в критический раздел через вызов begin_critical_section();. my_task заканчивается без вызова end_critical_section.

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

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset(void)
{
    begin_critical_section(); 
    global_var = 0;
    end_critical_section();
}

void my_task(void)
{
    begin_critical_section(); 
    global_var += 1;
    end_critical_section();
}

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset() {
    begin_critical_section();
    global_var=0;
    end_critical_section();
}

void my_task(void) {
    int index=0;
    volatile int numCycles;

    while(numCycles) {
      begin_critical_section();
      global_var ++;
      if(index%10==0) {
        global_var = 0;
        end_critical_section();
      }
      index++;
    }
}

В этом примере для эмуляции многозадачности задайте следующие параметры.

Выбор	Спецификация
Настройка многозадачности вручную
Задачи	my_task, reset
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	begin_critical_section	end_critical_section

В командной строке можно использовать следующее:

polyspace-bug-finder
   -entry-points my_task,reset
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1

Пример имеет две точки входа, my_task и reset.

В while петля, my_task входит в критический раздел через вызов begin_critical_section();. В итерации while цикл:

Поскольку numCycles является volatile переменная, она может принимать любое значение. Возможен любой из вышеуказанных случаев. Поэтому при вызове появляются дефект «Missing unlock» и дефект «Double lock» begin_critical_section.

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

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset() {
    begin_critical_section();
    global_var=0;
    end_critical_section();
}

void my_task(void) {
    int index=0;
    volatile int numCycles;

    while(numCycles) {
      begin_critical_section();
      global_var ++;
      if(index%10==0) {
        global_var=0;
      }
      end_critical_section();
      index++;
    }
}

Другой возможной поправкой является вызов функции разблокировки. end_critical_section во всех ветвях if состояние.

void begin_critical_section(void);
void end_critical_section(void);

int global_var;

void reset() {
    begin_critical_section();
    global_var=0;
    end_critical_section();
}

void my_task(void) {
    int index=0;
    volatile int numCycles;

    while(numCycles) {
      begin_critical_section();
      global_var ++;
      if(index%10==0) {
        global_var=0;
        end_critical_section();
      }
      else
        end_critical_section();
      index++;
    }
}

Двойная блокировка происходит в следующих случаях:

В многозадачном коде функция блокировки начинает критический раздел кода и функция разблокировки заканчивает его. Когда задача task1 вызывает функцию блокировки lock, другие задачи, вызывающие lock должен подождать до task вызывает соответствующую функцию разблокировки. Polyspace требует, чтобы функции блокировки и разблокировки имели вид void func(void).

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

Вызов функции блокировки начинает критический раздел, так что другие задачи должны ждать, чтобы войти в тот же критический раздел. Если та же самая функция блокировки вызывается снова в критическом разделе, задача блокируется сама собой.

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

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

См. примеры исправлений ниже. Чтобы избежать проблемы, можно следовать практике вызова функций блокировки и разблокировки в одном модуле на одном уровне абстракции. Например, в этом примере func вызывает функцию блокировки и разблокировки на одном уровне, но func2 не делает.

void func() {
  my_lock();
  {
    // ...
  }
  my_unlock();
}

void func2() {
  {
   my_lock();
   // ...
  }
  my_unlock();
}

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

int global_var;

void lock(void);
void unlock(void);

void task1(void)
{
    lock();
    global_var += 1;
    lock(); 
    global_var += 1;
    unlock();
}

void task2(void)
{
    lock(); 
    global_var += 1;
    unlock();
}

В этом примере для эмуляции многозадачности необходимо указать следующие параметры.

Выбор	Спецификация
Настройка многозадачности вручную
Задачи	my_task, reset
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	lock	unlock

В командной строке можно использовать следующее:

 polyspace-bug-finder
   -entry-points task1,task2
   -critical-section-begin lock:cs1
   -critical-section-end unlock:cs1

task1 входит в критический раздел через вызов lock();. task1 требования lock перед тем, как он покинет критический участок через вызов unlock();.

Если вы хотите первый global_var+=1; чтобы находиться вне критического раздела, одной из возможных корректировок является удаление первого вызова lock. Однако, если используются другие задачи global_var, этот код может создать Data race ошибка.

int global_var;

void lock(void);
void unlock(void);

void task1(void)
{
    global_var += 1;
    lock(); 
    global_var += 1;
    unlock();
}

void task2(void)
{
    lock(); 
    global_var += 1;
    unlock();
}

Если вы хотите первый global_var+=1; чтобы быть внутри критического раздела, одной из возможных корректировок является удаление второго вызова lock.

int global_var;

void lock(void);
void unlock(void);

void task1(void)
{
    lock();
    global_var += 1;
    global_var += 1;
    unlock();
}

void task2(void)
{
    lock(); 
    global_var += 1;
    unlock();
}

Если вы хотите второй global_var+=1; чтобы быть внутри критического раздела, другая возможная коррекция состоит в добавлении другого вызова unlock.

int global_var;

void lock(void);
void unlock(void);

void task1(void)
{
    lock();
    global_var += 1;
    unlock();
    lock();
    global_var += 1;
    unlock();
}

void task2(void)
{
    lock(); 
    global_var += 1;
    unlock();
}

int global_var;

void lock(void);
void unlock(void);

void performOperation(void) {
  lock();
  global_var++;
}

void task1(void)
{
    lock();
    global_var += 1;
    performOperation();
    unlock();
}

void task2(void)
{
    lock(); 
    global_var += 1;
    unlock();
}

В этом примере для эмуляции многозадачности необходимо указать следующие параметры.

Выбор	Спецификация
Настройка многозадачности вручную
Задачи	my_task, reset
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	lock	unlock

В командной строке можно использовать следующее:

 polyspace-bug-finder
   -entry-points task1,task2
   -critical-section-begin lock:cs1
   -critical-section-end unlock:cs1

task1 входит в критический раздел через вызов lock();. task1 вызывает функцию performOperation. В performOperation, lock вызывается снова, даже если task1 не покинул критический участок через вызов unlock();.

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

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

Одной из возможных корректировок является удаление вызова для lock в task1.

int global_var;

void lock(void);
void unlock(void);

void performOperation(void) {
  global_var++;
}

void task1(void)
{
    lock();
    global_var += 1;
    performOperation();
    unlock();
}

void task2(void)
{
    lock(); 
    global_var += 1;
    unlock();
}

Двойная разблокировка происходит в следующих случаях:

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

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

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

Исправление зависит от первопричины дефекта.

Определите каждый критический раздел кода, то есть раздел, который требуется выполнить как атомарный блок. Вызовите функцию блокировки в начале раздела. Только в конце раздела вызовите функцию разблокировки, соответствующую функции блокировки. Удалите любой другой резервный вызов функции разблокировки.

См. примеры исправлений ниже. Чтобы избежать проблемы, можно следовать практике вызова функций блокировки и разблокировки в одном модуле на одном уровне абстракции. Например, в этом примере func вызывает функцию блокировки и разблокировки на одном уровне, но func2 не делает.

void func() {
  my_lock();
  {
    // ...
  }
  my_unlock();
}

void func2() {
  {
   my_lock();
   // ...
  }
  my_unlock();
}

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

int global_var;

void BEGIN_CRITICAL_SECTION(void);
void END_CRITICAL_SECTION(void);

void task1(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
}

void task2(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
}

В этом примере для эмуляции многозадачности необходимо указать следующие параметры.

Выбор	Стоимость
Настройка многозадачности вручную
Задачи	task1 task2
Детали критического раздела	Запуск подпрограммы	Завершение процедуры
	BEGIN_CRITICAL_SECTION	END_CRITICAL_SECTION

В командной строке можно использовать следующее:

 polyspace-bug-finder
   -entry-points task1,task2
   -critical-section-begin BEGIN_CRITICAL_SECTION:cs1
   -critical-section-end END_CRITICAL_SECTION:cs1

task1 входит в критический раздел через вызов BEGIN_CRITICAL_SECTION();. task1 оставляет критический раздел через вызов END_CRITICAL_SECTION();. task1 требования END_CRITICAL_SECTION снова без промежуточного вызова BEGIN_CRITICAL_SECTION.

Если вы хотите второй global_var+=1; чтобы находиться вне критического раздела, одной из возможных корректировок является удаление второго вызова END_CRITICAL_SECTION. Однако, если используются другие задачи global_var, этот код может создать Data race ошибка.

int global_var;

void BEGIN_CRITICAL_SECTION(void);
void END_CRITICAL_SECTION(void);

void task1(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
    global_var += 1;
}

void task2(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
}

Если вы хотите второй global_var+=1; чтобы быть внутри критического раздела, одной из возможных корректировок является удаление первого вызова END_CRITICAL_SECTION.

int global_var;

void BEGIN_CRITICAL_SECTION(void);
void END_CRITICAL_SECTION(void);

void task1(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    global_var += 1;
    END_CRITICAL_SECTION();
}

void task2(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
}

Если вы хотите второй global_var+=1; чтобы быть внутри критического раздела, другая возможная коррекция состоит в добавлении другого вызова BEGIN_CRITICAL_SECTION.

int global_var;

void BEGIN_CRITICAL_SECTION(void);
void END_CRITICAL_SECTION(void);

void task1(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
}

void task2(void)
{
    BEGIN_CRITICAL_SECTION();
    global_var += 1;
    END_CRITICAL_SECTION();
}