С помощью Polyspace ® можно анализировать программы, в которых одновременно выполняется несколько потоков. В некоторых ситуациях Polyspace может автоматически обнаруживать создание потоков и критические разделы в коде. См. раздел Автоматическое обнаружение создания резьбы и критического сечения в Polyspace.
Если код имеет функции, предназначенные для параллельного выполнения, но не могут быть обнаружены автоматически, их необходимо указать перед анализом. Если эти функции работают с общей переменной, необходимо также указать механизмы защиты для этих операций.
Рабочий процесс анализа многозадачного кода см. в разделе Анализ многозадачных программ в многозадачном пространстве.
Используйте эти параметры, чтобы указать циклические задачи, прерывания и защиты для общих переменных. В интерфейсе пользователя Polyspace эти параметры находятся в узле Многозадачность на панели Конфигурация.
Entry points (-entry-points): Укажите нециклические функции точек входа.
Не указывать main. Polyspace неявно рассматривает main в качестве функции точки входа.
Cyclic tasks (-cyclic-tasks)Укажите функции, которые планируются с периодическими интервалами.
Interrupts (-interrupts): Укажите функции, которые могут выполняться асинхронно.
Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts): Укажите функции, которые отключают и повторно включают прерывания (только для поиска ошибок).
Critical section details (-critical-section-begin -critical-section-end): Укажите функции, начинающие и завершающие критические сечения.
Temporally exclusive tasks (-temporal-exclusions-file): Укажите группы функций, которые являются исключительными по времени.
-preemptable-interrupts: Укажите функции, которые имеют более низкий приоритет, чем прерывания, но более высокий приоритет, чем задачи (вытесняемые или неразрушаемые).
Только анализ Bug Finder учитывает приоритеты.
-non-preemptable-tasks: Укажите функции, которые имеют более высокий приоритет, чем задачи, но более низкий приоритет, чем прерывания (вытесняемые или неразрушаемые).
Только анализ Bug Finder учитывает приоритеты.
Многозадачный анализ в Code Prover является более исчерпывающим для поиска потенциально незащищенных общих переменных и поэтому следует строгой модели.
Задачи и прерывания должны быть функциями void-void.
Функции, указанные как задачи и прерывания, должны иметь прототип:
void func(void);
Предположим, что требуется указать функцию func для этого требуется int аргументы и имеет возвращаемый тип int:
int func(int);
func с изменчивым значением. Укажите эту функцию оболочки как задачу или прерывание.void func_wrapper() {
volatile int arg;
(void)func(arg);
}
main функция должна закончиться.
Средство проверки кода предполагает, что main функция заканчивается до начала выполнения всех задач и прерываний. Если main функция содержит бесконечный цикл или ошибку времени выполнения, задачи и прерывания не анализируются. Если вы видите, что в ваших задачах нет проверок и прерываний, найдите маркер, подчеркнутый пунктиром, чтобы идентифицировать проблему в main функция. См. раздел Причины снятия флажка с кода (средство проверки кода Polyspace).
Предположим, что необходимо указать main функция в качестве циклической задачи.
void performTask1Cycle(void);
void performTask2Cycle(void);
void main() {
while(1) {
performTask1Cycle();
}
}
void task2() {
while(1) {
performTask2Cycle();
}
}Заменить определение main с:
#ifdef POLYSPACE
void main() {
}
void task1() {
while(1) {
performTask1Cycle();
}
}
#else
void main() {
while(1) {
performTask1Cycle();
}
}
#endifmain и размещает содержание main в другую функцию task1 если макрос POLYSPACE определяется. Определение макроса POLYSPACE использование опции Preprocessor definitions (-D) и указать task1 для опции Tasks (-entry-points).Это предположение не применяется к автоматически обнаруженным потокам. Например, main функция может создавать потоки с помощью pthread_create.
Все задачи и прерывания могут прерывать друг друга.
В анализе Bug Finder рассматриваются приоритеты задач. Функция, указанная как задача, не может прерывать функцию, указанную как прерывание, поскольку прерывание имеет более высокий приоритет.
Анализ проверки кода считает, что все задачи и прерывания могут прерывать друг друга.
Многозадачный анализ Polyspace предполагает, что задача или прерывание не могут прервать себя.
Все задачи и прерывания могут выполняться любое количество раз в любой последовательности.
Анализ проверки кода считает, что все задачи и прерывания могут выполняться любое количество раз в любой последовательности.
Предположим, в этом примере вы указываете reset и inc как циклические задачи. Анализ показывает переполнение операции var+=2.
void reset(void) {
var=0;
}
void inc(void) {
var+=2;
}
Предположим, что вы хотите смоделировать планирование задач таким образом, что reset выполняется после inc исполнял пять раз. Запишите функцию-оболочку, реализующую эту последовательность. Укажите эту новую функцию как циклическую задачу, а не reset и inc.
void task() {
volatile int randomValue = 0;
while(randomValue) {
inc();
inc();
inc();
inc();
inc();
reset();
}
}Предположим, что вы хотите смоделировать планирование задач таким образом, что reset выполняется после inc выполнил от нуля до пяти раз. Запишите функцию-оболочку, реализующую эту последовательность. Укажите эту новую функцию как циклическую задачу, а не reset и inc.
void task() {
volatile int randomValue = 0;
while(randomValue) {
if(randomValue)
inc();
if(randomValue)
inc();
if(randomValue)
inc();
if(randomValue)
inc();
if(randomValue)
inc();
reset();
}
}