Polyspace でのスレッド作成とクリティカルセクションの自動検出

R2026a

Polyspace^® を使用して、複数のスレッドを同時実行するプログラムを解析できます。Polyspace では、解析でコード内に同時実行モデルが認識される場合、マルチタスキングコードのデータレース、デッドロック、その他の同時実行の欠陥を解析できます。場合によっては、Polyspace で、コード内のスレッド作成とクリティカルセクションを自動的に検出できます。Bug Finder では、それらを既定で検出します。Code Prover では、オプション [Code Prover の同時実行の自動検出を有効にする] (-enable-concurrency-detection) を使用して、自動検出を有効にします。

マルチタスキングコード解析のワークフローについては、Polyspace でのマルチタスキングプログラムの解析を参照してください。

スレッド作成関数が自動的に検出されない場合:

この関数を Polyspace で自動的に検出できるスレッド作成関数にマップすることもできます。オプション -code-behavior-specifications を使用します。
そうしない場合は、マルチタスキングスレッドのモデル化は、構成オプションを使用して手動で行わなければなりません。Polyspace マルチタスキング解析の手動設定を参照してください。

Polyspace で検出できるマルチタスキングルーチン

Polyspace では、これらのグループのプリミティブを使用する場合、スレッド作成とクリティカルセクションを検出できます。Polyspace では、これらのルーチンの呼び出しは、新しいスレッドの作成、またはクリティカルセクションの開始や終了として認識します。

POSIX

スレッド作成: pthread_create

クリティカルセクション開始: pthread_mutex_lock

クリティカルセクション終了: pthread_mutex_unlock

再帰ミューテックス: 属性 PTHREAD_MUTEX_RECURSIVE を指定した pthread_mutexattr_settype。

信号ハンドラー: signal

VxWorks

スレッド作成: taskSpawn

クリティカルセクション開始: semTake

クリティカルセクション終了: semGive

VxWorks^® の同時実行プリミティブ型の自動検出を有効にするには、プロジェクト構成で以下のマクロの値を設定します。

CPU=I80386
_GNUC__=2
__OS_VXWORKS

マクロの定義方法の詳細については、プリプロセッサ定義 (-D) を参照してください。

マルチタスキング関数が main という名前のエントリポイントから作成されている場合のみ、同時実行を検出できます。エントリポイントが vxworks_entry_point などの別の名前の場合、以下のいずれかを実行します。

main 関数を用意します。
オプション [プリプロセッサ定義] (-D) を使用して vxworks_entry_point=main を設定します。

Windows

スレッド作成: CreateThread

クリティカルセクション開始: EnterCriticalSection

クリティカルセクション終了: LeaveCriticalSection

μC/OS II

スレッド作成: OSTaskCreate

クリティカルセクション開始: OSMutexPend

クリティカルセクション終了: OSMutexPost

μC/OS III

スレッド作成: OSTaskCreate

クリティカルセクション開始: OSMutexPend

クリティカルセクション終了: OSMutexPost

Zephyr リアルタイムオペレーティングシステム

スレッド作成: k_thread_create

クリティカルセクション開始: k_sem_take

クリティカルセクション終了: k_sem_give

C++11、C++14、C++17

スレッド作成: std::thread::thread

クリティカルセクション開始: std::mutex::lock、std::mutex::try_lock、std::recursive_mutex::lock

クリティカルセクション終了: std::mutex::unlock、std::recursive_mutex::unlock

信号ハンドラー: std::signal

C++11 スレッドの自動検出には、コンパイラヘッダーファイルのパスを明示的に指定するか、polyspace-configure を使用します。

たとえば、スレッド作成に std::thread を使用する場合、thread.h を含むフォルダーへのパスを明示的に指定します。

スレッドの自動検出の制限も参照してください。

C11

スレッド作成: thrd_create

クリティカルセクション開始: mtx_lock

クリティカルセクション終了: mtx_unlock

信号ハンドラー: signal

再帰ミューテックス: mtx_recursive

自動スレッド検出の例

次のマルチタスキングコードでは、5 本のフォークを共有する 5 人の哲学者がモデル化されています。この例では、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;
}

それぞれの哲学者は、食事をするのにフォークを 2 本、右と左に 1 本ずつ必要としています。関数 philo1、philo2、philo3、philo4 および philo5 がそれぞれの哲学者を表現しています。各関数には、食事をするのに必要なフォーク 2 本を表現する 2 つの pthread_mutex_t リソースが必要です。5 つの関数はすべて、5 つのコンカレントスレッドで同時に実行されます。

ただし、この例ではデッドロックが発生します。それぞれの哲学者が最初のフォークを手にする (各スレッドが 1 つの pthread_mutex_t リソースをロックする) と、すべてのフォークが使用中になります。よって、哲学者 (スレッド) が 2 本目のフォーク (2 番目の pthread_mutex_t リソース) が使用可能になるのを待機します。しかし、待機中の哲学者 (スレッド) がすべてのフォーク (リソース) を持っているため、デッドロックが発生します。

自動的に検出されるスレッドの命名規則

