基于SPIN的Linux管道模型檢測研究

速昱行 ，王金波

（1.中國科學(xué)院大學(xué)北京100190；2.中國科學(xué)院空間應(yīng)用工程與技術(shù)中心北京100094）

為了適應(yīng)航天事業(yè)的快速發(fā)展，完成繁雜的空間任務(wù)，對嵌入式軟件系統(tǒng)的可靠性、穩(wěn)定性等提出了更高的要求，Linux作為一款開源、可裁剪、可移植的操作系統(tǒng)逐漸被應(yīng)用于國內(nèi)外航天嵌入式領(lǐng)域。

對于航天任務(wù)而言，其特殊性決定了必須在研制階段就確保星載嵌入式軟件的可靠性，否則可能會造成災(zāi)難性的后果。例如，1997年火星“探路者”號在執(zhí)行任務(wù)時，遇到系統(tǒng)頻繁重啟問題；1996年歐洲航天局發(fā)射的一架未載人的阿麗亞娜5號火箭，在發(fā)射升空40秒鐘之后發(fā)生了爆炸。因此，對操作系統(tǒng)進(jìn)行分析和驗證是至關(guān)重要的。目前，對于操作系統(tǒng)的測試驗證工作，尚無明確的標(biāo)準(zhǔn)和規(guī)范，主要的方法有以下幾種[1-5]：

1）通過各種系統(tǒng)調(diào)用測試內(nèi)核功能的安全性和正確性；

2）通過第三方的測試套件（工具）對內(nèi)核進(jìn)行測試；

3）各種性能測試，如實時性測試等。

針對已有測試手段只能盡可能多的找出錯誤和缺陷，形式化驗證通過對系統(tǒng)所有行為狀態(tài)的模擬，可以在早期便徹底的檢測系統(tǒng)是否還存在其他問題。模型檢測作為形式化驗證的其中一支于近年來成功地應(yīng)用在了通用操作系統(tǒng)的分析和驗證中[4]，特別是與數(shù)字電路和通信協(xié)議有關(guān)的設(shè)計中。同時進(jìn)程間通信（IPC）對操作系統(tǒng)的重要性不言而喻，因此對其進(jìn)行模型檢測非常有意義，也成為一個研究模型檢測對操作系統(tǒng)驗證的切入點。

1 模型檢測和SPIN概述

形式化驗證是基于用形式化語言描述的規(guī)格（specification）之上進(jìn)行模型（model）分析和驗證，從而發(fā)現(xiàn)系統(tǒng)中存在的不一致性、歧義性、不完整性和競態(tài)條件的方法。其主要手段包括模型檢測和定理證明。前者的應(yīng)用范圍限定在有限狀態(tài)并發(fā)系統(tǒng)上，可以在有限的時間和空間內(nèi)完全自動運行和終止；后者則被用于無限狀態(tài)的推理，但只有其中一部分可以自動進(jìn)行，但即使驗證性質(zhì)為真，卻可能需要無限大的時間和內(nèi)存。因此模型檢測應(yīng)用場景更加廣泛，可以用在中等規(guī)模的計算機上運行[4]。

模型檢測將建立的系統(tǒng)模型及性質(zhì)作為檢測工具的輸入，一般通過深度優(yōu)先遍歷的方式進(jìn)行狀態(tài)空間搜索，從而判斷屬性正確與否。目前已經(jīng)開發(fā)出的模型檢測工具有很多[5]，如SMV、SPIN、JPF、Isabelle/HOL、MOPS等。模型檢測一般經(jīng)過以下3個步驟：

1）建?！橄竽Ｐ吞崛∫约稗D(zhuǎn)化為能被檢測工具接受的形式；

2）刻畫——聲明模型需要滿足的性質(zhì)；

3）驗證——分析驗證結(jié)果（錯誤軌跡）。

