Murphi入门（八）—— German协议解析

发表于 更新于 分类于 阅读次数：

本文讲述但不仅限于：

  • German协议流程分析
  • Murphi执行German协议注意要点

基本概念

German缓存一致性协议适用于共享内存的并发多处理器系统。

简单来说，整个系统抽象成三个部分：

  • cache：缓存器——分别为每个程序存储一个临时数据
  • home：通道管理器——管理cache读、写数据的并发发生
  • Memory：内存——存储数据，可提供读、写操作

根据数据流向，可以分为以下两部分：

  • 从内存流向cache：cache向home提出申请，要求读入mem中的数据
  • 从cache流向内存：cache对内存中存储的数据进行重写

作为管理者，home执行的职责主要有三个关键点：

  • 读可以共享
  • 写不可共享
  • 读写不可同时进行

而管理者的管理方法类似于三次握手，发送完消息之后，还需要等待对方回复，再执行下一步操作。当然，管理者还有两个个小本本，分别记录共享中的cache和无效中的cache，方便管理。

home还会记得当下是哪个cache在提出申请，以及申请的命令是什么，这就是CurPtr和CurCmd。

cache有三种状态：I（invalid）无效、S（share）读共享、E（Exclusive）写互斥。三种状态不能同时共存，且多cache的状态可以有多I，多S，但最多只能有一个E。

管理者与cache直接交流的方式是通过3个通道，每个通道可传递的消息不同：

  • chanel1: cache向home发送——sendReqS, sendReqEI, sendReqES
  • chanel2: home向cache发送——InvS, InvE, GntS, GntE
  • chanel3: cache向home发送——InvAck

还一个互斥变量，类似于锁机制，叫做ExGntd，是布尔变量，表示是否互斥。只有在写操作正在进行时，才会是true。这样保证一次只会有一个cache对内存进行写操作。

图解

如果看不懂了上述概念和流程，那么用一个直观的流程图来表示German协议的执行过程（例子为3cache模型）

规则解读

初始化

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
ruleset d: DATA do startstate "Init"
 for i: NODE do
   Chan1[i].Cmd := Empty;
   Chan2[i].Cmd := Empty; 
   Chan3[i].Cmd := Empty;   
   Chan1[i].Data := d;
   Chan2[i].Data := d; 
   Chan3[i].Data := d;   
   Cache[i].State := I;
   Cache[i].Data := d;
   ShrSet[i] := false;
   InvSet[i] := false;
  end;
  CurCmd := Empty;
  ExGntd := false;
  MemData := d;
  AuxData := d;
endstartstate; endruleset;

  • 所有cache：

    • 状态为I
    • 数据为1或2

  • 所有cache不共享，也不需要进行无效操作，所以ShrSet和InvSet都是false

  • 没有cache在申请操作，因此CurCmd为空，CurPtr未定义

  • 没有cache在进行写操作，因此ExGntd为false

执行结果：（执行方法见下一section）

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
Startstate Init, d:1 fired.
Cache[1].State:I
Cache[1].Data:1
Cache[2].State:I
Cache[2].Data:1
Cache[3].State:I
Cache[3].Data:1
Chan1[1].Cmd:Empty
Chan1[1].Data:1
Chan1[2].Cmd:Empty
Chan1[2].Data:1
Chan1[3].Cmd:Empty
Chan1[3].Data:1
Chan2[1].Cmd:Empty
Chan2[1].Data:1
Chan2[2].Cmd:Empty
Chan2[2].Data:1
Chan2[3].Cmd:Empty
Chan2[3].Data:1
Chan3[1].Cmd:Empty
Chan3[1].Data:1
Chan3[2].Cmd:Empty
Chan3[2].Data:1
Chan3[3].Cmd:Empty
Chan3[3].Data:1
ShrSet[1]:false
ShrSet[2]:false
ShrSet[3]:false
InvSet[1]:false
InvSet[2]:false
InvSet[3]:false
ExGntd:false
CurCmd:Empty
CurPtr:Undefined
MemData:1
AuxData:1
----------

通道1相关规则

  • SendReqS
  • SendReqEI
  • SendReqES
  • RecvReq

解读

cache向通道申请的内容包括：申请读、申请写。

I、S、E三种操作，互相转换的关系如图：

代码

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
ruleset j: NODE do
 rule "SendReqS"
      Cache[j].State = I & Chan1[j].Cmd = Empty ==> 
        begin Chan1[j].Cmd := ReqS;
endrule; endruleset;

ruleset i: NODE do
 rule "SendReqEI"
      (Cache[i].State = I) & Chan1[i].Cmd = Empty ==> 
        begin Chan1[i].Cmd := ReqE;
