共有変数

複数のタスクの間で共有され、タスクによる同時アクセスから保護されたグローバル変数

このページをすべて展開する

説明

保護された共有グローバル変数には以下のプロパティがあります。

  • 変数は複数のタスクで使用されている。

  • 変数に対するすべての操作は、クリティカル セクションまたは時間的排他により、割り込みから保護されます。クリティカル セクションの開始および終了時の関数の呼び出しは到達可能でなくてはなりません。

マルチタスクを対象としていないコードでは、すべてのグローバル変数は非共有です。

検証結果では、これらの変数は [ソース]、[結果のリスト] および [変数アクセス] ペインにおいてグリーンで色付けされています。[ソース] ペインでは、色付けは宣言時にのみ変数に適用されます。

例

すべて展開する

#include <limits.h>
int shared_var;

void inc() {
    shared_var+=2;
}

void reset() {
    shared_var = 0;
}

void task() {
    volatile int randomValue = 0;
    while(randomValue) {
        reset();
        inc();
        inc();
    }
}

void interrupt() {
    shared_var = INT_MAX;
}

void interrupt_handler() {
    volatile int randomValue = 0;
    while(randomValue) {
        interrupt();
    }
}

void main() {
}

この例では、以下のマルチタスキング オプションが指定されている場合、shared_var は保護された共有変数です。

オプション値
マルチタスクを手動で構成
タスク

task

interrupt_handler

時間的に排他なタスクtask interrupt_handler

コマンド ラインでは以下を使用できます。 

 polyspace-code-prover
   -entry-points task,interrupt_handler
   -temporal-exclusions-file "C:\exclusions_file.txt"
ここで、ファイル C:\exclusions_file.txt には以下の行があります。 
task interrupt_handler

変数は task および interrupt_handler の間で共有されています。ただし、task および interrupt_handler は時間的に排他であるため、変数の操作は互いに割り込みできません。

#include <limits.h>
int shared_var;

void inc() {
    shared_var+=2;
}

void reset() {
    shared_var = 0;
}

void take_semaphore(void);
void give_semaphore(void);

void task() {
    volatile int randomValue = 0;
    while(randomValue) {
        take_semaphore();
        reset();
        inc();
        inc();
        give_semaphore();
    }
}

void interrupt() {
    shared_var = INT_MAX;
}

void interrupt_handler() {
    volatile int randomValue = 0;
    while(randomValue) {
        take_semaphore();
        interrupt();
        give_semaphore();
    }
}

void main() {
}

この例では、以下のオプションが指定されている場合、shared_var は保護された共有変数です。

オプション値
マルチタスクを手動で構成
タスク

task

interrupt_handler

クリティカル セクション詳細開始ルーチン終了ルーチン
take_semaphoregive_semaphore

コマンド ラインでは以下を使用できます。 

 polyspace-code-prover 
   -entry-points task,interrupt_handler
   -critical-section-begin take_semaphore:cs1
   -critical-section-end give_semaphore:cs1

変数は task および interrupt_handler の間で共有されています。ただし、変数の操作は同じクリティカル セクションの開始および終了手続きの呼び出しの間にあるため、互いに割り込みできません。

struct S {
    unsigned int var_1;
    unsigned int var_2;
};

volatile int randomVal;

struct S sharedStruct;

void task1(void) {
    while(randomVal)
    	operation1();
}

void task2(void) {
    while(randomVal)
	    operation2();
}

void operation1(void) {
        sharedStruct.var_1++;
}

void operation2(void) {
        sharedStruct.var_2++;
}

int main(void) {
    return 0;
}

この例では、以下のオプションが指定されている場合、sharedStruct は保護された共有変数です。

オプション値
マルチタスクを手動で構成
タスク

task1

task2

コマンド ラインでは以下を使用できます。 

 polyspace-code-prover 
    -entry-points task1,task2

ソフトウェアで sharedStruct が保護されていると判定される理由は次のとおりです。

  • task1 は sharedStruct.var_1 でのみ操作を実行する。

  • task2 は sharedStruct.var_2 でのみ操作を実行する。

この結果を選択すると、[結果の詳細] ペインには、変数に対するすべての操作がアクセス パターンによって保護されることが表示されます。[変数アクセス] ペインでは、変数 sharedStruct の行に Access pattern が保護型として記載されます。

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

pthread_mutex_t lock;
pthread_t id1, id2; 

int var; 

void * t1(void* b) { 
    pthread_mutex_lock(&lock); 
    var++; 
    pthread_mutex_unlock(&lock); 
} 

void * t2(void* a) { 
    pthread_mutex_lock(&lock); 
    var = 1; 
    pthread_mutex_unlock(&lock); 
} 

int main(void) { 
    pthread_create(&id1, NULL, t1, NULL); 
    pthread_create(&id2, NULL, t2, NULL); 

    return 0; 
}

以下のオプションが指定されている場合、var は保護された共有変数です。

オプション名値
同時実行の自動検出を有効にする

コマンド ラインでは以下を使用できます。 

 polyspace-code-prover
    -enable-concurrency-detection

この例では、同時実行検出オプションを指定した場合、プログラムでマルチタスキングを使用していることが Polyspace® Code Prover™ によって検出されます。2 つのタスク lock と var によって 2 つの変数が共有されています。lock は pthread ミューテックス変数であり、pthread_mutex_lock と pthread_mutex_unlock によってミューテックスのロックおよびロック解除に使用されます。pthread 固有の設計パターンにより、lock が保護されます。[結果の詳細] ペインと [変数アクセス] ペインでは、Design Pattern が保護型として示されます。

ミューテックスのロック メカニズムおよびロック解除メカニズムにより、もう一方の共有変数 var が保護されます。[結果の詳細] ペインと [変数アクセス] ペインでは、Mutex が保護型として示されます。

Code Prover は、名前がない共有メモリ領域を検出しません。絶対アドレスをポインターに割り当てたり、動的にメモリを割り当てたりすることで、名前なしメモリ領域が作成される場合があります。こうした領域を表す名前付き変数はありません。

たとえば、次の例では ptr が動的に割り当てられるメモリを指しています。

#include <stdlib.h>

int* ptr;

void flip() {
   *ptr = 0;
}

void flop() {
   if (*ptr == 0) {
      *ptr = 1;
  }
}
void main() {
   ptr = (int*) malloc(sizeof(int));
}
アプリケーションのエントリ ポイントとして機能する関数 flip() および flop() を指定した場合でも、Code Prover には、ptr (または *ptr) が指すメモリ領域に同時にアクセスできるとは示されません。

チェック情報

言語: C | C++

参考

| | | | | |

トピック