基于DivinE的分布式模型检测及协议验证
2016-08-17龙士工潘怀宇刘照祥
郑 涵，龙士工，潘怀宇，刘照祥
(贵州大学 计算机科学与技术学院，贵州 贵阳 550025)
基于DivinE的分布式模型检测及协议验证
郑涵，龙士工*，潘怀宇，刘照祥
(贵州大学 计算机科学与技术学院，贵州 贵阳 550025)
模型检测是一个高效且简单的方法来检测一个并发程序是否满足一个时序逻辑公式，它基于对系统状态空间的穷举搜索，通常采用深度优先搜索算法(DFS)。然而由于DFS算法固有的连续性，并且需要用到某些数据结构和同步机制，使得计算机的资源被大量的消耗，因此长期存在状态空间爆炸的问题。本文通过改进传统的DFS算法，利用DivinE工具，使状态空间爆炸问题能够在分布式环境下得到缓解。
模型检测；DFS；状态爆炸；分布式；DivinE
近年来，计算机技术进入高速发展的时代，人们对于计算机的应用需求也越来越高，为了保证计算机系统和网络更好地满足人们的要求，确保系统的正确性、安全性及活性等属性，我们需要对系统进行检测，找出系统存在的缺陷，并不断对其进行优化。模型检测(model checking)以其简洁明了和自动化程度高而引人注目。
模型检测是一个高效且简单的方法来检测一个并发程序是否满足一个时序逻辑公式，它主要检测有限状态程序，并把程序看成是一个结构，进而解释时序逻辑和评估公式，它比时序推论证明要简单得多，并且容易高效地实现。
模型检测的基本思想是用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型？”，用公式表示为S|=F？。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。
DivinE是最先进的模型检测工具之一，它主要是针对软件检测，而不是验证硬件是否能高效运行，通常用作协议一致性的辅助分析检测工具。DivinE既适合于单机系统，又适合于分布式并行系统。当它在单机系统下运行时，对系统状态空间的穷举搜索，采用传统的嵌套深度优先搜索算法；当它在分布式并行系统下运行时，对系统状态空间的穷举搜索，采用基于分布式的深度优先搜索算法。
1 传统的模型检测算法存在的问题
模型检测基于对系统状态空间的穷举搜索，通常采用深度优先搜索算法(DFS)。由于传统的深度优先搜索算法一直在单机环境下运行，所以长期存在空间状态爆炸的问题。所谓的状态爆炸问题，指的是对于并发系统，其状态的数目往往随并发分量的增长呈指数增长。因此当一个系统的并发分量较多时，直接对其状态空间进行搜索实际上是不可行的。
模型检测需要在一个状态迁移系统中检测是否存在可接受环，在过去传统的模型检测中，这个工作是由嵌套的深度优先搜索算法实现的(图1)。这个算法的正确性依赖于对状态空间的深度优先遍历。由于嵌套深度优先算法固有的连续性，并且需要用到某些数据结构和同步机制，使得计算机的资源被大量的消耗。对于现在大多数分布式环境来说，这是巨大的浪费，而且使用这种方法对某个算法的正确性进行形式化验证也是很不容易的。采用这种嵌套深度优先搜索算法将长期面临状态空间爆炸的问题。计算资源，特别是存储空间，是最主要的限制因素。
图1传统的嵌套深度优先搜索算法
2 分布式的模型检测解决状态空间爆炸的问题
随着软件的规模越来越大，解决的问题越来越复杂，空间状态爆炸的问题越来越突出，传统的并发式的模型检测技术已经不能满足软件生产的需要。由于时代的飞速发展，人们越来越热衷于追求高效率，再加上计算机硬件技术的不断革新，多核处理器的计算机越来越多，以及分布式技术的日趋成熟，这些都使得并行将成为程序设计以及算法设计的一大趋势。因为有效的并行算法可以使得计算速度成倍的提升，可以减少大量的计算时间。因而，在传统的模型检测中引入分布式并行的概念，可以使整个算法在计算速率上能有所提升，从而大大地缩短系统设计的设计周期，提高算法的工作效率。
在分布式模型检测方式下，状态空间被多个网络结点划分成多个部分，每个网络结点就是一个对性质进行验证的进程。一个划分函数将整个状态空间划分成多个等价类，使得这些环只存在于这些等价类之中。而环的检测也只在这些等价类中进行，无需多余的数据结构和同步机制。于是，状态空间将在网络结点中被分布式地遍历，每个网络结点拥有状态空间的一个子集，每个网络结点使用一个工作队列存储该结点中需要被访问的状态的集合。状态从这个工作队列中被提取出来，随后计算它的后继状态。如果这个后继状态属于其他的网络结点就会被送入相应网络结点中的工作队列中去；如果这个后继结点也属于该网络结点就会被遍历。当所有的网络结点空闲下来并且所有的工作队列为空的时候该分布式算法就结束了。当然，实现分布式模型检测的关键在于，将传统的嵌套深度优先搜索算法改进为能够适应分布式环境的分布式深度优先搜索算法(图2)。
图2 分布式深度优先搜索算法
图2给出了分布式嵌套深度优先搜索算法伪代码，算法假设全局状态空间已经被划分函数分成了多个等价类(SCC)，每个网络结点都执行相同的代码，每个网络结点拥有一个标识符my_pid，程序start()首先被执行，它初始化集合V用于保存访问过的状态结点和工作队列U，工作队列被设置成空除非某个结点里含有初始状态。随后程序visit()被唤醒，这个程序通过提取状态结点和唤醒程序dfs1管理工作队列，dfs1算法通过划分函数π去决定一个后继状态s是否被递归地遍历或是被送往另一个网络结点中。在嵌套的深度优先搜索算法中，当第一个DFS算法从某个已被访问过的可接受状态结点s原路返回时，第二个DFS算法(dfs2)就开始执行。这个状态结点s称为种子结点。此时，我们不能假设状态s的所有后继状态都被遍历了。由于一个强连通图中的所有状态属于同一个等价类，这说明从结点s出发是可达的，与s同属于一个强连通图的状态结点都被遍历过了。这个算法的正确性将在下一部分给出解释。由于不存在某个环同时存在于两个等价类中，所以第二个DFS算法(dfs2)仅仅遍历了与种子结点同属于一个等价类中的状态结点。
3 分布式深度优先搜索算法的正确性
上一部分给出的分布式嵌套搜索算法的正确性是假设全局状态空间已经被划分函数划分成多个强连通图。如果没有这个假设，这个算法有两大问题。首先，如果同一个SCC中的状态结点是被并行遍历的，则有可能出现环丢失的情况。如图3，如果一个嵌套搜索进程从状态A开始，访问并且标记了状态C，则另一个从状态B开始搜索的进程将无法检测出环B、C、D、B。
图3 并行嵌套搜索算法产生的问题
第二个问题出现的原因是环中的状态结点并不是按照深度优先序列进行遍历的，由于深度优先遍历序列没有保存，则一个从状态A开始的嵌套搜索进程仅仅能够访问到状态C，丢失了环C、D、B、C(图4)。
图4 非深度优先遍历序列产生的问题
如果假设一个环中的所有状态都属于同一个等价类，那么上述两个问题都避免了，因为同一个等价类中的状态结点是按照深度优先序列被连续地访问的。
我们用反证法说明这个问题，假设第二个搜索算法dfs2从第一个可接受状态s开始搜索并且丢失了一个已知存在的环。此时，环中至少存在一个被从s出发被dfs2访问标记过的状态结点。假设r是第一个这样的状态结点，dfs2从状态s′开始执行。由于dfs2对状态结点的遍历一直保持在同一个等价类中，所以s、r、s′属于同一个等价类，也就是π(s) =π(r) =π(s′)。按照我们的假设，dfs2从状态s′开始的搜索一定先于dfs2从状态s开始的搜索，那么就会有如下两种情况：
1)从状态s到状态s′是可达的。那么必然会存在一个环
2)从状态s到状态s′是不可达的。如果s′出现在一个环中，那么这个环在dfs2算法从状态s开始遍历之前就被丢失了。根据假设，s从r是可达的，于是s从s′也是可达的。因此，如果环中不包含s′，则在dfs1中，算法在第二次访问s′之前就会第二次访问s。由此算法dfs2一定是在从s′开始进行搜索之前从s开始进行搜索，这与假设矛盾。
在传统语文教学课堂中，教师往往将自我作为课堂中心，一味追求教学目标的实现，着重课堂内容的通读，往往忽视了学生的课堂学习进度。因此，要想提高教学课堂效率，就必须转变教学模式，将学生作为课堂主体，将课堂变成学堂而不是讲堂。首先，教师要反思教学方法，认清不足，做出相应措施；其次，教师可以通过开展课堂小组的学习模式，组织学生在课堂上通过小组间的讨论来进行对课文的学习，同时可展开多样化的小组间竞赛模式，激发学生的学习兴趣，大大提高课堂上的学习效率；最后，教师应充分了解学生的学习进度与状态，积极引导学生解决问题，同时培养学生敢于提问、积极思考的学习状态，进一步提高学生的学习效率。
综上所述，一个SCC中的状态结点是按照深度优先序列进行遍历的事实说明了分布式算法的正确性。因此，先前的推理仍然是满足的。
4 实验及运行结果
4.1peterson算法介绍
peterson算法是一个实现互斥锁的并发程序设计算法，可以控制两个进程访问一个共享的单用户资源而不发生访问冲突。该算法满足解决临界区问题的三个必须标准：互斥访问， 进入， 有限等待。
互斥访问：进程P0与P1显然不会同时在临界区: 如果进程P0在临界区内，那么P1只能在临界区外面等待，不能进入临界区。
进入：如果没有进程处于临界区内且有进程希望进入临界区， 则只有那些不处于剩余区的进程可以决定哪个进程获得进入临界区的权限，且这个决定不能无限推迟。剩余区是指进程已经访问了临界区，并已经执行完成退出临界区的代码，即该进程当前的状态与临界区关系不大。
有限等待：意味着一个进程在提出进入临界区请求后，只需要等待临界区被使用有上限的次数后，该进程就可以进入临界区。即进程不论其优先级多低，在该临界区入口处不应该出现死锁(deadlock)，这正是下面的实验即将验证的deadlock性质。
4.2采用传统模型检测方法在单机环境下验证peterson算法中的deadlock性质
图5试验结果一
根据结果显示，本次验证所花费的时间是6735秒，消耗的物理内存是184708字节。
4.3采用分布式模型检测方法在多机环境下验证peterson算法中的deadlock性质
操作系统：Linux 模型检测工具：DivinE 节点数：2(见图6)
图6试验结果二
根据结果显示，采用分布式模型检测在2台pc上验证同样的性质，花费的时间是5323秒，比单机环境节约了21%；平均消耗的物理内存是177040/2字节，比单机环境节约了52%。
5 结论
传统的DFS算法面临状态空间爆炸的问题。通过划分全局状态空间、将传统的嵌套深度优先搜索算法改进为分布式深度优先搜索算法，可以明显缩短模型检测消耗的时间和空间，从而缓解状态空间爆炸的问题。
[1] Lluch-Lafuente A. Simplified distributed model checking by localizing cycles[R]. Technical Report 176， Institute of Computer Science at Freiburg University， 2002.
[2] Informatics O. Distributed Memory LTL Model Checking[J].Programs-Abstracting the Context-Free Structure， Manuscript， Private communication， 2004， 164(2):9-14.
[3] Rockai P， Ceška M， Brim L， et al. DiVinE: Parallel Distributed Model Checker[C]// Parallel and Distributed Methods in Verification， 2010 Ninth International Workshop on， and High Performance Computational Systems Biology， Second International Workshop on. IEEE， 2010:4-7.
[4] Long S G， Yang H W. Modelling Peterson Mutual Exclusion Algorithm in DVE Language and Verifying LTL Properties[J]. Applied Mechanics & Materials， 2014，577:1012-1016.
(责任编辑：曾晶)
A Distributed Model Checking Based on DivinE and Protocol Verification
ZHENG Han， LONG Shigong*，PAN Huaiyu，LIU Zhaoxiang
(Couege of Computer Science and Technology， Guizhou University， Guiyang 550025， China )
Model checking is an effective and easy way to check if a concurrent program meets a sequential logical formula. Based on the exhaustive search of system state space， it usually adopts depth-first search algorithm (DFS). However， due to its continuity， it may need certain data structure and synchronization mechanism to consume lots of computer resources. Thus the problem of the explosion may exist in the state space. This problem was handled through the improvement of the traditional DFS algorithm via DivinE tools.
model checking； DFS； state explosion； distributed； DivinE
A
1000-5269(2016)03-0091-05
10.15958/j.cnki.gdxbzrb.2016.03.22
2015-11-24
国家自然科学基金(61163001)
郑涵(1990-)，男，在读硕士，研究方向：密码学与可信计算，Email：644144402@qq.com.
龙士工，Email：526796467@qq.com.
TP301