本文工作主要基于SPIN，其最大特點是采用了偏序規(guī)約、on the fly等技術(shù)[8]，從而狀態(tài)空間的數(shù)目得以縮減，提高了檢測效率。它的建模語言為Promela，可以用線性時態(tài)邏輯（LTL）和斷言（assertion）來聲明系統(tǒng)屬性，支持隨機、交互式和引導(dǎo)式模擬。SPIN的每個進(jìn)程都被看作有限狀態(tài)自動機來建模，實際并發(fā)系統(tǒng)的全局行為就通過計算這些自動機的異步交錯積來得到：1）對LTL公式刻畫的系統(tǒng)性質(zhì)取反，得到Büchi自動機P；2）計算系統(tǒng)中每個進(jìn)程的轉(zhuǎn)移子系統(tǒng)的乘積，建立Büchi自動機S，得到模型代表的系統(tǒng)的全局行為；3）計算P與S的乘積；4）檢查最后乘積得到的自動機，若其所能接受的語言為空，則表示系統(tǒng)滿足所描述的性質(zhì)，反之說明系統(tǒng)不滿足原本定義的屬性要求。具體在軟件中操作的過程如圖1直觀所示，證明時序邏輯公式φ是否在模型M中成立（即證明M|=φ）。

圖1 SPIN模型檢測過程

Promela是SPIN的建模語言，其中包括的抽象對象有變量、消息、通道、進(jìn)程、遷移和全局系統(tǒng)狀態(tài)。消息通道支持會面點（rendezvous）或緩沖的（buffered）消息傳遞方式，實現(xiàn)同步或者異步通信。

2 Linux管道的分析驗證

2.1 管道的描述

在Linux中，處于用戶空間的進(jìn)程擁有各自的地址空間，一般無法互相訪問。然而多數(shù)場景下需要進(jìn)程間進(jìn)行相互通信，以完成系統(tǒng)的某些功能，如數(shù)據(jù)傳輸、數(shù)據(jù)共享、消息通知、進(jìn)程控制等[7]。進(jìn)程通過與內(nèi)核及其它進(jìn)程之間的互相通信來協(xié)調(diào)各自的行為。管道屬于IPC中一種使用頻率較高的通信手段，有匿名管道和命名管道之分。前者只能在父子進(jìn)程或者兄弟進(jìn)程之間使用，而后者打破了這種限制，提供了文件的路徑來識別管道，從而實現(xiàn)在沒有親緣關(guān)系的進(jìn)程之間通信，本文僅討論匿名管道。管道從本質(zhì)上說也是文件的一種，但它又和普通的文件有所區(qū)別，它是內(nèi)核中一個大小固定的緩沖區(qū)。其具體實現(xiàn)的源代碼位于＜fs/pipe.c>中，創(chuàng)建過程如圖2所示。

圖2 管道創(chuàng)建過程

1）父進(jìn)程通過調(diào)用int pipe（int fd[2]）創(chuàng)建管道，這里得到的兩個文件描述符fd[0]、fd[1]，分別指向管道的讀端和寫端，此時讀端和寫端皆指向父進(jìn)程；

2）父進(jìn)程通過調(diào)用fork（）創(chuàng)建子進(jìn)程，子進(jìn)程拷貝了父進(jìn)程除某些資源之外的所有內(nèi)容，包括上一步創(chuàng)建的管道，即子進(jìn)程也有兩個文件描述符指向同一管道；

3）隨后，父進(jìn)程關(guān)閉讀端，子進(jìn)程關(guān)閉寫端，則前者向管道中寫入數(shù)據(jù)，而后者就可以將管道中的數(shù)據(jù)讀出，這樣就實現(xiàn)了進(jìn)程間通信。

管道使用的過程中可能會面臨問題有：緩沖區(qū)的溢出，即當(dāng)要寫入的數(shù)據(jù)大于緩沖區(qū)大小時，數(shù)據(jù)的丟失；阻塞問題，讀寫進(jìn)程在未滿足自身讀寫要求時，可能會陷入死等狀態(tài)；還有管道破裂，即讀寫進(jìn)程關(guān)閉不一致的情況；以及數(shù)據(jù)寫入可能不保證原子性等等。文獻(xiàn)[13]提出了一種建模方法，本文針對其中的疏漏和不完善進(jìn)行了研究和改進(jìn)。

2.2 管道的建模

根據(jù)管道通信思想和源代碼的研讀，結(jié)合SPIN的使用特點，用有限狀態(tài)自動機（FSA）描述模型。將管道、管道讀端以及寫端看作3個實體，建立3個相應(yīng)的FSA，3個實體的交互，必然涉及到消息傳遞以及共享變量狀態(tài)改變，加上遷移條件的復(fù)雜性和耦合性，加大了建模的難度。文獻(xiàn)[13]中的模型存在如下等問題：只使用了全局變量，遷移關(guān)系不完整，模型粒度不夠細(xì)化以及模型耦合關(guān)系復(fù)雜，現(xiàn)介紹另外一種改進(jìn)方案。

