С Polyspace®можно анализировать программы, где несколько потоков выполняются одновременно. Polyspace может анализировать ваш многозадачный код на гонки данных, взаимоблокировки и другие дефекты параллелизма, если анализу известно о модели параллелизма в вашем коде. В некоторых ситуациях Polyspace может автоматически обнаруживать создание потоков и критические разделы в вашем коде. Bug Finder обнаруживает их по умолчанию. В Code Prover вы включаете автоматическое обнаружение с помощью опции Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection).
Рабочий процесс анализа многозадачного кода см. в разделе Анализ многозадачных программ в Polyspace.
Если функция создания потоков не обнаружена автоматически:
Можно также сопоставить функцию с функцией создания потоков, которую Polyspace может обнаружить автоматически. Используйте опцию -code-behavior-specifications.
В противном случае необходимо вручную смоделировать многозадачные потоки с помощью опций строения. Смотрите Настройку многозадачного анализа Polyspace вручную.
Polyspace может обнаружить создание потоков и критические сечения, если вы используете примитивы из этих групп. Polyspace распознает вызовы этих стандартных программ как создание нового потока или как начало или конец критического раздела.
Создание потоков: pthread_create
Начинается критический раздел: pthread_mutex_lock
Критические сечения заканчиваются: pthread_mutex_unlock
Создание потоков: taskSpawn
Начинается критический раздел: semTake
Критические сечения заканчиваются: semGive
Активация автоматического обнаружения примитивов параллелизма для VxWork®, в пользовательском интерфейсе десктопных продуктов 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® стандартные программы создания потоков и иллюстрируют классический пример взаимоблокировки. Запустите Bug Finder на этом коде, чтобы увидеть тупик.
#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_<reservedrangesplaceholder0 >id - идентификатор, сопоставленный с потоком. В предыдущем примере потоки идентифицируются как 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 не может моделировать:
Приоритеты и атрибуты потока - проигнорированы 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 является NULLPolyspace обнаруживает только один образец этой функции или задачи.
(Только для C++ 11) Если во время создания потока в качестве начальных функций используются лямбда-выражения, Polyspace не обнаруживает общие переменные в лямбда-выражениях.
(C++ 11 потоков только с Polyspace Code Prover) Строковые литералы как аргумент функции потока - Code Prover показывает красную ошибку Illegally dereferenced pointer, если функция потока имеет std::string& параметр и вы передаете строковый буквальный аргумент.
-code-behavior-specifications | Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)
