С помощью Polyspace ® можно анализировать программы, в которых одновременно выполняется несколько потоков. Polyspace может анализировать многозадачный код на предмет поиска данных, взаимоблокировок и других дефектов параллелизма, если анализ знает модель параллелизма в коде. В некоторых ситуациях Polyspace может автоматически обнаруживать создание потоков и критические разделы в коде. Функция поиска ошибок обнаруживает их по умолчанию. В программе Code Prover автоматическое обнаружение включается с помощью опцииEnable automatic concurrency detection for Code Prover (-enable-concurrency-detection).
Рабочий процесс анализа многозадачного кода см. в разделе Анализ многозадачных программ в многозадачном пространстве.
Если функция создания потока не обнаружена автоматически:
Можно также сопоставить функцию с функцией создания потоков, которую Polyspace может обнаружить автоматически. Использовать опцию -code-behavior-specifications.
В противном случае необходимо вручную моделировать многозадачные потоки с помощью опций конфигурации. См. раздел Настройка многозадачного анализа в многозадачном пространстве вручную.
При использовании примитивов из этих групп полиспейс может обнаруживать создание потоков и критические сечения. 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): В определениях препроцессора, set 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); |
Если создаются два потока с различными идентификаторами потоков, но для идентификаторов потоков используется одно и то же имя локальной переменной, имя второго потока изменяется, чтобы отличить его от первого потока. Например, перечисленные ниже потоки отображаются как task_func:id и task_func:id:1.
void func()
{
{
pthread_t id;
pthread_create(&id, NULL, &task, NULL);
}
{
pthread_t id;
pthread_create(&id, NULL, &task, NULL);
}
} |
Многозадачная модель, извлеченная Polyspace, не включает некоторые функции. Полиспейс не может моделировать:
Приоритеты и атрибуты потоков - игнорируются Polyspace.
Рекурсивные семафоры.
Неограниченные идентификаторы потоков, такие как extern pthread_t ids[] - Предупреждение.
Вызовы примитива параллелизма через вызовы высокого порядка - предупреждение.
Псевдонимы на идентификаторах потоков (Aliases on thread identifiers) - сверхаппроксимация полипространства при использовании псевдонима.
Завершение потоков - Polyspace игнорирует pthread_join и thrd_join. Polyspace заменяет pthread_exit и thrd_exit стандартным выходом.
(Только ошибка Polyspace Finder™) Создание нескольких потоков с помощью нескольких вызовов одной и той же функции с разными аргументами указателя.
(Только Prover™ кода Polyspace) Общие локальные переменные - общими считаются только глобальные переменные. Если доступ к локальной переменной осуществляется несколькими потоками, анализ не учитывает общий характер переменной.
(Только средство проверки кода Polyspace) Общая динамическая память - общими считаются только глобальные переменные. Если динамически выделенная область памяти доступна нескольким потокам, анализ не учитывает ее общий характер.
Количество задач, созданных с помощью CreateThread когда threadId имеет значение NULL- При создании нескольких потоков, выполняющих одну и ту же функцию, если последний аргумент CreateThread является NULL, Polyspace обнаруживает только один экземпляр этой функции или задачи.
(Только C++ 11) Если лямбда-выражения используются в качестве функций запуска при создании потока, Polyspace не обнаруживает общие переменные в лямбда-выражениях.
(Только потоки C++ 11 с проверкой кода Polyspace) Строковые литералы в качестве аргумента функции потока - Функция проверки кода показывает ошибку указателя «Незаконно» красного цвета, если функция потока имеет std::string& и передается строковый литеральный аргумент.
-code-behavior-specifications | Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)
