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

速昱行 ，王金波

（1.中國科學院大學北京100190；2.中國科學院空間應用工程與技術中心北京100094）

為了適應航天事業的快速發展，完成繁雜的空間任務，對嵌入式軟件系統的可靠性、穩定性等提出了更高的要求，Linux作為一款開源、可裁剪、可移植的操作系統逐漸被應用于國內外航天嵌入式領域。

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

1）通過各種系統調用測試內核功能的安全性和正確性；

2）通過第三方的測試套件（工具）對內核進行測試；

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

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

1 模型檢測和SPIN概述

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

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

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

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

3）驗證——分析驗證結果（錯誤軌跡）。

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

圖1 SPIN模型檢測過程

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

2 Linux管道的分析驗證

2.1 管道的描述

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

圖2 管道創建過程

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

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

3）隨后，父進程關閉讀端，子進程關閉寫端，則前者向管道中寫入數據，而后者就可以將管道中的數據讀出，這樣就實現了進程間通信。

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

2.2 管道的建模

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

2.2.1 管道模型

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

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

圖3 管道模型

2.2.2 管道讀端

如果某個進程要讀取管道中的數據，那么該進程應當及時關閉fd[1]，以避免意外錯誤的發生。讀端進程通過調用read（）系統調用讀取管道內容，讀端實體進入READ狀態，此時分兩種情況，阻塞方式（NOBLOCK==0）和非阻塞方式讀?。∟OBLOCK==1）。

阻塞方式下：

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

2）如果管道中數據為0并且請求數據不為0時，若寫端文件描述符未關閉則進入等待狀態WAIT；

3）若管道中數據為0，寫端文件描述符關閉，則返回0，進入結束狀態FINISH；

4）阻塞等待的讀端進程在管道有數據寫入時再次進入讀取狀態READ；

5）當請求數據讀取完成后，進入完成FINISH狀態。

非阻塞方式下：

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

2）若管道中數據為0，若管道寫端被關閉，則返回0；若寫端未關閉則返回-1；進入FINISH狀態。

讀取結束，文件描述符關閉后，讀者計數器置0。具體的變遷過程如圖4所示。

圖4 管道讀端模型

2.2.3 管道寫端

因為緩沖區大小固定，管道寫端的情況相對更加復雜。寫進程寫入數據前需要關閉讀端，即close（fields[0]）。當寫進程向管道中寫入時，它利用標準的庫函數write（），系統根據庫函數傳遞的文件描述符，可找到該文件的file結構。file結構中指定了用來進行寫操作的函數（即寫入函數）地址，同時需要滿足管道沒有被讀進程占用。寫進程進入數據寫入狀態時，同樣分為阻塞和非阻塞兩種情況。

阻塞情況下：

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

2）當數據寫入完畢，進入FINISH狀態；

非阻塞情況下：

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

2）當寫入數據wdata大于管道總長度buf時，若管道未滿，則寫入可容納數據；若管道已滿則返回錯誤；

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

圖5 管道寫端模型

2.2.4 模型的Promela描述

3個實體分別為進程

各進程初始狀態分別為

對用到的狀態作枚舉說明

mtype={UNCREATED， CREATED， IsREAD，WRITTEN，ReadyCLOSE，BROKEN，CLOSE，UNWRITE，UNREAD，READ，WRITE，WAIT，FINISH}。

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

同時由于管道狀態與讀寫端進程是同步關系，定義消息通道

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

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

增加和細化的遷移條件，使新模型更加完善；對原建模方法當中的錯誤遷移條件進行了勘誤，如讀寫端進程是先結束，再關閉文件描述符，計數減少。

圖6 管道Promela部分代碼

3 實驗結果分析及改進

實驗中，屬性用LTL表達式進行描述，作為SPIN的輸入。

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

圖7 ltl屬性驗證

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

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

a.增加同步通道

這樣管道狀態變化可以及時與讀寫進程通信，通知讀寫進程。實際上，管道狀態和讀寫進程狀態是互相制約，同步轉換的。

b.為讀寫端實體各增加一個PAUSE狀態，與WAIT狀態區分，以讀端為例

圖8 改進讀端模型

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

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

圖9 SPIN模擬輸出結果

表1 各實體終止狀態

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

第二種情況代表寫端寫入數據時，讀端關閉，管道宣布破裂；

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

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

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

4 結 論

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