八卦一下模型检验（二）

接着八卦前先回答老大们直指灵魂的问题。不就是系统状态遍历的问题么？干嘛非得用什么时序逻辑、模型一类的形式化手段啊？搞得比陈凯歌还深沉。做人不能这么无耻不是？找个真正的程序员，放出手里的蝴蝶不就搞定了？

<shapetype id="_x0000_t75" stroked="f" filled="f" path="m@4@5l@4@11@9@11@9@5xe" o:preferrelative="t" o:spt="75" coordsize="21600,21600"><stroke joinstyle="miter"></stroke><formulas><f eqn="if lineDrawn pixelLineWidth 0"></f><f eqn="sum @0 1 0"></f><f eqn="sum 0 0 @1"></f><f eqn="prod @2 1 2"></f><f eqn="prod @3 21600 pixelWidth"></f><f eqn="prod @3 21600 pixelHeight"></f><f eqn="sum @0 0 1"></f><f eqn="prod @6 1 2"></f><f eqn="prod @7 21600 pixelWidth"></f><f eqn="sum @8 21600 0"></f><f eqn="prod @7 21600 pixelHeight"></f><f eqn="sum @10 21600 0"></f></formulas><path o:connecttype="rect" gradientshapeok="t" o:extrusionok="f"></path><lock aspectratio="t" v:ext="edit"></lock></shapetype><shape id="_x0000_i1026" style="WIDTH: 6in; HEIGHT: 294pt" type="#_x0000_t75"><imagedata o:title="" src="file:///C:%5CDOCUME~1%5CADMINI~1%5CLOCALS~1%5CTemp%5Cmsohtml1%5C01%5Cclip_image001.png"></imagedata></shape>

嗯，很多程序的确可以靠程序达人强大的自觉和天才的排错能力搞定。问题是，模型检验的对象是高并发复杂系统（比如说10²⁰个状态），目标是绝对可靠地查出系统的错误，既不错杀三千，也不放过一个。这些系统失败时的代价也高昂。奔腾94年的FDIV错误花掉Intel至少5亿美元。偏偏我们对并发系统编程也没有什么特别有效的手段，不然大家也不至于对Heisenbug津津乐道了。我们在这种情况下怎么能全靠自己的直觉？何况直觉有时相当不可靠。在这篇让人崩溃的论文问世前，谁能想到在一个异步多进程拥有可靠网络的的分布系统中，哪怕一个出错的进程就能所有进程无法通过消息传递对一个值达成共识呢？当我们需要确保设计无错的时候，形式推理非常称手的工具。有些老大可能不知道，我们只所以能放心使用常用的数据结构和算法，多少也因为那些算法经过了严格的证明。当初Purely Functional Data Structure这本牛书值得一篇博士毕业论文，也是因为证明纯函数的数据结构的正确和性能颇费周折。另外，模型验证还在发展中，我们需要回答很多本质问题，比如模型验证到底能解决多大规模的问题，到底能具备什么样的效率，到底能处理什么样的系统。这些问题都需要高效而严格的推理。这个时候，形式化工具就派上用场了。

继续八卦。上次说到Pnuelli提出用时序逻辑描述系统的性质，打开了自动验证系统的方便之门。不过光有逻辑表达式没用，我们还需要系统。有了系统，我们才能给时序逻辑的断言赋予意义，才能进行推理和证明。比如说，LTL断言P -> F(S)本身并无意义，但如果我们知道这段公式描述的是公寓的电梯系统，P表示有人在一楼按了电梯按钮，而S表示电梯到达一楼，我们立刻知道这条断言的意思是当有人按了一楼的电梯后，一定会有电梯到达一楼，而且可以进一步根据电梯的设计来证明这条断言是否永远为真。接下来的问题自然是，怎么描述系统？显然直接上电路设计图或者程序代码并不现实。它们包含太多与系统验证无关的细节，实在不适合人肉推理。我们需要的是剥离了具体细节，但又能形式化描述系统本质的抽象东东，也就是切口所谓的模型。好比regex能匹配千奇百怪的字符串，但它的模型却是淳朴的有限自动机。把系统转换为这套形式化抽象描述的过程，叫建模。