2.2.1 管道模型

在Linux中，管道的實現(xiàn)并沒有使用專門的數(shù)據(jù)結(jié)構(gòu)，而是借助了文件系統(tǒng)的file結(jié)構(gòu)和虛擬文件系統(tǒng)的索引節(jié)點inode。在此不展開探討，僅僅對其抽象狀態(tài)進(jìn)行討論。管道通過系統(tǒng)調(diào)用pipe（）創(chuàng)建后，可進(jìn)行讀寫操作，此時通過同步管道內(nèi)容管道進(jìn)行進(jìn)程間通信。在此期間，管道狀態(tài)可能是寫狀態(tài)或者是讀狀態(tài)，而且在讀寫端都未正式結(jié)束前，管道的狀態(tài)可能在兩個狀態(tài)間相互轉(zhuǎn)化。當(dāng)讀者或者寫者結(jié)束時，管道進(jìn)入預(yù)關(guān)閉狀態(tài)，直到?jīng)]有讀者和寫者，管道正式關(guān)閉。期間，若讀者提前退出，寫者還未完成，則管道破裂。如果缺少了管道讀寫狀態(tài)這一相互轉(zhuǎn)化的重要過程，也就是說，管道創(chuàng)建以后只能進(jìn)行單一的讀或者寫，這與實際情況是不符合的。

同時，盡管單獨把管道抽象成為一個實體，但其狀態(tài)變遷主要是依據(jù)讀寫端的狀態(tài)變化完成，而不是管道主動變遷的結(jié)果，因此讀寫端的操作指令應(yīng)當(dāng)存在讀寫端所代表實體中，而不是作為管道狀態(tài)的觸發(fā)條件。這樣的設(shè)計使實體間交互關(guān)系更加清楚，耦合性降低，同時也更符合設(shè)計邏輯。具體的過程見圖3所示。

圖3 管道模型

2.2.2 管道讀端

如果某個進(jìn)程要讀取管道中的數(shù)據(jù)，那么該進(jìn)程應(yīng)當(dāng)及時關(guān)閉fd[1]，以避免意外錯誤的發(fā)生。讀端進(jìn)程通過調(diào)用read（）系統(tǒng)調(diào)用讀取管道內(nèi)容，讀端實體進(jìn)入READ狀態(tài)，此時分兩種情況，阻塞方式（NOBLOCK==0）和非阻塞方式讀取（NOBLOCK==1）。

阻塞方式下：

1）如果管道中有數(shù)據(jù)（len>0）并且請求數(shù)據(jù)rdata不為0時，read操作時返回能夠讀取到的字節(jié)數(shù)。請求數(shù)據(jù)大于管道容量的，則返回管道中現(xiàn)有所有數(shù)據(jù)len；若請求字節(jié)數(shù)不大于管道容量，則返回現(xiàn)有所有數(shù)據(jù)或者請求的字節(jié)數(shù)；

2）如果管道中數(shù)據(jù)為0并且請求數(shù)據(jù)不為0時，若寫端文件描述符未關(guān)閉則進(jìn)入等待狀態(tài)WAIT；

3）若管道中數(shù)據(jù)為0，寫端文件描述符關(guān)閉，則返回0，進(jìn)入結(jié)束狀態(tài)FINISH；

4）阻塞等待的讀端進(jìn)程在管道有數(shù)據(jù)寫入時再次進(jìn)入讀取狀態(tài)READ；

5）當(dāng)請求數(shù)據(jù)讀取完成后，進(jìn)入完成FINISH狀態(tài)。

非阻塞方式下：

1）如果管道中有數(shù)據(jù)并且請求數(shù)據(jù)不為0時，read操作時返回能夠讀取到的字節(jié)數(shù)；

2）若管道中數(shù)據(jù)為0，若管道寫端被關(guān)閉，則返回0；若寫端未關(guān)閉則返回-1；進(jìn)入FINISH狀態(tài)。

讀取結(jié)束，文件描述符關(guān)閉后，讀者計數(shù)器置0。具體的變遷過程如圖4所示。

