С Polyspace®можно анализировать программы, где несколько потоков выполняются одновременно. В некоторых ситуациях Polyspace может автоматически обнаруживать создание потоков и критические разделы в вашем коде. Смотрите раздел «Автоматическое обнаружение создания резьбы и критического сечения» в Polyspace.
Если ваш код имеет функции, которые предназначены для параллельного выполнения, но которые не могут быть обнаружены автоматически, вы должны задать их перед анализом. Если эти функции работают с общей переменной, необходимо также задать механизмы защиты для этих операций.
Рабочий процесс анализа многозадачного кода см. в разделе Анализ многозадачных программ в Polyspace.
Используйте эти опции, чтобы задать циклические задачи, прерывания и защиты для общих переменных. В пользовательском интерфейсе Polyspace опции находятся на узле Multitasking в панели Configuration.
Entry points (-entry-points): Задайте нециклические функции точки входа.
Не указывайте main. Polyspace неявно рассматривает main как функцию точки входа.
Cyclic tasks (-cyclic-tasks): Задайте функции, которые запланированы через периодические интервалы.
Interrupts (-interrupts): Задайте функции, которые могут выполняться асинхронно.
Disabling all interrupts (-routine-disable-interrupts -routine-enable-interrupts): Укажите функции, которые отключают и повторяют прерывания (только для Bug Finder).
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 func(void);
Предположим, вы хотите задать функцию func который принимает int аргументы и имеет тип возврата int:
int func(int);
func с летучим значением. Задайте эту функцию оболочки как задачу или прерывание.void func_wrapper() {
volatile int arg;
(void)func(arg);
}
The main функция должна заканчиваться.
Code Prover принимает, что main функция заканчивается до начала всех задач и прерываний. Если на main функция содержит бесконечный цикл или ошибку времени выполнения, задачи и прерывания не анализируются. Если вы видите, что в ваших задачах нет проверок и прерываний, найдите лексему, подчеркнутый штриховым красным цветом, чтобы идентифицировать проблему в main функция. См. раздел Причины снятия проверки кода.
Предположим, вы хотите задать 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).Это предположение не применяется к автоматически обнаруженным потокам. Для образца, a main функция может создавать потоки, используя pthread_create.
Все задачи и прерывания могут прервать друг друга.
Анализ Bug Finder рассматривает приоритеты задач. Функция, которую вы задаете как задачу, не может прервать функцию, которую вы задаете как прерывание, потому что прерывание имеет более высокий приоритет.
Анализ Code Prover считает, что все задачи и прерывания могут прерывать друг друга.
Многозадачный анализ Polyspace принимает, что задача или прерывание не могут прервать себя.
Все задачи и прерывания могут выполняться любое количество раз в любой последовательности.
Анализ Code Prover считает, что все задачи и прерывания могут запускаться любое количество раз в любой последовательности.
Предположим, в этом примере вы задаете 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();
}
}