OpenMP Fortran程序中死锁的静态检测

与BARRIER相关的死锁是导致OpenMP程序失效的重要隐患之一.对该类隐患的静态检测有助于在OpenMP程序运行之前提高其正确性.为了便于检测,将这种死锁分为两类.借助搜索与数据流分析分别按照存在性规则和非一致性规则检测第1类和第2类死锁.扩展了传统的控制流图以表示OpenMP程序.对于每个检测到的死锁,通过回溯记录控制流图中相关的路径,并利用静态分支预测量化其严重程度.基于上述思想,实现了一个OpenMP Fortran程序中死锁的静态检测工具C-Checker.实验表明,该工具能有效地检测OpenMP程序中与BARRIER相关的死锁.

Static Detection of Deadlocks in OpenMP Fortran Programs

The deadlocks related to barriers are one kind of the major factors that cause OpenMP programs to malfunction. Static detection of these hazards can help enhance the correctness of OpenMP programs before they are executed. For convenience of detection, this kind of deadlocks is classified into two categories. By searching and data flow analysis, the first and the second category of deadlocks are detected according to the existence rule and nonuniformity rule respectively. Traditional control flow graph is extended to represent OpenMP programs. For each detected deadlock, backtracking is used to record the related paths in the control flow graph, and static branch prediction is employed to quantify its severity. Based on these ideas, a tool, called C-Checker, to statically detect deadlocks in OpenMP Fortran programs is implemented. Experiments show the C-Checker can effectively detect the deadlocks concerned.