圖4 管道讀端模型

2.2.3 管道寫端

因為緩沖區(qū)大小固定，管道寫端的情況相對更加復(fù)雜。寫進(jìn)程寫入數(shù)據(jù)前需要關(guān)閉讀端，即close（fields[0]）。當(dāng)寫進(jìn)程向管道中寫入時，它利用標(biāo)準(zhǔn)的庫函數(shù)write（），系統(tǒng)根據(jù)庫函數(shù)傳遞的文件描述符，可找到該文件的file結(jié)構(gòu)。file結(jié)構(gòu)中指定了用來進(jìn)行寫操作的函數(shù)（即寫入函數(shù)）地址，同時需要滿足管道沒有被讀進(jìn)程占用。寫進(jìn)程進(jìn)入數(shù)據(jù)寫入狀態(tài)時，同樣分為阻塞和非阻塞兩種情況。

阻塞情況下：

1）只有緩沖區(qū)未滿的情況下，才能寫入數(shù)據(jù)。當(dāng)寫入數(shù)據(jù)wdata小于管道總長度buf時，保證寫入的原子性atomic，如果此時當(dāng)前可容納長度小于寫入數(shù)據(jù)時，寫進(jìn)程進(jìn)入阻塞狀態(tài)WAIT，直到可以一次性寫入；而當(dāng)寫入數(shù)據(jù)大于管道總長度時，不再保證寫入過程的原子性，只要管道未滿，就寫入數(shù)據(jù)，否則進(jìn)入阻塞狀態(tài)WAIT直到數(shù)據(jù)寫完；

2）當(dāng)數(shù)據(jù)寫入完畢，進(jìn)入FINISH狀態(tài)；

非阻塞情況下：

1）同樣也只有在管道未滿狀態(tài)下寫入數(shù)據(jù)。當(dāng)寫入數(shù)據(jù)wdata小于管道總長度buf時，保證寫入原子性，如果當(dāng)前可容納長度大于寫入長度，則一次性寫入，否則直接返回；

2）當(dāng)寫入數(shù)據(jù)wdata大于管道總長度buf時，若管道未滿，則寫入可容納數(shù)據(jù)；若管道已滿則返回錯誤；

在寫入過程中，如果讀端完畢，關(guān)閉了文件描述符，則管道宣布破裂，產(chǎn)生信號SIGPIPE，返回-1。具體如圖5所示。

圖5 管道寫端模型

2.2.4 模型的Promela描述

3個實體分別為進(jìn)程

各進(jìn)程初始狀態(tài)分別為

對用到的狀態(tài)作枚舉說明

mtype={UNCREATED， CREATED， IsREAD，WRITTEN，ReadyCLOSE，BROKEN，CLOSE，UNWRITE，UNREAD，READ，WRITE，WAIT，F(xiàn)INISH}。

限于篇幅，同樣以管道部分Promela代碼為例，如圖6。新的建模方法中，管道部分加入了WRITTEN和READ狀態(tài)的相互轉(zhuǎn)化，同時剝離了管道和讀寫端的操作聯(lián)系，狀態(tài)遷移僅由讀寫端狀態(tài)和文件描述符狀態(tài)（讀寫端計數(shù)）給出，如下：

同時由于管道狀態(tài)與讀寫端進(jìn)程是同步關(guān)系，定義消息通道

mtype為枚舉類型，代表讀寫端狀態(tài)；byte代表讀寫端計數(shù)，即文件描述符。這樣的做法使管道狀態(tài)與讀寫端進(jìn)程更能保持同步變化，比單純用全局變量更加精確，全局變量在SPIN中并不能保證同步。

對讀寫端，為了減少狀態(tài)數(shù)，read和write操作返回值不同的情況將由打印信息printf（）給出，但都?xì)w為FINISH狀態(tài)。提高了程序可讀性，減少了模型檢測過程中系統(tǒng)的存儲狀態(tài)數(shù)，從而模型的復(fù)雜程度也得到簡化。

增加和細(xì)化的遷移條件，使新模型更加完善；對原建模方法當(dāng)中的錯誤遷移條件進(jìn)行了勘誤，如讀寫端進(jìn)程是先結(jié)束，再關(guān)閉文件描述符，計數(shù)減少。

圖6 管道Promela部分代碼

