С 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: Задайте функции, которые имеют более низкий приоритет, чем прерывания, но более высокий приоритет, чем задачи (выгружаемый или non-preemptable).
Только анализ Bug Finder рассматривает приоритеты.
-non-preemptable-tasks: Задайте функции, которые имеют более высокий приоритет, чем задачи, но более низкий приоритет, чем прерывания (выгружаемый или non-preemptable).
Только анализ Bug Finder рассматривает приоритеты.
Многозадачный анализ в Программе автоматического доказательства Кода является более исчерпывающим о нахождении потенциально незащищенных совместно используемых переменных и поэтому следует строгой модели.
Задачами и прерываниями должны быть пустые пустотой функции.
Функции, которые вы задаете как задачи и прерывания, должны иметь прототип:
void func(void);
Предположим, что вы хотите задать функциональный func это берет int аргументы и имеют, возвращаются, вводят int:
int func(int);
func с энергозависимым значением. Задайте эту функцию обертки как задачу или прерывание.void func_wrapper() {
volatile int arg;
(void)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.
Все задачи и прерывания могут прервать друг друга.
Анализ 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();
}
}