A Simple Method for Parameterized Verification of Cache Coherence Protocols 读书笔记

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

本文摘要出 A Simple Method for Parameterized Verification of Cache Coherence Protocols 的重要部分，对整体的知识框架作出总结，并融入了一些思考。

对于论文的代码及实现，可以在http://www.markrtuttle.com/fmcad08/里找到。或在文章下方给作者评论～比心❤️～

文章脉络

一句话概括

提出验证带参缓存一致协议安全性质的简单方法——模型抽象，最大限度的降低搜索范围

例子

  1. 任意多节点的 German如何用murphi和循环推理来验证

  2. Flash的简单验证，用simulation proofs间接证明了循环推理

（具体分析，详见下一节）

目标

带参验证 —— 不可判定问题

  • 最小化人工干涉
  • 最大化自动机／自动验证 —— 希望能提取出重要的信息，以供人来参考

优点

  • 可以被任意模型检验的工具使用。——对于缓存一致协议而言，显示状态模型检验比符号模型检测更好用，本文使用murphi语言
  • 易于理解。——基于仿真证明，来证明循环推理的有效性。
  • 不变式远远短于完整的归纳不变量。——这对于复杂协议非常重要
  • 模型检测完全搜索可达集的能力，被用于自动的推理独立节点的状态，并且被用于发现节点之间的重要交互。——给验证者建立正确的非干涉引理起到重要作用。
  • 已成功应用于German和Flash。——可靠性。

展望

  • 将该方法与其他带参验证相比较
    • 复合模型检测
    • 机器辅助定理证明
    • 谓词抽象模型
    • 不可见不变式
    • 截止定理（限界）

扩展（仅供参考，自己总结）：

  • 指明可改进的方向
    • 希望用自动推理机进行证明，而不是人工 —— 可实现
    • 希望自动生成初始的抽象版本 —— 可实现
    • 希望能自动通过反例，加强规则 —— 正在做

German

目标

检验不变式：

  • CtrlProp
1
2
3
4
invariant "CtrlProp"
	forall i: NODE do forall j: NODE do
		i != j -> (Cache[i].State = E -> Cache[j].State = I) & (Cache[i].State = S -> Cache[j].State = I | Cache[j].State = S)
		end;
  • DataProp
1
2
3
invariant "DataProp"
	( ExGntd = false -> MemData = AuxData ) & forall i : NODE do Cache[i].State != I -> Cache[i].Data = AuxData 
	end;

一般先检验控制逻辑（CtrlProp），再观察数据路径（DataProp）

建模

抽象

选择两个节点（对称性，所以具体是哪两个，没有影响） + 抽象节点

保持性质

  • 这三个节点能保持所有可能的状态（包括其他状态能对它们造成的影响）
  • 不变式能在这个抽象模型中得到检验

规则改变

  • 对于节点 = 被观察的两个节点时，规则不变
  • 对于Other，则去掉其状态的改变，及发出的请求，只关心其对于全局变量的改变（具体的抽象过程见论文Page5 第6点的b的5个小点）

反例

情景

节点n1发送ReqE，home接受并发送GntE。n1接受后置成E。 此时，节点n2发送ReqS，home知道有节点在E，所以发送Inv给n1，告诉它该送回数据了。但突然，此时有一个其他（这两个节点之外）的节点发送了一个InvAck给home，而home因为默认这个InvAck是n1给它的，所以没有进行判断，就给n2发了GntS，从而把n2置为S。这就违反了CtrlProp，因为这时系统中有一个E（n1），和一个S（n2）。

加强

通过这个反例，我们发现，当有节点处于E状态时，home不能从其他任何节点接受InvAck这个消息，因为这样会造成混淆。

看一下原来的这条规则：

1
2
3
4
5
rule "ABS_RecvInvAck"
	CurCmd != Empty & ExGntd = true
==>
	ExGntd := false; undefine MemData;
end;

经过加强，这条规则：

1
2
3
4
5
6
rule "ABS_RecvInvAck"
	CurCmd != Empty & ExGntd = true & forall j : NODE do
	Cache[j].State != E & Chan2[j].Cmd != GntE end
==> 
	ExGntd := false; undefine MemData;
end;

Cache[j].State != E很好理解，就是其他的节点都不能为E，但是Chan2[j].Cmd != GntE是有一点超前了。这是因为有可能那个本来不 为E的节点，正在接收GntE的消息，那它下一步就会置为E。所以，如果只加强检测其他节点是否状态为E，则无法检测到这种即将为E的情况。

加强抽象的规则

把出错的原因，放在抽象协议中的前提里。也就是说，因为发生过错误，不该执行某条规则时却执行了这条规则，导致违反了安全性质，所以现在增订了一条规定，说这个情况下不能这么执行。

具体见第八页Fig 3：

