鄭　涵，龍士工，潘懷宇，劉照祥

(貴州大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，貴州 貴陽 550025)

?

基于DivinE的分布式模型檢測及協(xié)議驗證

鄭涵，龍士工*，潘懷宇，劉照祥

(貴州大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，貴州 貴陽 550025)

模型檢測是一個高效且簡單的方法來檢測一個并發(fā)程序是否滿足一個時序邏輯公式，它基于對系統(tǒng)狀態(tài)空間的窮舉搜索，通常采用深度優(yōu)先搜索算法(DFS)。然而由于DFS算法固有的連續(xù)性，并且需要用到某些數(shù)據(jù)結(jié)構(gòu)和同步機制，使得計算機的資源被大量的消耗，因此長期存在狀態(tài)空間爆炸的問題。本文通過改進傳統(tǒng)的DFS算法，利用DivinE工具，使?fàn)顟B(tài)空間爆炸問題能夠在分布式環(huán)境下得到緩解。

模型檢測；DFS；狀態(tài)爆炸；分布式；DivinE

近年來，計算機技術(shù)進入高速發(fā)展的時代，人們對于計算機的應(yīng)用需求也越來越高，為了保證計算機系統(tǒng)和網(wǎng)絡(luò)更好地滿足人們的要求，確保系統(tǒng)的正確性、安全性及活性等屬性，我們需要對系統(tǒng)進行檢測，找出系統(tǒng)存在的缺陷，并不斷對其進行優(yōu)化。模型檢測(model checking)以其簡潔明了和自動化程度高而引人注目。

模型檢測是一個高效且簡單的方法來檢測一個并發(fā)程序是否滿足一個時序邏輯公式，它主要檢測有限狀態(tài)程序，并把程序看成是一個結(jié)構(gòu)，進而解釋時序邏輯和評估公式，它比時序推論證明要簡單得多，并且容易高效地實現(xiàn)。

模型檢測的基本思想是用狀態(tài)遷移系統(tǒng)(S)表示系統(tǒng)的行為，用模態(tài)/時序邏輯公式(F)描述系統(tǒng)的性質(zhì)。這樣“系統(tǒng)是否具有所期望的性質(zhì)”就轉(zhuǎn)化為數(shù)學(xué)問題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個模型？”，用公式表示為S|=F？。對有窮狀態(tài)系統(tǒng)，這個問題是可判定的，即可以用計算機程序在有限時間內(nèi)自動確定。

DivinE是最先進的模型檢測工具之一，它主要是針對軟件檢測，而不是驗證硬件是否能高效運行，通常用作協(xié)議一致性的輔助分析檢測工具。DivinE既適合于單機系統(tǒng)，又適合于分布式并行系統(tǒng)。當(dāng)它在單機系統(tǒng)下運行時，對系統(tǒng)狀態(tài)空間的窮舉搜索，采用傳統(tǒng)的嵌套深度優(yōu)先搜索算法；當(dāng)它在分布式并行系統(tǒng)下運行時，對系統(tǒng)狀態(tài)空間的窮舉搜索，采用基于分布式的深度優(yōu)先搜索算法。

1　傳統(tǒng)的模型檢測算法存在的問題

模型檢測基于對系統(tǒng)狀態(tài)空間的窮舉搜索，通常采用深度優(yōu)先搜索算法(DFS)。由于傳統(tǒng)的深度優(yōu)先搜索算法一直在單機環(huán)境下運行，所以長期存在空間狀態(tài)爆炸的問題。所謂的狀態(tài)爆炸問題，指的是對于并發(fā)系統(tǒng)，其狀態(tài)的數(shù)目往往隨并發(fā)分量的增長呈指數(shù)增長。因此當(dāng)一個系統(tǒng)的并發(fā)分量較多時，直接對其狀態(tài)空間進行搜索實際上是不可行的。

模型檢測需要在一個狀態(tài)遷移系統(tǒng)中檢測是否存在可接受環(huán)，在過去傳統(tǒng)的模型檢測中，這個工作是由嵌套的深度優(yōu)先搜索算法實現(xiàn)的(圖1)。這個算法的正確性依賴于對狀態(tài)空間的深度優(yōu)先遍歷。由于嵌套深度優(yōu)先算法固有的連續(xù)性，并且需要用到某些數(shù)據(jù)結(jié)構(gòu)和同步機制，使得計算機的資源被大量的消耗。對于現(xiàn)在大多數(shù)分布式環(huán)境來說，這是巨大的浪費，而且使用這種方法對某個算法的正確性進行形式化驗證也是很不容易的。采用這種嵌套深度優(yōu)先搜索算法將長期面臨狀態(tài)空間爆炸的問題。計算資源，特別是存儲空間，是最主要的限制因素。

