-critical-section-begin -critical-section-end)Задайте функции, которые начинают и заканчивают критические разделы
При проверке многозадачного кода 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();
}Используя ваши спецификации, верификация Программы автоматического доказательства Кода проверяет, разблокировало ли ваше размещение блокировки и функции, защищает все совместно используемые переменные от параллельного доступа. При определении значений тех переменных верификация составляет то, что критические разделы в различных задачах не прерывают друг друга.
Анализ Средства поиска Ошибки использует критическую информацию о разделе, чтобы искать дефекты параллелизма, такие как гонка данных и мертвая блокировка.
Никакое значение по умолчанию
Щелкните
, чтобы добавить поле.
В 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).
При рассмотрении возможных значений совместно используемых переменных верификация Программы автоматического доказательства Кода учитывает спецификации для критических разделов.
Однако, если совместно используемая переменная является указателем или массивом, программное обеспечение использует спецификации только, чтобы определить, является ли переменная разделяемой защищенной глобальной переменной. Для проверки ошибки времени выполнения программное обеспечение не принимает ваши спецификации во внимание и полагает, что к переменной можно одновременно получить доступ.
Параметр: -critical-section-begin | -critical-section-end |
| Никакое значение по умолчанию |
Значение: |
Пример (средство поиска ошибки):
|
Пример (программа автоматического доказательства кода): |
Пример (сервер средства поиска ошибки):
|
Пример (сервер программы автоматического доказательства кода):
|
-non-preemptable-tasks | -preemptable-interrupts | Cyclic tasks (-cyclic-tasks) | Interrupts (-interrupts) | Tasks (-entry-points) | Temporally exclusive tasks (-temporal-exclusions-file)