该博文主要用思维导图的方式，分析murphi验证互斥协议的流程。
互斥协议（murphi版）
互斥概念
最关键的思想就是控制临界区的使用情况，使得临界区不会因并发操作而造成混乱。
当多个进程需要读、写临界区的数据时，由于并发执行，则需要一个类似于锁的机制，来保证进入临界区的原子性和正确性。
状态迁移
代码结构分析
运行结果
代码
把进程数改成2，便于观察：
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
| const clientNUMS : 2; -- 设置成2，比较方便观察结果
type state : enum{I, T, C, E}; -- 4种进程的状态
client: 1..clientNUMS;
var n : array [client] of state; -- 存储各个进程状态的数组
x : boolean; -- 临界区的标志
ruleset i : client do -- 规则集，使得每个进程都都按照这个规则集运行
rule "Try" n[i] = I ==> begin
n[i] := T;endrule;
rule "Crit"
n[i] = T& x = true ==>begin
n[i] := C; x := false; endrule;
rule "Exit"
n[i] = C ==>begin
n[i] := E;endrule;
rule "Idle"
n[i] = E ==> begin n[i] := I;
x := true;endrule;
endruleset;
startstate -- 初始状态时，每个进程都是I状态。 临界区为“可申请”状态
begin
for i: client do
n[i] := I;
endfor;
x := true;
endstartstate;
ruleset i:client; j: client do -- 对于每2个进程之间，都满足该一致性协议
invariant "coherence"
i != j -> (n[i] = C -> n[j] != C);
endruleset;
|
运行结果
1
2
3
4
5
6
7
8
9
10
11
12
13
14
| State Space Explored:
12 states, 20 rules fired in 0.10s.
Rules Information:
Fired 2 times - Rule "Idle, i:1"
Fired 2 times - Rule "Idle, i:2"
Fired 2 times - Rule "Exit, i:1"
Fired 2 times - Rule "Exit, i:2"
Fired 2 times - Rule "Crit, i:1"
Fired 2 times - Rule "Crit, i:2"
Fired 4 times - Rule "Try, i:1"
Fired 4 times - Rule "Try, i:2"
|
其中，i的1，2为进程1和进程2。 Rule "Idle, i:1" 为对于进程1，执行rule ”Idle“
总结
这个程序能看到murphi对于并发执行程序的检验方式。