圖1傳統(tǒng)的嵌套深度優(yōu)先搜索算法

2　分布式的模型檢測解決狀態(tài)空間爆炸的問題

隨著軟件的規(guī)模越來越大，解決的問題越來越復(fù)雜，空間狀態(tài)爆炸的問題越來越突出，傳統(tǒng)的并發(fā)式的模型檢測技術(shù)已經(jīng)不能滿足軟件生產(chǎn)的需要。由于時代的飛速發(fā)展，人們越來越熱衷于追求高效率，再加上計算機硬件技術(shù)的不斷革新，多核處理器的計算機越來越多，以及分布式技術(shù)的日趨成熟，這些都使得并行將成為程序設(shè)計以及算法設(shè)計的一大趨勢。因為有效的并行算法可以使得計算速度成倍的提升，可以減少大量的計算時間。因而，在傳統(tǒng)的模型檢測中引入分布式并行的概念，可以使整個算法在計算速率上能有所提升，從而大大地縮短系統(tǒng)設(shè)計的設(shè)計周期，提高算法的工作效率。

在分布式模型檢測方式下，狀態(tài)空間被多個網(wǎng)絡(luò)結(jié)點劃分成多個部分，每個網(wǎng)絡(luò)結(jié)點就是一個對性質(zhì)進行驗證的進程。一個劃分函數(shù)將整個狀態(tài)空間劃分成多個等價類，使得這些環(huán)只存在于這些等價類之中。而環(huán)的檢測也只在這些等價類中進行，無需多余的數(shù)據(jù)結(jié)構(gòu)和同步機制。于是，狀態(tài)空間將在網(wǎng)絡(luò)結(jié)點中被分布式地遍歷，每個網(wǎng)絡(luò)結(jié)點擁有狀態(tài)空間的一個子集，每個網(wǎng)絡(luò)結(jié)點使用一個工作隊列存儲該結(jié)點中需要被訪問的狀態(tài)的集合。狀態(tài)從這個工作隊列中被提取出來，隨后計算它的后繼狀態(tài)。如果這個后繼狀態(tài)屬于其他的網(wǎng)絡(luò)結(jié)點就會被送入相應(yīng)網(wǎng)絡(luò)結(jié)點中的工作隊列中去；如果這個后繼結(jié)點也屬于該網(wǎng)絡(luò)結(jié)點就會被遍歷。當(dāng)所有的網(wǎng)絡(luò)結(jié)點空閑下來并且所有的工作隊列為空的時候該分布式算法就結(jié)束了。當(dāng)然，實現(xiàn)分布式模型檢測的關(guān)鍵在于，將傳統(tǒng)的嵌套深度優(yōu)先搜索算法改進為能夠適應(yīng)分布式環(huán)境的分布式深度優(yōu)先搜索算法(圖2)。

圖2　分布式深度優(yōu)先搜索算法

圖2給出了分布式嵌套深度優(yōu)先搜索算法偽代碼，算法假設(shè)全局狀態(tài)空間已經(jīng)被劃分函數(shù)分成了多個等價類(SCC)，每個網(wǎng)絡(luò)結(jié)點都執(zhí)行相同的代碼，每個網(wǎng)絡(luò)結(jié)點擁有一個標(biāo)識符my_pid，程序start()首先被執(zhí)行，它初始化集合V用于保存訪問過的狀態(tài)結(jié)點和工作隊列U，工作隊列被設(shè)置成空除非某個結(jié)點里含有初始狀態(tài)。隨后程序visit()被喚醒，這個程序通過提取狀態(tài)結(jié)點和喚醒程序dfs1管理工作隊列，dfs1算法通過劃分函數(shù)π去決定一個后繼狀態(tài)s是否被遞歸地遍歷或是被送往另一個網(wǎng)絡(luò)結(jié)點中。在嵌套的深度優(yōu)先搜索算法中，當(dāng)?shù)谝粋€DFS算法從某個已被訪問過的可接受狀態(tài)結(jié)點s原路返回時，第二個DFS算法(dfs2)就開始執(zhí)行。這個狀態(tài)結(jié)點s稱為種子結(jié)點。此時，我們不能假設(shè)狀態(tài)s的所有后繼狀態(tài)都被遍歷了。由于一個強連通圖中的所有狀態(tài)屬于同一個等價類，這說明從結(jié)點s出發(fā)是可達的，與s同屬于一個強連通圖的狀態(tài)結(jié)點都被遍歷過了。這個算法的正確性將在下一部分給出解釋。由于不存在某個環(huán)同時存在于兩個等價類中，所以第二個DFS算法(dfs2)僅僅遍歷了與種子結(jié)點同屬于一個等價類中的狀態(tài)結(jié)點。

