Deadlock_Racer

僵局

僵局是一種靜態分析儀，用於檢測作為Frama-C平台插件的C計劃中潛在的僵局。

核心算法基於現有的工具racerx。所謂的鎖定分析遍歷控制流程圖，併計算在任何程序點上保存的鎖集。當獲得鎖定鎖定的鎖定鎖定時，鎖定鎖定已包含鎖定A時，將依賴項A-> b添加到鎖定器中。然後，此圖中的每個週期都報告為潛在的僵局。

該插件使用eVA（frama-c的值分析插件）來計算鎖定操作參數的May-Point-to信息。由於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釩兼容，其詳細的安裝指南可以在用戶手冊中找到，並且需要OCAML版本至少4.12。除了Frama-C，僵局還需要安裝OPAM軟件包：

 ounit2
containers

在安裝依賴項並克隆此倉庫後，可以將僵局安裝如下：

 cd Deadlock
make setup
make
make install

您也可以通過使用docker run -it tdacik/deadlock或運行make docker構建最新版本的圖像。

用法

運行插件的最簡單方法是：

 frama-c -deadlock source_file1.c source_file2.c ...

有關更高級的用法，請參見用於調整分析和GUI手冊的命令行選項列表，以可視化Frama-C的GUI應用程序中的結果。

相關論文

DacíkT。 frama-C的靜態僵局在Excel@fit'20的論文集。布爾諾技術大學，信息技術學院。 2020

DacíkT。 Frama-C環境中的靜態分析重點是僵局檢測學士學位論文。布爾諾技術大學，信息技術學院。 2020-07-10。由VojnarTomáš監督。

接觸

如果您有任何疑問，請隨時與工具/方法作者聯繫：

• tomášDacík <[email protected]>
• tomášvojnar <[email protected]>

執照

該插件可在MIT許可證下使用。