-detect-atomic-data-race

アトミック操作でのデータレース検出の有効化

構文

-detect-atomic-data-race

説明

-detect-atomic-data-race は、解析でアトミック操作でのデータレースをチェックする必要があることを指定します。

既定では、Polyspace^® はアトミック操作でのデータレースをチェックしません。Bug Finder は、操作を 1 つのマシン命令で実行できる場合、その操作をアトミック操作と見なします。次に例を示します。

以下の演算を考えます。
```
int var = 0;
```
int のサイズがターゲットのワードサイズまたはポインターサイズより小さい場合、この操作は 1 つのマシン命令で実行できます。
以下の演算を考えます。
```
MYREG = (u32dma0_chbit << 8UL) | u32dma0_chbit;
```
この操作を実行するには複数のサイクルが必要になるため、これは非アトミック操作です。

マルチタスキングコードでのアトミック操作の定義を参照してください。アトミック操作のこの定義を使用せずに、すべての操作でデータレースをチェックするには、オプション -detect-atomic-data-race を指定します。

ユーザーインターフェイスから検証を実行する場合 (デスクトップ製品のみ)、[その他] フィールドでこのオプションを指定します。Otherを参照してください。

例

このコード例では、タスク task1 での書き込み操作 var=1; がタスク task2 での読み取り操作 local_var=var; と同時に実行されます。既定では、Polyspace は書き込み操作をアトミック操作であると見なします。環境によっては、書き込み操作を含むように data race チェッカーを拡張する必要がある場合もあります。

コード例

この例のアトミック操作でデータレースをチェックするには、コマンドラインで以下のオプションを指定します。

 polyspace-bug-finder -sources SRC -checkers DATA_RACE
   -entry-points task1,task2,task3
   -critical-section-begin begin_critical_section:cs1
   -critical-section-end end_critical_section:cs1
   -detect-atomic-data-race

Polyspace ユーザーインターフェイスでは、以下の表に記載するオプションを使用します。

オプション	仕様
`Other`	`-detect-atomic-data-race`
`マルチタスクを手動で構成`
`タスク (-entry-points)`	`task1` `task2` `task3`
`クリティカルセクション詳細 (-critical-section-begin -critical-section-end)`	開始ルーチン	終了ルーチン
	`begin_critical_section`	`end_critical_section`

依存関係

データレースを検出するには、以下の同時実行オプションを構成する必要があります。
- タスク (-entry-points)
- クリティカルセクション詳細 (-critical-section-begin -critical-section-end)
マルチタスキングを参照してください。同時実行オプションを構成せずにオプション -detect-atomic-data-race を指定すると、Polyspace が警告を出力します。
このオプションは以下のチェッカーを拡張するものであり、これらのチェッカーを少なくとも 1 つ有効にしていない限り、役に立ちません。

ヒント

このオプションは、Polyspace as You Code 解析では役立ちません。

参考

トピック

Extend Data Race Checkers to Atomic Operations