模型验证里与时序逻辑配套的模型，叫Kripke Structure。Kripke Structure是CS里强大的工具，结构简单，却能简洁精准地描述各式并行系统。Kripke Structure由美国逻辑学家Saul Aaron Kripke于1963年前后提出。K老师是早慧天才。小学四年级读完莎士比亚全套戏剧后，就开始追问诸如“如何知道自己真实存在”这类恐怖问题。关于“我”的讨论是K老师毕生兴趣之一。这点和台湾陈老师相反。按理说儿童5岁（还是三岁？）前没有自我意识，所以不会用“我”自称，而用名字代替。比如二狗想吃冰淇淋，5岁前只会说“二狗想吃冰淇淋”，而5岁后说“我想吃冰淇淋”。偏偏知天命多年的陈老师专爱在群众大会上水扁长水扁短，声音还拖得忒长忒绵软。只能说品味与人囧异。当K老师问他爹“how do I know I’m not dreaming?”的时候，当犹太牧师的老爹告诉他，这个问题嘛，笛卡尔已经讨论过了。于是K老师从12岁起读笛老师的大部头，开始哲学研究，16岁就写出了关于模态逻辑的论文，讨论模态逻辑完备性定理。在哈佛上大二的时候就在MIT教研究生逻辑。著名的K Logic便是以他名字命名。K老师毕业后继续走天才路线，在抽象数学，哲学推理，主观句式，语言哲学，维特根斯坦的思想等方面贡献卓著，写了大量俺肯定看不懂的著作，包括对nature of being这种终极问题的深入讨论。K老师颇有人类早期哲人风范，不同于当代入世颇深的大牛们，比如萨特，罗素，或者乔姆斯基。他研究哲学的强大动力完全出自不可抑制的好奇心，跟现实彻底脱节。用K老师自己的话说，The idea that philosophy should be relevant to life is a modern idea. A lot of philosophy does not have relevance to life。

Kripke Structure本质是不确定性有限状态机，描述有限状态间的转换。它出彩的地方之一是形式化地定义了从状态到原子命题的映射，使得单个状态可用命题逻辑公式来描述。下面是一坨用Kripke Structure描述mutex的例子：

<shape id="_x0000_i1025" style="WIDTH: 6in; HEIGHT: 354pt" type="#_x0000_t75"><imagedata o:title="" src="file:///C:%5CDOCUME~1%5CADMINI~1%5CLOCALS~1%5CTemp%5Cmsohtml1%5C01%5Cclip_image003.png"><font size="3"></font></imagedata></shape>

这坨例子展示了Kripke Structure的要素：

• 原子命题（Atomic Proposition）。所谓原子命题，就是说该命题的值不依赖于其他命题。换句话说，原始命题表达式里不包含任何逻辑操作符。例子里的NC0，NC1, TRY0, TRY1, CS0, CS1都是原子命题。我们用原子命题来描述系统最基本的状态。比如NC0的意思是线程0没有进入critical section。原子命题的集合叫AP，也就是Atomic Proposition的缩写。
  
  
• 状态。每个圆角方框代表一坨状态。上面例子有八坨状态，从S0到S8。一个状态可以用多条原子命题描述。比如说状态S0满足两条命题：NC0和NC1。
  
  
• 状态转移。状态转移用有向箭头表示。比如S0到S1的箭头表示状态能够从S0转换到S1。反过来说，S1不能直接转移到S0，所以没有S1到S0的箭头。状态间的转移也表示时间的改变。比如从S0到S1表示我们假想的离散时间前进了一格。
  
  
• 标签函数。我们怎么知道某个状态满足哪些命题嗫？这个就要靠标签函数了。标签函数把状态映射到AP的幂集，2^AP。换句话说，任意状态可能满足AP中任意命题的组合。如果AP={P, Q, S}，那一个状态可能满足的组合就是{F}，{P}, {Q}, {S}，{P, Q}, {P, S}, {Q, S}, {P, Q, S}。

有了这些基本概念，我们就能理解这托例子展示了mutex 系统里两枚线程获取及释放critical section的过程：

• 状态S0表示两条线程都没有占用critical section。NC0表示线程0在non-critical section。NC1表示线程1在non-critical section。
• 状态S1表示线程0开始试着获取critical section，而线程1还在non-critical section。
• 状态S2表示线程1试图进入critical section， 而线程0还在non-critical section。
• 系统可以保持S0的状态，也可以进入S1或者S2。
• 状态S3表示线程0和线程1同时试图进入critical section。
• 状态S4表示线程0进入critical section, 而线程1还在non-critical section。
• 状态S5表示线程0和线程1都试图进入critical section。
• 状态S6表示线程0在non-critical section，而线程1进入了critical section。
• 状态S7表示线程0还在critical section的时候，线程试图进入critical section。
• 状态S8表示线程0试图进入critical section，而线程1还在critical section内。
  
  

有了直观的解释，Kripke Structure的形式化表述就容易理解了。另外形式化表述也是必要的。除了研究Kripke Structure的性质以外，我们的代码也建立在形式化表达的基础上。