右边是新制定的规则，它的前提是左边原油的前提（左边黄色部分）& 原规则（没有抽象之前的）的RecvInvAck规则的前提。

建模启发

  1. 把选择语句，换成可判断的语句

比如，当需要用CurPtr来表示当前进程时，改成CurPtr = i的形式，然后用 i 做为索引。这样，就可以把CurPtr = i当作一个逻辑公式，具有真假值，可以判断对错。

  1. 找到反例，并且加强

比如，达到了某个违反安全性质的状态。首先观察这个状态为什么违反，然后再进行加强。加强的地方，不一定是执行的最后一条规则，有可能是之前执行序列中就埋下的伏笔。

结果

最终，通过6个反例，加强了抽象出来的German协议。

反思

初始的抽象模型是如何写出来的？ —— 可否自动化 —— 是否从murphi语言内部去改，还是纯文本地改写？

反例是如何找出来的？ —— 可否自动化地找

根据反例的加强，能否自动？

推理过程能否自动？ —— Isabelle定理证明机

证明过程

PS. 这是上面建模+找反例+加强协议 的形式化证明过程。写的不太详细，可以跳过。

形式化模型

卫式迁移模型 $M = (S, I, T)$

可达集：$R(M)$

不变式：$ P $ （ $R(M)\subseteq P\subseteq S$ ）

归纳不变式： $Q $ （$Q \rightarrow P$）归纳不变式比不变式强；R(M)一定是M的一个归纳不变式

所有的安全性质都能被缩减为不变式，只要通过增加辅助变量（比如AuxData）

模拟（Simulation）

如果M是原来的协议，$\tilde{M}$是抽象之后的协议。一个模拟(P, f) 由归纳不变式P，和抽象函数$f\in S \rightarrow \tilde{S}$组成。其中，这个函数满足：
$$
\forall s\in I:s\in P \wedge f(s) \in \tilde{I} \ \ \ \ \ \ (1)
$$

$$
\forall (s,s’)\in T: s\in P \Rightarrow s’\in P\wedge f(s,s’)\in \tilde{T} \ \ \ \ \ \ (2)
$$

（1）的意思是说，原来在M中的初始状态s，一定满足归纳不变式P，且经过f的映射，也一定在M～的初始状态中。（2）的意思是说，对于M中的迁移，只要规则的前断言满足P，则后断言也一定满足P；且这个迁移，经过f映射之后，也一定在M～的迁移规则集中。

定理1

$$
\forall s\in R(M):s\in P\wedge f(s)\in R(\tilde{M}) \ \ \ \ \ \ (3)
$$

也就是说，M中的可达状态s，都满足P（这个跟前面的定义一样），而且经过f的映射，也都会落在M～的可达集中。

进一步来看，也就是M，通过函数f（其实是反函数$f^{-1}$）继承了$\tilde{M}$中的不变式. 那么如果能在抽象模型中得到某个不变式，则在原来的模型中，就可以把M～中得到的不变式，通过f来反向推导出适用于M的不变式了。也就是打通了M和M～之间的不变式桥梁。

当然，要想想出一个归纳不变式，本身就很难。但是幸好有定理2。

定理2

首先看(6)，意思是说M中的s，经过f映射之后，都在M～中，即大模型的状态都能在抽象模型中找到对应。（4）（5）分别从初始状态和迁移规则做映射，保证了初始状态和规则都经过映射到达M～中，则可推出（6），即M的可达集都可以经过映射，抵达M～的可达集中。其中，$f^{-1}(R(\tilde{M}))$是M中的一个不变式。也就是把M～的可达集经过f反向映射回来之后，就是不变式。

要验证的东西是协议本身是否能够保证inv不被违反。有了inv之后，需要通过反例来对协议的一些推理规则进行加强。当然，是在有了抽象的模型之后，再进行加强。找到不对的地方，然后加强。

写在最后

其实证明过程我也没有怎么具体看懂，但是毕竟加强过程才是重点嘛，证明可以由自动机去证明，所以就重点关注如何加强抽象协议去了。

总的来说，它的基本思想有：

  • 参数可以取到很多，但是可以对抽象出来的节点造成的影响是有限的
  • 将所有可能的影响抽象成一个抽象节点，然后证明在这个抽象的协议中能够保持原来模型的安全性质
  • 证明过程实际上就是在证明：在抽象协议上穷举状态，证明安全的，也就意味着在带参协议中是安全的

目前的思考：

  • 所谓“寻找反例，逐步求精”，实际上是一种被动的寻找。是否能够化被动为主动，还需要进一步实验
  • 协议的抽象节点，人工做起来虽然挺快的，但是架不住规则多。所以还是找找方法，看是文本分析、还是转c之后用c来做，以实现直接自动抽象出抽象的规则。但是好像做出来之后用处也不是非常大？
  • 要怎样跟机器学习做结合，关键还是预处理