С Polyspace® можно анализировать программы где несколько потоков, запущенных одновременно. Polyspace может анализировать ваш многозадачный код для гонок данных, мертвых блокировок и других дефектов параллелизма, если анализ знает о модели параллелизма в вашем коде. В некоторых ситуациях Polyspace может обнаружить создание потока и критические разделы в вашем коде автоматически. Средство поиска ошибки обнаруживает их по умолчанию. В Программе автоматического доказательства Кода вы включаете автоматическое обнаружение с помощью опции Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection).
Для многозадачного рабочего процесса анализа кода смотрите, Анализируют Многозадачные Программы в Polyspace.
Если ваша функция создания потока не обнаруживается автоматически:
Можно также сопоставить функцию с функцией создания потока, которую Polyspace может обнаружить автоматически. Используйте опцию -function-behavior-specifications.
В противном случае необходимо вручную смоделировать многозадачные потоки при помощи параметров конфигурации. Смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.
Polyspace может обнаружить создание потока и критические разделы, если вы используете примитивы от этих групп. Polyspace распознает вызовы этих стандартных программ как создание нового потока или как начало или конец критического раздела.
Создание потока: pthread_create
Критический раздел начинается: pthread_mutex_lock
Критические концы раздела: pthread_mutex_unlock
Создание потока: taskSpawn
Критический раздел начинается: semTake
Критические концы раздела: semGive
Чтобы активировать автоматическое обнаружение примитивов параллелизма для VxWorks®, в пользовательском интерфейсе десктопных решений Polyspace, используют шаблон VxWorks. Для получения дополнительной информации о шаблонах смотрите, Создают Проект Используя Шаблон конфигурации. В командной строке используйте эти опции:
-D1=CPU=I80386 -D2=__GNUC__=2 -D3=__OS_VXWORKS
Обнаружение параллелизма возможно, только если многозадачные функции создаются из точки входа под названием main. Если точка входа имеет другое имя, такое как vxworks_entry_point, выполнить одно из следующих действий:
Обеспечьте функцию main.
Preprocessor definitions (-D): В определениях препроцессора, набор vxworks_entry_point=main.
Создание потока: CreateThread
Критический раздел начинается: EnterCriticalSection
Критические концы раздела: LeaveCriticalSection
Создание потока: OSTaskCreate
Критический раздел начинается: OSMutexPend
Критические концы раздела: OSMutexPost
Создание потока: std::thread::thread
Критический раздел начинается: std::mutex::lock
Критические концы раздела: std::mutex::unlock
Для автоматического обнаружения C++ 11 потоков явным образом задайте пути к своим заголовочным файлам компилятора или используйте polyspace-configure.
Например, если вы используете std::thread для создания потока, явным образом задаете путь к папке, содержащей thread.h.
См. также Ограничения Автоматического Обнаружения Потока.
Создание потока: thrd_create
Критический раздел начинается: mtx_lock
Критические концы раздела: mtx_unlock
Следующие многозадачные модели кода пять философов, совместно использующих пять ветвлений. Пример использует стандартные программы создания потока POSIX® и иллюстрирует классический пример мертвой блокировки. Запустите Средство поиска Ошибки на этом коде, чтобы видеть мертвую блокировку.
#include "pthread.h"
#include <stdio.h>
#include <unistd.h>
pthread_mutex_t forks[5];
void* philo1(void* args)
{
while (1) {
printf("Philosopher 1 is thinking\n");
sleep(1);
pthread_mutex_lock(&forks[0]);
printf("Philosopher 1 takes left fork\n");
pthread_mutex_lock(&forks[1]);
printf("Philosopher 1 takes right fork\n");
printf("Philosopher 1 is eating\n");
sleep(1);
pthread_mutex_unlock(&forks[1]);
printf("Philosopher 1 puts down right fork\n");
pthread_mutex_unlock(&forks[0]);
printf("Philosopher 1 puts down left fork\n");
}
return NULL;
}
void* philo2(void* args)
{
while (1) {
printf("Philosopher 2 is thinking\n");
sleep(1);
pthread_mutex_lock(&forks[1]);
printf("Philosopher 2 takes left fork\n");
pthread_mutex_lock(&forks[2]);
printf("Philosopher 2 takes right fork\n");
printf("Philosopher 2 is eating\n");
sleep(1);
pthread_mutex_unlock(&forks[2]);
printf("Philosopher 2 puts down right fork\n");
pthread_mutex_unlock(&forks[1]);
printf("Philosopher 2 puts down left fork\n");
}
return NULL;
}
void* philo3(void* args)
{
while (1) {
printf("Philosopher 3 is thinking\n");
sleep(1);
pthread_mutex_lock(&forks[2]);
printf("Philosopher 3 takes left fork\n");
pthread_mutex_lock(&forks[3]);
printf("Philosopher 3 takes right fork\n");
printf("Philosopher 3 is eating\n");
sleep(1);
pthread_mutex_unlock(&forks[3]);
printf("Philosopher 3 puts down right fork\n");
pthread_mutex_unlock(&forks[2]);
printf("Philosopher 3 puts down left fork\n");
}
return NULL;
}
void* philo4(void* args)
{
while (1) {
printf("Philosopher 4 is thinking\n");
sleep(1);
pthread_mutex_lock(&forks[3]);
printf("Philosopher 4 takes left fork\n");
pthread_mutex_lock(&forks[4]);
printf("Philosopher 4 takes right fork\n");
printf("Philosopher 4 is eating\n");
sleep(1);
pthread_mutex_unlock(&forks[4]);
printf("Philosopher 4 puts down right fork\n");
pthread_mutex_unlock(&forks[3]);
printf("Philosopher 4 puts down left fork\n");
}
return NULL;
}
void* philo5(void* args)
{
while (1) {
printf("Philosopher 5 is thinking\n");
sleep(1);
pthread_mutex_lock(&forks[4]);
printf("Philosopher 5 takes left fork\n");
pthread_mutex_lock(&forks[0]);
printf("Philosopher 5 takes right fork\n");
printf("Philosopher 5 is eating\n");
sleep(1);
pthread_mutex_unlock(&forks[0]);
printf("Philosopher 5 puts down right fork\n");
pthread_mutex_unlock(&forks[4]);
printf("Philosopher 5 puts down left fork\n");
}
return NULL;
}
int main(void)
{
pthread_t ph[5];
pthread_create(&ph[0], NULL, philo1, NULL);
pthread_create(&ph[1], NULL, philo2, NULL);
pthread_create(&ph[2], NULL, philo3, NULL);
pthread_create(&ph[3], NULL, philo4, NULL);
pthread_create(&ph[4], NULL, philo5, NULL);
pthread_join(ph[0], NULL);
pthread_join(ph[1], NULL);
pthread_join(ph[2], NULL);
pthread_join(ph[3], NULL);
pthread_join(ph[4], NULL);
return 1;
} |
Каждому философу нужны два ветвления, чтобы поесть, право и левое ветвление. Функции philo1, philo2, philo3, philo4 и philo5 представляют философов. Каждая функция требует двух ресурсов pthread_mutex_t, представляя эти два ветвления, требуемые поесть. Все пять функций, запущенных одновременно в пяти параллельных потоках.
Однако мертвая блокировка происходит в этом примере. Когда каждый философ берет их первое ветвление (каждый поток блокирует один ресурс pthread_mutex_t), все ветвления используются. Так, философы (потоки) ожидают своего второго ветвления (второй ресурс pthread_mutex_t), чтобы стать доступными. Однако все ветвления (ресурсы) сохранены философами ожидания (потоки), вызвав мертвую блокировку.
Если вы используете функцию, такую как pthread_create(), чтобы создать новые потоки (задачи), каждый поток сопоставлен с уникальным идентификатором. Например, в этом примере, два потока создаются с идентификаторами id1 и id2.
pthread_t* id1, id2;
void main()
{
pthread_create(id1, NULL, start_routine, NULL);
pthread_create(id2, NULL, start_routine, NULL);
}Если гонка данных происходит между потоками, анализ может обнаружить ее. При отображении результатов потоки обозначаются как task_idid является идентификатором, сопоставленным с потоком. В предыдущем примере потоки идентифицированы как task_id1 и task_id2.
Если поток идентификаторы:
Локальный для функции, имя потока показывает функцию.
Например, поток, созданный ниже, появляется как task_f:id
void f(void)
{
pthread_t* id;
pthread_create(id, NULL, start_routine, NULL);
}Поле структуры, имя потока показывает структуру.
Например, поток, созданный ниже, появляется как task_a#id
struct {pthread_t* id; int x;} a;
pthread_create(a.id,NULL,start_routine,NULL);
Участник массивов, имя потока показывает массив.
Например, поток, созданный ниже, появляется как task_tab[1].
pthread_t* tab[10]; pthread_create(tab[1],NULL,start_routine,NULL);
Многозадачная модель, извлеченная Polyspace, не включает некоторые функции. Polyspace не может смоделировать:
Распараллельте приоритеты и атрибуты — Проигнорированный Polyspace.
Рекурсивные семафоры.
Неограниченные идентификаторы потока, такие как extern pthread_t ids[] — Предупреждение.
Вызовы параллелизма, примитивного через старшие вызовы — Предупреждение.
Псевдонимы на идентификаторах потока — Polyspace сверхаппроксимирует, когда псевдоним используется.
Завершение потоков — Polyspace игнорирует pthread_join и thrd_join. Polyspace заменяет pthread_exit и thrd_exit стандартным выходом.
(Только Polyspace Bug Finder™) Создание нескольких потоков через множественные вызовы той же функции с различными аргументами указателя.
(Только Polyspace Code Prover™), Разделяемые локальные переменные — Только глобальные переменные рассматриваются разделяемыми. Если к локальной переменной получают доступ несколько потоков, анализ не учитывает разделяемую природу переменной.
(Только Polyspace Code Prover), Разделяемая динамическая память — Только глобальные переменные рассматриваются разделяемыми. Если к динамически выделенной области памяти получают доступ несколько потоков, анализ не учитывает свой разделяемый характер.
Количество задач создало с CreateThread, когда threadId установлен в NULL — Когда вы создаете несколько потоков, которые выполняют ту же функцию, если последним аргументом CreateThread является NULL, Polyspace только обнаруживает один экземпляр этой функции или задачу.
(C++ 11 только), Если вы используете лямбда-выражения, как запускают функции во время создания потока, Polyspace, не обнаруживает совместно используемые переменные в лямбда-выражениях.
(C++ 11 потоков только с Polyspace Code Prover) Строковые литералы как аргумент функции потока — Программа автоматического доказательства Кода показывает красную ошибку Illegally dereferenced pointer, если функция потока имеет параметр std::string&, и вы передаете аргумент строкового литерала.
-function-behavior-specifications | Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)
