CIVL 框架

CIVL (Concurrency Intermediate Verification Language) 框架的用途是验证 C 并发程序。CIVL 框架提供了三个环境:

  1. CIVL-C 编程语言。CIVL-C 语言是 C 语言的一个子集,并且扩展了部分指令,用于描述并发程序的元素。
  2. 验证和分析工具,包括基于符号执行的模型检测器,能够找到 CIVL-C 程序的缺陷。
  3. 一切其他工具,

C 程序若用了一些类库,比如 MPI, CUDA,OpenMP,OpenCL 等等,能够自动被转换到 CIVL-C 程序。

CIVL 安装

  1. 安装 Z3 求解器。
  2. 下载源码
  3. 解压: tar xvf xxxxx.tgz
  4. 使用命令: java -jar /path/to/civl-xxxx.jar

例子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
// file:  diningBad.cvl

#include <civlc.cvh>

$input int B = 4; // upper bound on number of philosophers
$input int n; // number of philosophers
$assume(2<=n && n<=B);

_Bool forks[n]; // Each fork will be on the table ($true) or in a hand ($false).

void dine(int id) {
int left = id;
int right = (id + 1) % n;

while (1) {
$when (forks[left]) forks[left] = $false;
$when (forks[right]) forks[right] = $false;
forks[right] = $true;
forks[left] = $true;
}
}

void main() {
$for(int i: 0 .. n-1)
forks[i] = $true;
$parfor(int i: 0 .. n-1)
dine(i);
}

使用 civl 验证:

civl verify -inputB=4 diningBad.cvl
设置 (upper bound of number of philosophers) 为4

验证报告

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
Violation 0 encountered at depth 21:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at diningBad.cvl:25.11-11
dine(i);
^

A deadlock is possible:
Path condition: true
Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false

Call stacks:
process 0:
main at diningBad.cvl:25.11 ";"
process 1:
dine at diningBad.cvl:15.4-8 "$when" called from
_par_proc0 at diningBad.cvl:25.4-7 "dine"
process 2:
dine at diningBad.cvl:15.4-8 "$when" called from
_par_proc0 at diningBad.cvl:25.4-7 "dine"

Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
Terminating search after finding 1 violation.

=== Source files ===
diningBad.cvl (diningBad.cvl)


=== Command ===
civl verify -inputB=4 diningBad.cvl

=== Stats ===
time (s) : 1.61
memory (bytes) : 128974848
max process count : 3
states : 32
states saved : 26
state matches : 1
transitions : 30
trace steps : 21
valid calls : 104
provers : z3
prover calls : 3

=== Result ===
The program MAY NOT be correct. See CIVLREP/diningBad_log.txt