Exponenta Banner

Critical section details (-critical-section-begin -critical-section-end)

Задайте функции, которые начинают и заканчивают критические сечения

Описание

Эта опция недоступна для кода, сгенерированного из MATLAB® код или Simulink® модели.

При проверке многозадачного кода Polyspace® считает, что критический раздел лежит между вызовами функции блокировки и функцией разблокировки. 

lock();
/* Critical section code */
unlock();
Задайте имена функции блокировки и разблокировки для критических сечений (для образца, lock() и unlock() в приведенном выше примере).

Задать опцию

Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Multitasking. Смотрите Зависимости для других опций, которые вы также должны включить.

Командная строка и файл опций: Используйте опцию -critical-section-begin и -critical-section-end. См. «Информация о командной строке».

Зачем использовать эту опцию

Когда задача my_task вызывает функцию блокировки my_lock, другие задачи, вызывающие my_lock необходимо подождать до my_task вызывает соответствующую функцию разблокировки. Поэтому операции критического разреза в других задачах не могут прервать операции критического разреза в my_task.

Например, операция var++ в my_task1 и my_task2 невозможно прервать друг друга.

int var;

void my_task1() {
   my_lock();
   var++;
   my_unlock();
}

void my_task2() {
   my_lock();
   var++; 
   my_unlock();
}

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

Анализ Bug Finder использует информацию критического раздела для поиска дефектов параллелизма, таких как гонка данных и взаимоблокировка.

Настройки

По умолчанию нет

Щелкните, чтобы добавить поле.

  • В Starting routine введите имя функции блокировки.

  • В Ending routine введите имя функции разблокировки.

Введите имена функции или выберите из списка.

  • Щелкните, чтобы добавить поле и ввести имя функции.

  • Щелкните, чтобы отобразить функции в коде. Выберите функции из списка.

Зависимости

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

Совет

  • Можно также использовать примитивы, такие как POSIX® функции pthread_mutex_lock и pthread_mutex_unlock чтобы начать и закончить критические участки. Список примитивов, которые Polyspace может обнаружить автоматически, см. в разделах Автоматическое обнаружение создания потоков и Критическое сечение в Polyspace.

  • Для вызовов функций, которые начинают и заканчивают критические разделы, Polyspace игнорирует аргументы функции.

    Для образца Polyspace рассматривает две секции кода ниже как один и тот же критический раздел.

    Starting routine: my_lock
    Ending routine: my_unlock
    void my_task1() {
   my_lock(1);
   /* Critical section code */
   my_unlock(1);
}
    		 
    void my_task2() {
   my_lock(2);
   /* Critical section code */
   my_unlock(2);
}

    Для работы с ограничением смотрите Задать критические разделы с функциями, которые берут аргументы.

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

    #define init() num_locks++
    Вы не можете использовать макрос init() чтобы начать или завершить критический раздел.

  • Когда вы используете несколько критических разделов, можно столкнуться с такими проблемами, как:

    • Тупик: Последовательность вызовов функций блокировки заставляет две задачи блокировать друг друга.

    • Двойная блокировка: Функция блокировки вызывается дважды в задаче без промежуточного вызова функции разблокировки.

    Используйте Polyspace Bug Finder™, чтобы обнаружить такие проблемы. См. «Дефекты параллелизма».

    Затем используйте Polyspace Code Prover™, чтобы обнаружить, действительно ли ваше размещение функций блокировки и разблокировки защищает все общие переменные от параллельного доступа. См. «Глобальные переменные» (Polyspace Code Prover).

  • При рассмотрении возможных значений общих переменных верификация Code Prover учитывает ваши спецификации для критических разделов.

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

Информация о командной строке

Параметр: -critical-section-begin | -critical-section-end
По умолчанию нет
Значение: function1:cs1 [function2:cs2 [...]]
Пример (Bug Finder): polyspace-bug_finder -sources file_name -критически-сечение-начало func_begin:cs1 -критически-сечение-конец func_end:cs1
Пример (Code Prover): Polyspace Code Prover -sources file_name -критически-сечение-начало func_begin:cs1 -критически-сечение-конец func_end:cs1
Пример (Bug Finder Server): polyspace-bug_finder-server -sources file_name -критически-сечение-начало func_begin:cs1 -критически-сечение-конец func_end:cs1
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -критически-сечение-начало func_begin:cs1 -критически-сечение-конец func_end:cs1

См. также

| | | | |

Темы

Документация Polyspace Bug Finder

Поддержка