endrule; endruleset;

ruleset i: NODE do
 rule "SendReqES"
      (Cache[i].State = S) & Chan1[i].Cmd = Empty ==> 
        begin Chan1[i].Cmd := ReqE;
endrule; endruleset;

ruleset i: NODE do
 rule "RecvReq"
       CurCmd = Empty & Chan1[i].Cmd != Empty ==>
        begin CurCmd := Chan1[i].Cmd; 
              Chan1[i].Cmd := Empty;
              CurPtr := i;
              for j: NODE do
                InvSet[j] := ShrSet[j];
              endfor;
endrule; endruleset;

通道2相关规则

  • SendInvE
  • SendInvS
  • SendGntS
  • SendGntE
  • RecvGntS
  • RecvGntE

解读

通道2是home向cache发送命令的通道，主要用于

  • 使cache无效，发生情况有：
    • 某个cache想申请写内存，这时候其他cache必须无效
    • 某个cache想读内存中的数据，但这时候有其他cache正在写，这时候就要让那个正在写的cache带着现有的数据返回内存，并不再操作
  • 通过请求，告知申请的cache可以执行操作，发生的情况有：
    • 某个cache申请读操作，且现在没有cache正在写
    • 某个cache申请读操作，且现在没有在写和读的cache
  • cache收到home的确认，进行原来想要进行的操作，发生的情况有：
    • cache得到允许，可以读数据，且数据随通道带回来了
    • cache得到允许，可以写数据，且数据随通道带回来了

代码

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
49
50
51
52
53
54
55
56
57
58
59
ruleset i: NODE do
 rule "SendInvE"
      (CurCmd = ReqE)
      & InvSet[i] & Chan2[i].Cmd = Empty ==>
       begin
        Chan2[i].Cmd := Inv;
        InvSet[i] := false;
endrule; endruleset;
  
ruleset i: NODE do
 rule "SendInvS"
      (CurCmd = ReqS & ExGntd)
      & InvSet[i] & Chan2[i].Cmd = Empty ==>
       begin
        Chan2[i].Cmd := Inv;
        InvSet[i] := false;
endrule; endruleset;

ruleset i: NODE do
 rule "SendGntS"
      CurCmd = ReqS & CurPtr = i
      & !ExGntd & Chan2[i].Cmd = Empty ==>
      begin
       ShrSet[i] := true;
       CurCmd := Empty;
       Chan2[i].Cmd := GntS;
       Chan2[i].Data := MemData;
endrule; endruleset;

ruleset i: NODE do
 rule "SendGntE"
      CurCmd = ReqE & CurPtr = i & !ExGntd 
      & forall j: NODE do ShrSet[j] = false endforall
      & Chan2[i].Cmd = Empty ==>
      begin
       ShrSet[i] := true;
       CurCmd := Empty;
       ExGntd := true;
       Chan2[i].Cmd := GntE;
       Chan2[i].Data := MemData;
endrule; endruleset;

ruleset i: NODE do
 rule "RecvGntS"
      Chan2[i].Cmd = GntS ==>
      begin
       Cache[i].State := S;
       Chan2[i].Cmd := Empty;
       Cache[i].Data := Chan2[i].Data;
endrule; endruleset;

ruleset i: NODE do
 rule "RecvGntE"
      Chan2[i].Cmd = GntE ==>
      begin
       Cache[i].State := E;
       Chan2[i].Cmd := Empty;
       Cache[i].Data := Chan2[i].Data;
endrule; endruleset;

通道3相关规则

  • SendInvAck
  • RecvInvAck

解读

命令从cache流向home，用于确认之前收到的home传来的使无效命令。home因为有cache想申请写操作，或想申请读操作但有cache在写，所以要先使在读或在写的cache先无效。

  • SendInvAck：cache收到无效命令，如果正在读，就退出读状态；如果正在写，就退出写状态，且将数据由通道带回。
  • RecvInvAck：home收到cache从通道3带回来的回应，知道该cache已经无效了，如果此时没有其他的非无效cache，则可以继续；如果刚刚返回的cache是正在写的cache，则它返回时还会带着修改过的数据，则还需要将互斥锁解锁，再将数据写回内存。

代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
ruleset i: NODE do
 rule "SendInvAck"
      Chan2[i].Cmd = Inv & Chan3[i].Cmd = Empty ==>
      begin
       Chan2[i].Cmd := Empty;
       Chan3[i].Cmd := InvAck;
       if (Cache[i].State = E) then Chan3[i].Data := Cache[i].Data; end;
       Cache[i].State := I;
endrule; endruleset;