3　分布式深度優(yōu)先搜索算法的正確性

上一部分給出的分布式嵌套搜索算法的正確性是假設(shè)全局狀態(tài)空間已經(jīng)被劃分函數(shù)劃分成多個強連通圖。如果沒有這個假設(shè)，這個算法有兩大問題。首先，如果同一個SCC中的狀態(tài)結(jié)點是被并行遍歷的，則有可能出現(xiàn)環(huán)丟失的情況。如圖3，如果一個嵌套搜索進程從狀態(tài)A開始，訪問并且標(biāo)記了狀態(tài)C，則另一個從狀態(tài)B開始搜索的進程將無法檢測出環(huán)B、C、D、B。

圖3　并行嵌套搜索算法產(chǎn)生的問題

第二個問題出現(xiàn)的原因是環(huán)中的狀態(tài)結(jié)點并不是按照深度優(yōu)先序列進行遍歷的，由于深度優(yōu)先遍歷序列沒有保存，則一個從狀態(tài)A開始的嵌套搜索進程僅僅能夠訪問到狀態(tài)C，丟失了環(huán)C、D、B、C(圖4)。

圖4　非深度優(yōu)先遍歷序列產(chǎn)生的問題

如果假設(shè)一個環(huán)中的所有狀態(tài)都屬于同一個等價類，那么上述兩個問題都避免了，因為同一個等價類中的狀態(tài)結(jié)點是按照深度優(yōu)先序列被連續(xù)地訪問的。

我們用反證法說明這個問題，假設(shè)第二個搜索算法dfs2從第一個可接受狀態(tài)s開始搜索并且丟失了一個已知存在的環(huán)。此時，環(huán)中至少存在一個被從s出發(fā)被dfs2訪問標(biāo)記過的狀態(tài)結(jié)點。假設(shè)r是第一個這樣的狀態(tài)結(jié)點，dfs2從狀態(tài)s′開始執(zhí)行。由于dfs2對狀態(tài)結(jié)點的遍歷一直保持在同一個等價類中，所以s、r、s′屬于同一個等價類，也就是π(s) =π(r) =π(s′)。按照我們的假設(shè)，dfs2從狀態(tài)s′開始的搜索一定先于dfs2從狀態(tài)s開始的搜索，那么就會有如下兩種情況：

1)從狀態(tài)s到狀態(tài)s′是可達的。那么必然會存在一個環(huán) 被丟失，否則算法就會終止。然而，這與我們假設(shè)第二個搜索算法dfs2從第一個可接受狀態(tài)s開始遍歷并且丟失了一個已知存在的環(huán)所矛盾。

2)從狀態(tài)s到狀態(tài)s′是不可達的。如果s′出現(xiàn)在一個環(huán)中，那么這個環(huán)在dfs2算法從狀態(tài)s開始遍歷之前就被丟失了。根據(jù)假設(shè)，s從r是可達的，于是s從s′也是可達的。因此，如果環(huán)中不包含s′，則在dfs1中，算法在第二次訪問s′之前就會第二次訪問s。由此算法dfs2一定是在從s′開始進行搜索之前從s開始進行搜索，這與假設(shè)矛盾。

