С 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): Задайте функции, которые отключают и повторно включают прерывания (Только Средство поиска ошибки).
Critical section details (-critical-section-begin -critical-section-end): Задайте функции, которые начинают и заканчивают критические разделы.
Temporally exclusive tasks (-temporal-exclusions-file): Задайте группы функций, которые временно исключительны.
-preemptable-interrupts: Задайте функции, которые имеют более низкий приоритет, чем прерывания, но более высокий приоритет, чем задачи (выгружаемый или non-preemptable).
Только анализ Средства поиска Ошибки рассматривает приоритеты.
-non-preemptable-tasks: Задайте функции, которые имеют более высокий приоритет, чем задачи, но более низкий приоритет, чем прерывания (выгружаемый или non-preemptable).
Только анализ Средства поиска Ошибки рассматривает приоритеты.
Многозадачный анализ в Программе автоматического доказательства Кода является более исчерпывающим о нахождении потенциально незащищенных совместно используемых переменных и поэтому следует строгой модели.
Задачами и прерываниями должны быть пустые пустотой функции.
Функции, которые вы задаете как задачи и прерывания, должны иметь прототип:
void func(void);
Предположим, что вы хотите задать функциональный func, который берет аргументы int:
void func(int);
func с энергозависимым значением. Задайте эту функцию обертки как задачу или прерывание.void func_wrapper() {
volatile int arg;
func(arg);
}
Функция main должна закончиться.
Программа автоматического доказательства кода принимает, что концы функции main перед всеми задачами и прерываниями начинаются. Если функция main содержит бесконечный цикл или ошибку времени выполнения, задачи и прерывания не анализируются. Если вы видите, что нет никаких регистраций ваших задач и прерываний, не ищут лексему, подчеркнутую в пунктирном красном, чтобы идентифицировать проблему в функции main. Видьте Основания для Кода Непроверенного (Polyspace Code Prover).
Предположим, что вы хотите задать функцию 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.
Все задачи и прерывания могут прервать друг друга.
Анализ Средства поиска Ошибки рассматривает приоритеты задач. Функция, которую вы задаете как задача, не может прервать функцию, которую вы задаете как прерывание, потому что прерывание имеет более высокий приоритет.
Анализ Программы автоматического доказательства Кода полагает, что все задачи и прерывания могут прервать друг друга.
Все задачи и прерывания могут запустить любое число раз в любой последовательности.
Анализ Программы автоматического доказательства Кода полагает, что все задачи и прерывания могут запустить любое число раз в любой последовательности.
Предположим в этом примере, вы задаете 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();
}
}