Deadlock_Racer
v1.0.1
Deadlockは、FRAMA-Cプラットフォームのプラグインとして実装されたCプログラムで潜在的なデッドロックを検出するための静的分析器です。
コアアルゴリズムは、既存のツールRacerxに基づいています。いわゆるロックセット分析は、制御フローグラフを通過し、任意のプログラムポイントに保持されているロックのセットを計算します。ロックBが既にロックAを含む電流ロックセットで取得されると、依存性a-> bがロックグラフに追加されます。このグラフの各サイクルは、潜在的なデッドロックとして報告されます。
プラグインは、EVA（Frama-Cの値分析プラグイン）を使用して、ロック操作のパラメーターの5月のポイントツー情報を計算します。 EVAは同時プログラムをネイティブに分析できないため、最初にプログラム内のすべてのスレッドを特定し、スレッドが作成されたプログラムポイントのコンテキストで各スレッドに対して個別に実行します。結果は承認不足になりますが、スレッドのインターリービングは考慮されません。
この例は、簡単なデッドロックでプログラムの出力を示しています。より複雑な例はここにあります。
void * thread1 ( void * v )
{
pthread_mutex_lock ( & lock1 );
pthread_mutex_lock ( & lock2 );
...
pthread_mutex_unlock ( & lock2 );
pthread_mutex_unlock ( & lock1 );
}
void * thread2 ( void * v )
{
pthread_mutex_lock ( & lock2 );
pthread_mutex_lock ( & lock1 );
...
pthread_mutex_unlock ( & lock1 );
pthread_mutex_unlock ( & lock2 );
} [kernel] Parsing simple_deadlock.c (with preprocessing)
[Deadlock] Deadlock analysis started
[Deadlock] === Assumed threads: ===
[Deadlock] main
[Deadlock] thread1
[Deadlock] thread2
[Deadlock] === Lockgraph: ===
[Deadlock] lock1 -> lock2
[Deadlock] lock2 -> lock1
[Deadlock] ==== Results: ====
[Deadlock] Deadlock between threads thread1 and thread2:
Trace of dependency (lock2 -> lock1):
In thread thread2:
Lock of lock2 (simple_deadlock.c:20)
Lock of lock1 (simple_deadlock.c:21)
Trace of dependency (lock1 -> lock2):
In thread thread1:
Lock of lock1 (simple_deadlock.c:10)
Lock of lock2 (simple_deadlock.c:11)
現在のバージョンはFrama-C Vanadiumと互換性があり、詳細なインストールガイドはユーザーマニュアルにあり、OCAMLバージョンが少なくとも4.12を必要とします。 Frama-Cに加えて、 Deadlockでは、Opamパッケージをインストールする必要があります。
ounit2
containers
依存関係をインストールし、このリポジタリティをクローニングした後、デッドロックは次のようにインストールできます。
cd Deadlock
make setup
make
make install
また、 docker run -it tdacik/deadlockを使用するか、 make dockerを実行して最新のバージョンの画像を作成することにより、Dockerでデッドロックを実行することもできます。
プラグインを実行する最も簡単な方法は、次のとおりです。
frama-c -deadlock source_file1.c source_file2.c ...
より高度な使用については、FRAMA-CのGUIアプリケーションでの結果の視覚化のために、分析とGUIマニュアルを調整するためのコマンドラインオプションのリストを参照してください。
DacíkT。Excel@Fit'20の議事録におけるFrama-Cの静的デッドロック検出。 BRNO工科大学、情報技術学部。 2020
DacíkT。Frama-C環境における静的分析は、Deadlock検出学士の論文に焦点を当てています。 BRNO工科大学、情報技術学部。 2020-07-10。 VojnarTomášによって監督。
ご不明な点がございましたら、ツール/メソッドの著者にお問い合わせください。
プラグインはMITライセンスで利用できます。