3 實驗結(jié)果分析及改進(jìn)

實驗中，屬性用LTL表達(dá)式進(jìn)行描述，作為SPIN的輸入。

1）首先，是其有界性。即管道數(shù)據(jù)長度len，不能超過管道總長度buf，否則將會導(dǎo)致緩沖區(qū)溢出。用 ltl公式描述為 ltl p1{[]（len ＜ =buf）}，[]表示always。檢測結(jié)果表明性質(zhì)滿足。

圖7 ltl屬性驗證

2）其次，驗證讀寫端不能同時占用管道，即讀端狀態(tài)為READ，寫端狀態(tài)為WRITE。用ltl公式描述 為 ltl p2{[]!（Reader_State==READ&&Writer_State==WRITE）}。

檢驗的結(jié)果表明，系統(tǒng)不滿足性質(zhì)，經(jīng)過反例查驗，Reader_State==READ和Writer_State==WRITE可以同時成立，這與實際情況并不相符。原因在于同步機制，內(nèi)核會利用一定的機制同步對管道的訪問，為此，內(nèi)核使用了鎖、等待隊列和信號。而本方法在管道到讀寫進(jìn)程狀態(tài)只是使用了全局變量，致使讀寫端進(jìn)程狀態(tài)沒有得到更新，為了更好的模擬實際情況，給出改進(jìn)措施：

a.增加同步通道

這樣管道狀態(tài)變化可以及時與讀寫進(jìn)程通信，通知讀寫進(jìn)程。實際上，管道狀態(tài)和讀寫進(jìn)程狀態(tài)是互相制約，同步轉(zhuǎn)換的。

b.為讀寫端實體各增加一個PAUSE狀態(tài)，與WAIT狀態(tài)區(qū)分，以讀端為例

圖8 改進(jìn)讀端模型

3）最后，通過更改初始參數(shù)，模擬不同的情況，驗證可終止性，得到系統(tǒng)不同的結(jié)束狀態(tài)。也可用ltl 公 式 {＜ >（Reader_State == FINISH &&Writer_State==FINISH&&Pipe_State==CLOSE）}來檢驗。當(dāng)違反屬性時，SPIN生成反例trail文件，可以沿錯誤路徑再次進(jìn)行模擬，得到反例情況。

SPIN模擬輸出的結(jié)果格式如圖9所示，具體所有結(jié)果列于表1。

圖9 SPIN模擬輸出結(jié)果

表1 各實體終止?fàn)顟B(tài)

第一種情況代表管道讀寫端正確讀?。ɑ蜃x取實際可讀數(shù)據(jù)）和寫入數(shù)據(jù)后關(guān)閉；

第二種情況代表寫端寫入數(shù)據(jù)時，讀端關(guān)閉，管道宣布破裂；

第三種情況表明管道以非阻塞形式打開，但管道為空，讀者返回-1；

第四種情況表明管道以非阻塞形式打開，寫入數(shù)據(jù)大于緩沖區(qū)總長度且管道已滿或者寫入數(shù)據(jù)小于緩沖區(qū)長度但管道不足以容納；

第五種情況表明管道以阻塞形式打開，寫端寫入完成，但讀端進(jìn)入了等待讀取數(shù)據(jù)的情況。實際上讀取進(jìn)程也可能工作得比寫進(jìn)程快，當(dāng)寫進(jìn)程還未關(guān)閉前，讀進(jìn)程讀空管道數(shù)據(jù)進(jìn)入了等待狀態(tài)，只有等待新的數(shù)據(jù)被寫入。這種情況對應(yīng)于實際編程中打開了文件描述符，而操作結(jié)束后，忘記close的情況，應(yīng)當(dāng)引起注意。

4 結(jié) 論

本文基于實際工作中的測試需要，對操作系統(tǒng)驗證方法進(jìn)行了調(diào)研。簡要介紹了形式化方法中的模型檢測，并對模型檢測工具SPIN及其編程語言Promela進(jìn)行了詳細(xì)描述。基于SPIN，對Linux進(jìn)程間通信手段之一的管道進(jìn)行了建模分析，對前人有關(guān)研究工作進(jìn)行了改進(jìn)、細(xì)化和補充完善。希望能夠拋磚引玉，對操作系統(tǒng)驗證工作有所幫助和啟發(fā)。