pthread_create() などの関数を使用して新しいスレッド (タスク) を作成する場合、各スレッドは固有の識別子に関連付けられます。たとえば、以下の例では、識別子 id1 と id2 を使用して 2 つのスレッドが作成されます。

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);
```

異なるスレッド識別子を使用して 2 つのスレッドを作成し、それらのスレッド識別子に対して同じローカル変数名を使用した場合、2 つ目のスレッドの名前は 1 つ目のスレッドと区別するために変更されます。たとえば、以下のスレッドは 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 はスレッドが 1 つだけ作成されたと見なします。
pthread_t id1, id2; void start(pthread_t* id) { pthread_create(id, NULL, start_routine, NULL); } void main() { start(&id1); start(&id2); }

(Polyspace Code Prover™ のみ) 共有ローカル変数 — グローバル変数のみが共有と見なされます。ローカル変数に複数のスレッドからアクセスがある場合、解析ではその変数の共有特性は考慮されません。

例

この例では、(新しいスレッドの作成後) ローカル変数 x に task1 と task2 の両方からアクセスできることが解析で考慮されません。

#include <pthread.h>
#include <stdlib.h>


void* task2(void* args)
{
    int* x = (int*) args;
    *x = 1;
    return (void*)x;
}

void task1()
{
    int x;
    x = 2;
    pthread_t id;
    (void)pthread_create(&id, NULL, task2, (void*) &x);
    /* x (local var) passed to task2 */
    x = 3 ;

    /* Unknown thread priority means x = 1 OR x = 3.*/
    /* However, the analysis considers  x = 3 */
    /* Assertion below is green */
    assert(x == 3);
}

int main(void)
{
    task1();
    return 0;
}

(Polyspace Code Prover のみ) 共有動的メモリ — グローバル変数のみが共有と見なされます。動的に割り当てられたメモリ領域に複数のスレッドからアクセスがある場合、解析ではその変数の共有特性は考慮されません。
この例では、lx が共有メモリ領域を参照していることが解析で考慮されません。(新しいスレッドの作成後) この領域には task1 と task2 の両方がアクセスできます。Code Prover 解析でも、lx は共有されない変数としてレポートされます。
#include <pthread.h> #include <stdlib.h> static int* lx; void* task2(void* args) { int* x = (int*) args; *x = 1; return (void*)x; } void task1() { pthread_t id; lx = (int*)malloc(sizeof(int)); if (lx == NULL) exit(1); (void)pthread_create(&id, NULL, task2, (void*) lx); *lx = 3 ; /* Unknown thread priority means *lx = 1 OR *lx = 3.*/ /* However, the analysis considers *lx = 3 */ /* Assertion below is green */ assert(*lx == 3); } int main(void) { task1(); return 0; }
threadId が NULL に設定されている場合に CreateThread で作成されるタスクの数 — 同じ関数を実行する複数のスレッドを作成するとき、CreateThread の最後の引数が NULL である場合、Polyspace はこの関数の 1 つのインスタンス (つまりタスク) のみ検出します。
この例では、Polyspace により検出される thread_function1() のインスタンスは 1 つのみですが、thread_function2() のインスタンスは 10 個検出されます。
#include <windows.h> #define MAX_LOOP_THREADS 10 DWORD WINAPI thread_function1(LPVOID data) {} DWORD WINAPI thread_function2(LPVOID data) {} HANDLE hds1[MAX_LOOP_THREADS]; HANDLE hds2[MAX_LOOP_THREADS]; DWORD threadId[MAX_LOOP_THREADS]; int main(void) { for (int i = 0; i < MAX_LOOP_THREADS; i++) { hds1[i] = CreateThread(NULL, 0, thread_function1, NULL, 0, NULL); hds2[i] = CreateThread(NULL, 0, thread_function2, NULL, 0, &threadId[i]); } return 0; }
(Polyspace Code Prover での C++11 スレッドのみ) スレッド関数の引数としての文字列リテラル — スレッド関数に std::string& パラメーターがあり、文字列リテラル引数を渡す場合、Code Prover では [不適切にデリファレンスされたポインター] のレッドエラーが表示されます。
この例では、スレッド関数 foo に std::string& パラメーターがあります。スレッドが開始されると、文字列リテラルがこの関数に引数として渡され、std::string 型への暗黙的な変換が行われます。この変換により Code Prover は元の文字列リテラルを追跡できなくなります。そのため、foo 本体の operator<< に下線が赤の破線で表示され、operator<< 本体に [不適切にデリファレンスされたポインター] のレッドチェックが表示されます。
#include <iostream> #include <thread> using namespace std; void foo(const std::string& f) { std::cout << f; } void main() { std::thread t1(foo,"foo_arg"); }
この問題を回避するには、文字列リテラルを一時変数に代入し、その変数を引数としてスレッド関数に渡します。
#include <iostream> #include <thread> using namespace std; void foo(const std::string& f) { std::cout << f; } void main() { std::string str = "foo_arg"; std::thread t1(foo, str); }

参考

Code Prover の同時実行の自動検出を有効にする (-enable-concurrency-detection) | -code-behavior-specifications

Polyspace でのスレッド作成とクリティカル セクションの自動検出

Polyspace で検出できるマルチタスキング ルーチン