ruleset i: NODE do
 rule "RecvInvAck"
      CurCmd != Empty & Chan3[i].Cmd = InvAck ==>
      begin 
       ShrSet[i] := false;
       if (ExGntd = true) then 
        ExGntd := false; 
        MemData := Chan3[i].Data; 
       end;
       Chan3[i].Cmd := Empty;
endrule; endruleset;

Murphi执行German

常数

已有murphi程序，将cache数量设置成3，数据数量设置成2，即：

1
2
3
const
    NODE_NUM : 3;
    DATA_NUM : 2;

编译

将terminal的路径cd到german的murphi程序所在的地方，执行：

1
../../src/mu n_g2k.m

其中mu为murphi编译器，将murphi文件编译成cpp

再将cpp编译成.o：

1
g++ -ggbd -o n_g2k.cpp n_g2k.m -I ../../include -lm

之后就可以执行了

1
./n_g2k.o

注意

但是因为murphi设置的默认开辟的状态集（状态hash表）大小有限，所以此时会提示“too many active states”，提示我们无法遍历完所有的状态，并且告诉我们，总共需要322583k的大小。

也就是说，要想遍历完所有的状态，则需要加参数 -k或 -m。

所以执行：

1
./n_g2k.o -k322583

显示结果

但是这样执行完之后没有感觉，只有在执行了68.44s之后得出“no error found”的结果。如果想显示结果，可以加-ta 或 -tf 或-pr 或-p。

  • -ta： 输出所有状态至少一次
  • -tf： 所有状态只输出一次，且只输出与前一状态的改变量
  • -pr：会显示每一条规则执行几次，但无关顺序
  • -p： 从初始状态到最后，每一步都会详细展开，但是因为过于详细，所以占用空间太大

当设置了某个安全性质，想知道怎样最快到达该路径时，记得加参数-vdfs，这样就是深度优先，能够最快到达，否则默认的是广度优先。

最后的输出语句就成了：

1
./n_g2k.o -k322583 -ta -vdfs

结果输出

结果输出，有两种方式：

  • murphi自带：-d ./
  • 终端自带：>./trace.txt

但要注意，murphi自带的-d，是需要在编译的时候，就把它解析成哈希表模式，也就是在编译时：

1
../../src/mu -c n_g2k.m

加上参数-c，这样在后面.o文件执行的时候才不会报错。不过经试验，-d命令在Mac上并不使用得了，可能是murphi文件本身的问题，因为并没有报错。

如果在ubuntu下，会自动存储到./路径下的（该路径可修改，根据自己的需要自行修改）trace文件夹中。

终端自带的就没什么好说了，就是这个命令而已，路径也可以修改。

安全性质

可以通过加安全性质的方式，知道路径怎么运行，也就能更方便地知道规则是怎么执行的，就不用人工自己去判断了。

增添的方法是，写invariant。如：想知道什么时候cache会从状态I变到状态S，则设置安全性质为：

1
2
3
4
rulleset i:NODE do
	invariant "I2S"
		!Cache[i].State = S
	end;

那么，只要有一个Cache的状态变成S，就会break，并根据参数-ta，-vdfs，会进行深度优先的搜索，输出最短的到达该状态的一条路径。

多设置一些安全性质，就能比较清晰的知道该协议是怎样运行的了。

Tips

当然，如果当你没有对协议这么清楚的认识，只想先看看协议自己跑一下，可以通过调整参数-k的大小，来先看一些步骤。具体方法是：

1
./n_g2k.o -k100 -ta -vdfs

-k100是表示只开辟100k大小的状态表，这样不会跑到太多。-ta或者-tf都行，这样不会太繁琐，可以只看到改变的量，以及不会看到重复的状态。-vdfs是因为比较方便看运算的路径，毕竟人的思维比较习惯深度地思考，而广度的思考不利于理解协议。

总结

对于一个新拿到手的协议，可以先运行上一个section的Tips，跑着看看。等有了更深刻的认识之后，可以用安全性质来做测试。最后就是完全理解协议。当然，能有可视化的方法，就更好理解了。

目前正在思考有没有方法可以直接可视化。python里提供了一些画图工具，如matplot或者z3都可以画图。问题就是如何将murphi的一条条规则转换成图。如果针对全局变量进行迁移，最多可以生成类似以下的图。

但是如果希望生成这样的图

可能得先给出这样的图，然后根据-ta的输出，每次更改改变了的数据，最后将生成的一张张图进行视频合成输出，方可实现。

还是需要对python之类的工具有更深刻的理解和实践才能再有更多的想法呀。深深感到自己的心有余而力不足，加油努力吧～