Автоматическое обнаружение создания потока и критического раздела в Polyspace

С Polyspace® можно анализировать программы где несколько потоков, запущенных одновременно. Polyspace может анализировать ваш многозадачный код для гонок данных, мертвых блокировок и других дефектов параллелизма, если анализ знает о модели параллелизма в вашем коде. В некоторых ситуациях Polyspace может обнаружить создание потока и критические разделы в вашем коде автоматически. Средство поиска ошибки обнаруживает их по умолчанию. В Программе автоматического доказательства Кода вы включаете автоматическое обнаружение с помощью опции Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection).

Для многозадачного рабочего процесса анализа кода смотрите, Анализируют Многозадачные Программы в Polyspace.

Если ваша функция создания потока не обнаруживается автоматически:

Многозадачные Стандартные программы, которые Может Обнаружить Polyspace

Polyspace может обнаружить создание потока и критические разделы, если вы используете примитивы от этих групп. Polyspace распознает вызовы этих стандартных программ как создание нового потока или как начало или конец критического раздела.

POSIX

Создание потока: pthread_create

Критический раздел начинается: pthread_mutex_lock

Критические концы раздела: pthread_mutex_unlock

VxWorks

Создание потока: taskSpawn

Критический раздел начинается: semTake

Критические концы раздела: semGive

Чтобы активировать автоматическое обнаружение примитивов параллелизма для VxWorks®, в пользовательском интерфейсе десктопных решений Polyspace, используют VxWorks шаблон. Для получения дополнительной информации о шаблонах смотрите, Создают Проект Используя Шаблон конфигурации (Polyspace Code Prover). В командной строке используйте эти опции:

-D1=CPU=I80386
-D2=__GNUC__=2
-D3=__OS_VXWORKS

Обнаружение параллелизма возможно, только если многозадачные функции создаются из точки входа под названием main. Если точка входа имеет другое имя, такое как vxworks_entry_point, выполнить одно из следующих действий:

  • Обеспечьте main функция.

  • Preprocessor definitions (-D): В определениях препроцессора, набор vxworks_entry_point=main.

Windows

Создание потока: CreateThread

Критический раздел начинается: EnterCriticalSection

Критические концы раздела: LeaveCriticalSection

μC/OS II

Создание потока: OSTaskCreate

Критический раздел начинается: OSMutexPend

Критические концы раздела: OSMutexPost

C++ 11

Создание потока: std::thread::thread

Критический раздел начинается: std::mutex::lock

Критические концы раздела: std::mutex::unlock

Для автоматического обнаружения C++ 11 потоков явным образом задайте пути к своим заголовочным файлам компилятора или использованию polyspace-configure.

Например, если вы используете std::thread для создания потока явным образом задайте путь к папке, содержащей thread.h.

См. также Ограничения Автоматического Обнаружения Потока.

C11

Создание потока: 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_id, где 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 isNull, Polyspace только обнаруживает один экземпляр этой функции или задачу.

     Пример

  • (C++ 11 только), Если вы используете лямбда-выражения, как запускают функции во время создания потока, Polyspace, не обнаруживает совместно используемые переменные в лямбда-выражениях.

     Пример

  • (C++ 11 потоков только с Polyspace Code Prover) Строковые литералы как аргумент функции потока — Программа автоматического доказательства Кода показывает красную ошибку Illegally dereferenced pointer, если функция потока имеет std::string& параметр и вы передаете аргумент строкового литерала.

     Пример

Смотрите также

|

Похожие темы