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

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

(貴州大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，貴州 貴陽(yáng) 550025)

?

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

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

(貴州大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，貴州 貴陽(yáng) 550025)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4　實(shí)驗(yàn)及運(yùn)行結(jié)果

4.1peterson算法介紹

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

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

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

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

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

圖5試驗(yàn)結(jié)果一

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

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

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

圖6試驗(yàn)結(jié)果二

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

5　結(jié)論

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

[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

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

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

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

TP301