マルチタスキングコードでの共有変数の保護

コードがマルチタスキングを対象としている場合、コードのタスクは共通の共有変数にアクセスできます。データレースを防ぐために、変数に対する読み取りと書き込み操作を保護できます。このトピックでは、Polyspace^® が認識できるさまざまな保護メカニズムを示します。

保護されていないアクセスの検出

Bug Finder と Code Prover のいずれかを使用して、保護されていないアクセスを検出できます。Code Prover はより網羅的で、共有変数が同時アクセスから保護されているかどうかを証明します。

Bug Finder は結果の [データレース] を使用して、保護されていないアクセスを検出します。データレースを参照してください。
Code Prover は結果の [Shared unprotected global variable] を使用して、保護されていないアクセスを検出します。保護されていない可能性のある変数を参照してください。

signal_handler_1 と signal_handler_2 を周期タスクとして指定して、次のコードを解析するとします。解析オプション [周期タスク] (-cyclic-tasks) を使用します。

#include <limits.h>
int shared_var;

void inc() {
     shared_var+=2;
}

void reset() {
     shared_var = 0;
}

void signal_handler_1(void) {
    reset();
    inc();
    inc();
}

void signal_handler_2(void) {
    shared_var = INT_MAX;
}

 void main() {
}

Bug Finder では、shared_var に対してデータレースが示されます。Code Prover では、shared_var が保護されていない可能性のある変数であることが示されます。また、Code Prover では、操作 shared_var += 2 がオーバーフローする可能性があることも示されます。このオーバーフローは、signal_handler_2 の操作 shared_var = INT_MAX の直後に signal_handler_1 の inc が呼び出される場合に発生します。

クリティカルセクションを使用した保護

1 つの解決策として、クリティカルセクションを使用して、共有変数に対する操作を保護します。

前の例で、shared_var に対する操作が同じクリティカルセクション内になるようにコードを変更します。関数 take_semaphore と関数 give_semaphore を使用して、クリティカルセクションを開始および終了します。クリティカルセクションを開始、終了するこれらの関数を指定するには、解析オプション [クリティカルセクション詳細] (-critical-section-begin -critical-section-end) を使用します。

#include <limits.h>
int shared_var;

void inc() {
 shared_var+=2;
}

void reset() {
 shared_var = 0;
}

/* Declare lock and unlock functions */
void take_semaphore(void);
void give_semaphore(void);

void signal_handler_1() {
    /* Begin critical section */
    take_semaphore();
    reset();
    inc();
    inc();
    /* End critical section */
    give_semaphore();
    
}

void signal_handler_2() {
   /* Begin critical section */
   take_semaphore();
   shared_var = INT_MAX;
   /* End critical section */
   give_semaphore();
   
}

void main() {
}

Bug Finder ではデータレースが示されません。Code Prover では、共有変数が保護されていることが証明されます。signal_handler_1 の reset() 呼び出しが常に inc() 呼び出しに先行するため、オーバーフローも示されません。

POSIX^® 関数 pthread_mutex_lock や pthread_mutex_unlock などのプリミティブ型を使用して、クリティカルセクションを開始および終了することもできます。Polyspace で自動的に検出できるプリミティブ型のリストについては、Polyspace でのスレッド作成とクリティカルセクションの自動検出を参照してください。

時間的に排他なタスクを使用した保護

別の解決策として、タスクのグループを時間的に排他として指定します。時間的に排他なタスクは互いに割り込むことはできません。

前の例で、signal_handler_1 および signal_handler_2 は時間的に排他であると指定します。オプション [時間的に排他なタスク] (-temporal-exclusions-file) を使用します。

優先順位を使用した保護

別の解決策として、1 つのタスクの優先順位を他よりも高く指定します。

前の例で、signal_handler_1 は割り込みであると指定します。signal_handler_2 を周期タスクとして保持します。オプション [周期タスク] (-cyclic-tasks) と [割り込み] (-interrupts) を使用します。

Bug Finder ではデータレース検出がもう示されません。理由は以下です。

signal_handler_2 の操作 shared_var = INT_MAX はアトミックです。そのため、signal_handler_1 の操作がそれに割り込む可能性はありません。
signal_handler_1 の優先順位が高いため、signal_handler_1 の操作に signal_handler_2 の操作が割り込む可能性はありません。

以下のオプションを使用して最大 4 つの異なる優先順位を指定できます (優先順位が高い順にリスト)。

優先順位の高いタスクは、優先順位の低いタスクに対してアトミックです。オプション -detect-atomic-data-race を使用した解析では、優先順位の違いを無視し、引き続きデータレースを表示することに注意してください。Polyspace でのデータレース検出のタスク優先順位の定義も参照してください。

Code Prover では操作のアトミック性が考慮されないため、shared_var は保護されていない可能性のある変数であることが引き続き示されます (signal_handler_1 の操作は引き続き signal_handler_2 の操作に割り込むことができます)。signal_handler_1 と signal_handler_2 の両方を割り込みとして指定する場合にのみ、Code Prover で shared_var が保護された変数として示されます。

割り込みの無効化による保護

Bug Finder 解析では、現在のもの以外のすべてのタスクと割り込みを無効にして操作のグループを保護できます。

オプション [すべての割り込みを無効にする] (-routine-disable-interrupts -routine-enable-interrupts) を使用して、呼び出されたときにすべての割り込みを無効にするルーチンと、それらを再度有効にするルーチンを指定します。無効にするルーチンは、次のすべてに優先して無効にします。

非周期のタスク。
タスク (-entry-points) を参照してください。
周期タスク。
周期タスク (-cyclic-tasks) を参照してください。
割り込み。
割り込み (-interrupts) を参照してください。

つまり、解析では、無効にするルーチンと有効にするルーチンの間にある演算本体はアトミックで、まったく割り込むことはできないと見なされます。

割り込みを無効にするルーチンを呼び出した後は、割り込みを再度有効にする別のルーチンを呼び出すまで、以降の操作はすべてアトミックになります。それらの操作は、すべての他のタスクでの操作に対してアトミックです。