在傳統(tǒng)語文教學(xué)課堂中，教師往往將自我作為課堂中心，一味追求教學(xué)目標(biāo)的實現(xiàn)，著重課堂內(nèi)容的通讀，往往忽視了學(xué)生的課堂學(xué)習(xí)進度。因此，要想提高教學(xué)課堂效率，就必須轉(zhuǎn)變教學(xué)模式，將學(xué)生作為課堂主體，將課堂變成學(xué)堂而不是講堂。首先，教師要反思教學(xué)方法，認(rèn)清不足，做出相應(yīng)措施；其次，教師可以通過開展課堂小組的學(xué)習(xí)模式，組織學(xué)生在課堂上通過小組間的討論來進行對課文的學(xué)習(xí)，同時可展開多樣化的小組間競賽模式，激發(fā)學(xué)生的學(xué)習(xí)興趣，大大提高課堂上的學(xué)習(xí)效率；最后，教師應(yīng)充分了解學(xué)生的學(xué)習(xí)進度與狀態(tài)，積極引導(dǎo)學(xué)生解決問題，同時培養(yǎng)學(xué)生敢于提問、積極思考的學(xué)習(xí)狀態(tài)，進一步提高學(xué)生的學(xué)習(xí)效率。

綜上所述，一個SCC中的狀態(tài)結(jié)點是按照深度優(yōu)先序列進行遍歷的事實說明了分布式算法的正確性。因此，先前的推理仍然是滿足的。

4　實驗及運行結(jié)果

4.1peterson算法介紹

peterson算法是一個實現(xiàn)互斥鎖的并發(fā)程序設(shè)計算法，可以控制兩個進程訪問一個共享的單用戶資源而不發(fā)生訪問沖突。該算法滿足解決臨界區(qū)問題的三個必須標(biāo)準(zhǔn)：互斥訪問， 進入， 有限等待。

互斥訪問：進程P0與P1顯然不會同時在臨界區(qū): 如果進程P0在臨界區(qū)內(nèi)，那么P1只能在臨界區(qū)外面等待，不能進入臨界區(qū)。

進入：如果沒有進程處于臨界區(qū)內(nèi)且有進程希望進入臨界區(qū)， 則只有那些不處于剩余區(qū)的進程可以決定哪個進程獲得進入臨界區(qū)的權(quán)限，且這個決定不能無限推遲。剩余區(qū)是指進程已經(jīng)訪問了臨界區(qū)，并已經(jīng)執(zhí)行完成退出臨界區(qū)的代碼，即該進程當(dāng)前的狀態(tài)與臨界區(qū)關(guān)系不大。

有限等待：意味著一個進程在提出進入臨界區(qū)請求后，只需要等待臨界區(qū)被使用有上限的次數(shù)后，該進程就可以進入臨界區(qū)。即進程不論其優(yōu)先級多低，在該臨界區(qū)入口處不應(yīng)該出現(xiàn)死鎖(deadlock)，這正是下面的實驗即將驗證的deadlock性質(zhì)。

4.2采用傳統(tǒng)模型檢測方法在單機環(huán)境下驗證peterson算法中的deadlock性質(zhì)

圖5試驗結(jié)果一

根據(jù)結(jié)果顯示，本次驗證所花費的時間是6735秒，消耗的物理內(nèi)存是184708字節(jié)。

4.3采用分布式模型檢測方法在多機環(huán)境下驗證peterson算法中的deadlock性質(zhì)

操作系統(tǒng)：Linux 模型檢測工具：DivinE 節(jié)點數(shù)：2(見圖6)

圖6試驗結(jié)果二

根據(jù)結(jié)果顯示，采用分布式模型檢測在2臺pc上驗證同樣的性質(zhì)，花費的時間是5323秒，比單機環(huán)境節(jié)約了21%；平均消耗的物理內(nèi)存是177040/2字節(jié)，比單機環(huán)境節(jié)約了52%。

5　結(jié)論

傳統(tǒng)的DFS算法面臨狀態(tài)空間爆炸的問題。通過劃分全局狀態(tài)空間、將傳統(tǒng)的嵌套深度優(yōu)先搜索算法改進為分布式深度優(yōu)先搜索算法，可以明顯縮短模型檢測消耗的時間和空間，從而緩解狀態(tài)空間爆炸的問題。

[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.

(責(zé)任編輯：曾晶)

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

國家自然科學(xué)基金(61163001)

鄭涵(1990-)，男，在讀碩士，研究方向：密碼學(xué)與可信計算，Email：644144402@qq.com.

龍士工，Email：526796467@qq.com.

TP301