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许可证下使用。