Kripke Structure 被定义为在给定原子命题集合AP基础上的4-tuple K = （I, S, R, L）。I是初始状态的集合。S是有限状态的集合。R是状态关系函数，R ` R % R。R必须是完全函数。也就是说对状态集合里的任意状态s来说，R(s)必须是S里一个元素。换句话说，任何一个状态都必须有条向外的箭头。这同普通状态机不同。而L则是标签函数，把状态映射到AP的幂集，L : S -> 2^AP。上面例子的形式表述就是：

• I = {S0}
• S = {S0, S1, S2, S3, S4, S5, S6, S7, S8}
• R = {(S0, S0), (S0, S1), (S0, S2), (S1, S4), (S1, S3), (S2, S5), (S2, S6), (S4, S7), (S4, S0), (S3, S7), (S3, S2), (S5, S8), (S6, S8), (S6, S0), (S8, S1)}
• L(S0) = {NC0, NC1}, L(S1) = {TRY0, NC1}, L(S2) = {NC0, TRY1}, L(S3) = {TRY0, TRY1}, L(S4) = {CS0, NC1}, L(S5) = {TRY0, TRY1}, L(S6) = {NC0, CS1}, L(S7) = {CS0, TRY1}, L(S8) = {TRY0, CS1}
  
  

有了Kripke Structure描述的模型，就可以开始考察系统的性质了。任何一坨mutex系统都需要满足一些基本性质：

1. 任何时候线程0与线程1都不能同时进入critical section。这是critical section的基本要求，不然基于加锁的多线程也没法玩儿了。用LTL描述一下：

• 线程0进入critical section用CS0表示。线程1进入critical section用CS1表示。那两坨线程同时进入critical section自然是CS0 . CS1
• 两者不能同时进入critical section，无非是对上面的陈述取反。所以我们得到 × (CS0 . CS1)
• 表示“任何时候“的操作符是G，所以我们得到了最终的表达式：G(× (CS0 . CS1))

这是所谓的安全特性(safety property)，用来确定某些情况任何时候都不会发生。我们的mutex系统明显满足该性质，因为例子里的每坨状态最多有CS0和CS1中的一项。

1. 有了安全性质不够，还应该有活性性质(liveness property)，也就是某些特性最终应该发生。比如说，当线程0要进入critical section，它最终一定能进入。这条也很重要，不然我们就遇到死锁或活锁了。形式化的过程就省略了，反正也不难。最终公式是G(TRY0 -> F(CS0))。我们的例子也满足这坨公式。线程0试图进入critical section的状态包括S1, S3, S5, S8。从这些状态出发，我们总能找到一条路径，到达包含CS0的状态。比如说S1->S4, S3->S7, S5->S8->S1->S4, S8->S1->S4。
   
   
2. 马斯洛爷爷说了，光有安全需求和生理需求是不够滴。人不能苟活着。我们还需要健康的激励，而激励的基石之一就是公平（fairness property）：如果线程0无限次试图进入critical section，它就能无限次进入critical section。按需分配的共产狂想性质啊：GF(TRY0) -> GF(CS0)（fairness也有好多种。我们这里谈的是强公平）。这坨公式其实也好理解。F(TRY0)表示TRY0在未来某个时候会发生。GF(TRY0)就表示从任何时刻算起，TRY0都能发生，也就是可以无限次发生的意思。这和big-O或者极限的定义里表达无限逼近的手段相似。显然我们的mutex系统也满足这条性质。只要TRY0出现也就是线程0试图进入critical section，系统肯定进入状态S1，而进入状态S1后，不管哪条路径都导致包含CS0的状态。也就是说，只要TRY0无限次出现，CS0也无限次出现。这样的路径也有个名堂，叫公路，也即公平路径(fair path)的简称。

从上面简单例子可以看出模型检验的套路：

1. 用Kripke Structure建立系统模型。
2. 用时序逻辑公式描述我们期望的系统性质
3. 证明这些公式在第一步建立的Kripke Structure上永远为真。上面的例子只给出了正确公式的演示。其实更绝妙的是当系统有错的时候，模型检验不仅能查出错误，还能给出生成错误的执行路线，也就是反例。这些反例往往比人肉查错来得短小。在某些情况下，模型检查甚至可以保证生成最短小的反例。
   

对于简单例子，我们可以做如上人肉分析，再配上大批公式和所有希腊字母唬人。可惜真正的系统动辄成千上万甚至上亿状态（这也是为什么Dijkstra倡导的人肉证明行不通的原因之一），手工证明代价过于高昂。幸好Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis等人发明了一系列算法，让模型验证彻底自动化。算法的大体思路其实相当粗暴：遍历模型也就是Kripke Structure所有可能的执行路线，看他们是不是全部满足时序逻辑描述的性质。如果不满足，则打印出使验证失败的路径。真正有意思的是怎么遍历和组织数据。而这，才是模型检验魔力所在。我们交代了模型，下面就可以聊精彩的算法了。