實時操作系統(tǒng)中有限優(yōu)先級反轉(zhuǎn)的驗證

張 嘯 然

1(中國科學技術(shù)大學 計算機科學與技術(shù)學院，合肥 230027) 2(中國科學技術(shù)大學 蘇州研究院軟件安全實驗室，江蘇 蘇州 215123)

1 引 言

優(yōu)先級調(diào)度算法是實時操作系統(tǒng)中常用的一種調(diào)度算法.這種調(diào)度算法始終選擇最高優(yōu)先級的就緒態(tài)中優(yōu)先級最高的任務執(zhí)行，基于這種性質(zhì)，用戶可以分配給不同任務不同的優(yōu)先級來確保任務的實時性得以滿足.然而，當系統(tǒng)中同時使用了優(yōu)先級調(diào)度與信號量同步機制時，由于阻塞的產(chǎn)生，會導致優(yōu)先級反轉(zhuǎn)問題：擁有高優(yōu)先級的任務會被低優(yōu)先級的任務無限制的阻塞.圖1給出了一個簡單的優(yōu)先級反轉(zhuǎn)問題的例子.

假設(shè)t1,t2,t3是3個按優(yōu)先級從低到高排列的任務.在開始階段，只有任務t1執(zhí)行，在其執(zhí)行的過程中，他獲取了信號量s.之后任務t3被創(chuàng)建，由于t3的優(yōu)先級大于t1，調(diào)度器會讓t3優(yōu)先執(zhí)行.在t3運行一段時間后，他也需要獲取信號量s，但由于此時任務t1已經(jīng)得到了信號量s，所以他只能等待t1釋放信號量s.由于此時t3進入了等待狀態(tài)，系統(tǒng)會切換到t1執(zhí)行.在t1執(zhí)行一段時間后，任務t2被創(chuàng)建，由于t2的優(yōu)先級大于t1，t2會被優(yōu)先執(zhí)行.如果此時t2是一個永續(xù)的任務，那么此時t3會被永遠的阻塞.這時，一個典型的優(yōu)先級反轉(zhuǎn)問題發(fā)生了：t2的優(yōu)先級低于t3，但其卻永遠的阻塞了t3的執(zhí)行.

圖1 無限優(yōu)先級反轉(zhuǎn)Fig.1 Unbounded priority inversion

為了解決這個問題，Sha等人[1]中提出了優(yōu)先級繼承協(xié)議與優(yōu)先級天花板協(xié)議.并分別給出了這兩種協(xié)議中高優(yōu)先級任務會被低優(yōu)先級任務所阻塞的最長時間.在這之后，也有各種各樣的用于避免產(chǎn)生無限優(yōu)先級反轉(zhuǎn)問題的協(xié)議被提出.如Baker[2]就提出了棧資源協(xié)議，用于只在棧上分配資源的同時避免此問題.Chen等人[3]也提出運用動態(tài)優(yōu)先級天花板的新思路.而常被參考的IEEE的POSIX操作系統(tǒng)標準中也給出了兩套建議的協(xié)議規(guī)范(優(yōu)先級繼承協(xié)議與優(yōu)先級保護協(xié)議)來解決這個問題.

然而由于這些協(xié)議設(shè)計的較為精妙，在實現(xiàn)的過程中一些細節(jié)常常被忽略而導致錯誤的產(chǎn)生.Yodaiken[4]中就指出，在Sha等人[1]給出的最早版本的優(yōu)先級繼承協(xié)議代碼實現(xiàn)中實際上在一些情況下是錯誤的.Xu等人[5]中也指出只有當信號量同步機制不被嵌套使用時，操作系統(tǒng)μC/OS-Ⅱ中所實現(xiàn)的防止優(yōu)先級反轉(zhuǎn)協(xié)議才有作用.雖然目前已經(jīng)有了關(guān)于避免優(yōu)先級反轉(zhuǎn)問題的一些驗證工作[7-10]，但該工作依然未能做到驗證底層真實的代碼.

本文將給出一套保證有限優(yōu)先級反轉(zhuǎn)性質(zhì)的驗證框架.該系統(tǒng)的整體性概覽可參見圖2.一套防止無限優(yōu)先級反轉(zhuǎn)問題的協(xié)議，可以看作圖中高層代碼抽象部分.其是否能夠保證有限優(yōu)先級反轉(zhuǎn)性質(zhì)可以看作為使用該規(guī)范的系統(tǒng)在執(zhí)行時是否所有的執(zhí)行跡都滿足有限優(yōu)先級反轉(zhuǎn)的定義(圖中①和②).但由于這樣的證明過程往往過于復雜，本文提出了合理OS實現(xiàn)的定義，并證明了如果靜態(tài)協(xié)議抽象可以滿足該定義，那么使用該套協(xié)議所可能產(chǎn)生的所有跡均可滿足有限優(yōu)先級反轉(zhuǎn)(圖中③和④).圖中的下半部分給出了本文對于具體底層代碼層面驗證的思路.本文在第六章中提供了一套驗證邏輯，該套邏輯能夠用于證明底層代碼生成的跡與對應的高層代碼間具有子集關(guān)系.這樣，自然的也就得到了底層代碼具有有限優(yōu)先級反轉(zhuǎn)性質(zhì).最后，作為實例，本文驗證了POSIX標準中提供的兩個用于保證有限優(yōu)先級反轉(zhuǎn)的協(xié)議——優(yōu)先級保護協(xié)議和優(yōu)先級繼承協(xié)議.此外，由于本文中所提到的所有工作均通過了驗證輔助工具Coq的檢驗，因此文中省略了具體的定理證明部分.

相比之前的工作，本文的工作具有以下幾點貢獻：

1)本文基于代碼執(zhí)行過程中產(chǎn)生的跡給出了一個協(xié)議無關(guān)的有限優(yōu)先級反轉(zhuǎn)的形式化定義，此定義可以被同時運用在抽象機器層面與實際機器層面.

圖2 概覽Fig.2 Overview

2)本文建立的框架提供了一套抽象語言.用戶可以用此語言簡單的描述出算法協(xié)議.此外，本文給出了一套基于該語言的輔助定義“合理OS實現(xiàn)”并證明了該定義蘊含有限優(yōu)先級反轉(zhuǎn).對于一個協(xié)議，用戶可以通過證明協(xié)議滿足該定義來就簡單的得到協(xié)議可以保證有限優(yōu)先級反轉(zhuǎn)性質(zhì).該證明方案大大降低了證明有限優(yōu)先級反轉(zhuǎn)問題的難度.

3)本文給出了一套程序邏輯用于證明底層C代碼實現(xiàn)與高層抽象語言之間的精化關(guān)系.此精化關(guān)系可以傳遞有限優(yōu)先級反轉(zhuǎn)性質(zhì)，從而使得對于此問題的驗證可以被用于底層.這也是第一次能夠做到在實際機器層面保證該性質(zhì).

4)通過應用該驗證框架，作為實例，本文在最后證明了POSIX標準中的兩套協(xié)議確實能夠防止無限優(yōu)先級反轉(zhuǎn)的問題.并且對于這兩套協(xié)議分別給出了對應的底層C代碼實現(xiàn)，并證明了它們間的精化關(guān)系.

2 相關(guān)工作

目前已經(jīng)有了數(shù)個工作與本文的工作相關(guān).但這些工作都沒有在實際的代碼層面對該問題進行驗證.此外，以已有的工作都是面向特定的協(xié)議進行驗證的，而本文的工作則更為宏觀的提出了一套可用于驗證多種防止無限優(yōu)先級反轉(zhuǎn)協(xié)議的方案.

Zhang等人基于Isabelle/HOL的項目[6]是最接近本文的.該項目引入了一個記錄每個操作的跡(包括了獲取信號量，釋放信號量，創(chuàng)建任務等)，并于跡上定義了有限優(yōu)先級反轉(zhuǎn)以及優(yōu)先級繼承協(xié)議.之后，該項目證明了當跡滿足協(xié)議定義時，其必將滿足有限優(yōu)先級反轉(zhuǎn)性質(zhì).然而，這種定義方案嚴重的限制了該項目的可擴展性：該項目對跡的硬編碼使得該方案難以在加入新的接口(如信號量等待超時等)，而這在實際的應用中常常是需要的.此外，該方案中缺乏對語義的描述，這使得該方案難以被用來進行代碼層面的驗證.

Dutertre[7]通過PVS框架定義了優(yōu)先級天花板協(xié)議并給出了使用此協(xié)議時的任務執(zhí)行時間的上界.該工作使用了模型檢測方案，這使得該工作只能被運用在有限任務且有限跡的系統(tǒng)中.此外，該項目對于協(xié)議的硬編碼也導致了擴展性的缺乏.

總的來說，相比以前的工作，本文的工作具有以下優(yōu)點：

1)本文的方案具有較高的可拓展性，可以便捷的對信號量加入新的特性以及API等.

2)本文的方案可以被運用于多種保證有限優(yōu)先級反轉(zhuǎn)性質(zhì)的協(xié)議中.

3)本文的方案能夠用于驗證底層的C代碼實現(xiàn)的協(xié)議.

3 優(yōu)先級反轉(zhuǎn)的形式化定義

本章會介紹有限優(yōu)先級反轉(zhuǎn)的形式化定義.同時，由于該性質(zhì)并不只能由協(xié)議本身保證：用戶正確的使用協(xié)議也是保證該性質(zhì)發(fā)生的一個重要因素，在本章中也會對這部分內(nèi)容進行形式化的刻畫.

3.1 抽象內(nèi)核模型和優(yōu)先級反轉(zhuǎn)

一個抽象內(nèi)核模型必須要實現(xiàn)四種抽象方法：GetCur,GetPrio,GetSemOwner以及GetTaskState.方法GetCur()用于返回抽象內(nèi)核狀態(tài)的當前執(zhí)行任務，方法GetPrio(t)用于取得任務t的優(yōu)先級.方法GetSemOwner(s)用于返回信號量s的所有者.方法GetTaskState(t)則用來返回任務t的狀態(tài).

定義1.優(yōu)先級反轉(zhuǎn)

狀態(tài)Σ對于任務t是優(yōu)先級反轉(zhuǎn)的，當且僅當該狀態(tài)中任務t的優(yōu)先級高于正在被調(diào)度執(zhí)行的任務.

3.2 跡和有限優(yōu)先級反轉(zhuǎn)

由于在操作系統(tǒng)中，往往會使用信號量來控制共享資源，這導致偶爾單次的優(yōu)先級反轉(zhuǎn)發(fā)生本身是不可避免的.本文中真正想要避免出現(xiàn)的問題是優(yōu)先級反轉(zhuǎn)狀態(tài)在系統(tǒng)執(zhí)行過程中出現(xiàn)了無限多次，這種情況被為無限優(yōu)先級反轉(zhuǎn)(UPI).

為了描繪這種情況，首先引入跡的定義.

ξ:=|||Σ::ξ(coinductive)

為了描述可能存在的無限情形，定義中使用共歸納(coinductive)的方式來定義跡.在該定義中，符號用來描繪跡結(jié)束于靜默執(zhí)行(沒有新事件生成，但系統(tǒng)依然執(zhí)行)；符號用于描繪系統(tǒng)正常退出，而符號則用來描繪系統(tǒng)以崩潰的方式結(jié)束.

由于無限優(yōu)先級反轉(zhuǎn)是在表達系統(tǒng)未來的行為.為了便于表達和理解，定義中使用了線性時態(tài)邏輯進行表達.關(guān)于線性時態(tài)邏輯的定義可以參考圖3.

圖3 線性時態(tài)邏輯Fig.3 Linear temporal logic

定義2.無限優(yōu)先級反轉(zhuǎn)

自然地，有限優(yōu)先級反轉(zhuǎn)的定義可以被定義如下：

定義3.有限優(yōu)先級反轉(zhuǎn)

需要注意的是，有限優(yōu)先級反轉(zhuǎn)的成立與否并不僅僅取決于調(diào)度算法及各操作系統(tǒng)接口的實現(xiàn).該性質(zhì)與用戶對于操作系統(tǒng)接口的正確使用也是息息相關(guān)的.

具體的，考慮如下情形：

任務t1和任務t2是兩個按優(yōu)先級從低到高排序的任務.假設(shè)在開始階段系統(tǒng)中只有任務t1在執(zhí)行.在這時，t1獲取了信號量s.之后，任務t2被創(chuàng)建，由于t2優(yōu)先級高于t1，所以此時系統(tǒng)會切換到t2執(zhí)行.如果此時t2也需要信號量s，他會被迫等待t1.如果t1永遠不釋放信號量s，那么這時候t2就會被無限制的阻塞.

在這種情況下，應當認為是用戶的錯誤使用導致了無限優(yōu)先級反轉(zhuǎn)問題的發(fā)生.系統(tǒng)很難處理這種由于用戶錯誤操作導致的問題.實際上，協(xié)議在設(shè)計時往往假設(shè)用戶正確的使用了這些系統(tǒng)接口.具體的來說，本文對用戶做出以下假設(shè)：

1)假設(shè)任務獲取某信號量后，如果該任務能夠執(zhí)行，那么最終該任務一定會釋放該信號量.

2)系統(tǒng)不會發(fā)生死鎖.

3)信號量的獲取與釋放是正確的被嵌套使用的.

下面給出這些假設(shè)的形式化的定義(定義中出現(xiàn)的輔助定義參考圖4)：

定義4.有限臨界區(qū)假設(shè)

跡符合有限臨界區(qū)假設(shè)成立當且僅當對于任何任務t，如果該任務能被執(zhí)行，那么它所持有的任意信號量s都最終會被釋放.

注意到定義中強調(diào)了如果該任務能夠被執(zhí)行，這一點對于用戶滿足這個假設(shè)是非常重要的：用戶難以保證任務在不被執(zhí)行的情況下依然能夠釋放信號量.

定義5.無死鎖假設(shè)

無死鎖假設(shè)成立當且僅當序列中的所有狀態(tài)均不存在死鎖環(huán)(存在某任務直接或間接的等待他自己).

無死鎖假設(shè)也是必要的，由于當死鎖發(fā)生時系統(tǒng)實際上難以正確運行，討論有限優(yōu)先級反轉(zhuǎn)也就什么意義了.

定義6.正確嵌套假設(shè)

?s′,?IsOW(t,s′)」→。(?IsOW(t,s′)」W?IsOW(t,s)」)

正確嵌套假設(shè)成立當且僅當對任意的任務t和信號量s，如果任務在獲得信號量s后獲得了s′，那么該任務一定會優(yōu)先釋放信號量s′.

最終，用戶需要滿足的所有的規(guī)范可以定義如下：

定義7.用戶正確操作

4 高層機器與語言的刻畫

由于用戶真正關(guān)心的是如何證明的是內(nèi)核代碼能否符合有限優(yōu)先級反轉(zhuǎn).本章會首先給出一套高層抽象語言的定義，該套語言可以被用來刻畫各種優(yōu)先級反轉(zhuǎn)協(xié)議.之后，本章定義了靜態(tài)代碼層面的有限優(yōu)先級反轉(zhuǎn)——對于任意用戶代碼，只要用戶正確的使用操作系統(tǒng)接口，所有由該系統(tǒng)執(zhí)行生成出的跡均滿足有限優(yōu)先級反轉(zhuǎn).

4.1 高層程序

系統(tǒng)抽象代碼(P)的定義可參考圖5.其由兩個部分組成：用戶代碼A以及內(nèi)核規(guī)范代碼O.內(nèi)核規(guī)范代碼包括了內(nèi)核的應用編程接口ρ，中斷處理程序Q以及調(diào)度器χ.其中，應用編程接口是由函數(shù)名到該函數(shù)的規(guī)范代碼的映射.中斷處理程序則是一個規(guī)范代碼的列表，其中列表的第n項代表了該代碼是n級中斷的處理函數(shù).調(diào)度器是內(nèi)核狀態(tài)Σ和任務標識符t的關(guān)系，用來描繪若在內(nèi)核狀態(tài)下進行調(diào)度，調(diào)度目標將會是t.

規(guī)范代碼ω一共有6種形式：元語γ在接收一個參數(shù)列表后會是兩種抽象內(nèi)核狀態(tài)之間的關(guān)系，他能被用來描述各式各樣的協(xié)議.sched描述了一個產(chǎn)生調(diào)度的語句，而create則用來描述一個創(chuàng)建新任務.ω1;ω2用來描述串行語句，該語句會按照順序依次執(zhí)行，ω1+ω2用來表達選擇執(zhí)行語句，機器可以選擇其中的任意一條進行執(zhí)行.end v則用來表達規(guī)范代碼執(zhí)行結(jié)束，返回值是v.

4.2 高層機器狀態(tài)

高層狀態(tài)的定義可以參考圖6，高層機器狀態(tài)Φ包含了程序當前執(zhí)行Π，客戶狀態(tài)Δ和內(nèi)核狀態(tài)Σ.Π是一個由任務標識符到代碼執(zhí)行棧的映射，系統(tǒng)會始終從中取出當前被執(zhí)行任務的代碼片段進行執(zhí)行.Δ是一個由任務標識符到客戶局部內(nèi)存的映射，代表了客戶程序的內(nèi)存狀態(tài).而Σ則代表了內(nèi)核狀態(tài)信息，其可以根據(jù)需要進行具體的實例化.

圖6 抽象狀態(tài)Fig.6 Abstract state

4.3 語義及跡的生成

為了合理的描繪中斷，本文的語義部分定義采用了非確定性的形式.高層機器的中斷描繪較為簡單：中斷可以在任何情況下執(zhí)行，當中斷發(fā)生時，系統(tǒng)會立即將中斷代碼置入當前任務的代碼棧中，這樣中斷處理函數(shù)就會立刻響應執(zhí)行.此外，語義需要記錄高層抽象狀態(tài)隨著系統(tǒng)執(zhí)行的變化，這樣就可以得到一個上文提到的所需的跡.

有一個關(guān)鍵的問題是，需要記錄哪些系統(tǒng)狀態(tài)的變化？從應用程序用戶的視角來看，所有的系統(tǒng)應用接口的調(diào)用都是一個黑箱，并且，系統(tǒng)中斷也不在這些用戶的考慮范圍之內(nèi).因此，本文將語義在進行任務步驟時(執(zhí)行用戶代碼的步)會輸出一個當前內(nèi)核狀態(tài)的記錄；而在系統(tǒng)步驟中(執(zhí)行API或中斷處理函數(shù)期間)不輸出這樣的狀態(tài)記錄.這樣，跡就可以通過記錄語義的內(nèi)核狀態(tài)輸出來得到了.

跡的生成被定義為如下形式：

定義8.跡的生成

所有可能生成的跡則通過以下定義得到：

定義9.所有合法跡

其中：

高層系統(tǒng)滿足有限優(yōu)先級反轉(zhuǎn)定義如下：

定義10.高層系統(tǒng)有限優(yōu)先級反轉(zhuǎn)

5 在抽象規(guī)范層面證明有限優(yōu)先級反轉(zhuǎn)

之前的章節(jié)定義了高層系統(tǒng)上的有限優(yōu)先級反轉(zhuǎn)，但直接證明這個性質(zhì)往往是十分困難的.這主要是因為定義涉及到由靜態(tài)高層抽象規(guī)范生成動態(tài)的跡.本章會嘗試簡化證明的思路.參考了之前Gu等人已有的相關(guān)工作[10]，本章引入一些單步的性質(zhì)，并證明這些性質(zhì)可以推導出高層系統(tǒng)有限優(yōu)先級反轉(zhuǎn).通過將復雜的全局問題規(guī)約成每一小步的性質(zhì)，就能夠簡化許多證明的工作.

回憶圖1中描繪的情形，當優(yōu)先級反轉(zhuǎn)發(fā)生時，應該讓t1在t2被創(chuàng)建后接著執(zhí)行.這是由于此時t1阻塞了t3，所以該任務應當被認為具有至少為t3的緊急程度.因此，必須讓該任務首先得到執(zhí)行.這樣的需求要求設(shè)計出一種新的調(diào)度器，該調(diào)度器并不能僅僅只根據(jù)每個任務的優(yōu)先級執(zhí)行任務調(diào)度——它還需要考慮任務間的阻塞關(guān)系.

所以，一個可能可行的方案就是，讓調(diào)度器選擇的對象要么具有最高優(yōu)先級，要么阻塞了最高優(yōu)先級任務的執(zhí)行.然而，這個要求對于一個一般的防止無限優(yōu)先級反轉(zhuǎn)的協(xié)議太過于嚴格.實際上，考慮每個臨界區(qū)均在有限執(zhí)行時間內(nèi)被完成時，可以合理地認為調(diào)度器只要能夠不停地調(diào)度到任意一個具有信號量的任務或最高優(yōu)先級的任務，那么有限優(yōu)先級反轉(zhuǎn)就可以滿足了.

形式化的，可以給出如下的定義：

定義11.合理調(diào)度策略

(χ├((ω,K),Σ)→((ω′,K′),Σ′))→

ProperlySched(χ,Σ)→ProperlySched(χ,Σ′)

其中

HighestPrio(Σ,t)∨(?s,Σ.IsOW(t,s))

定義中符號_├_|→_用于指代高層語義中的單步內(nèi)核操作語義.

合理調(diào)度策略成立當且僅當對任意初始狀態(tài)Σ，根據(jù)代碼ω執(zhí)行一步后變?yōu)闋顟B(tài)Σ′時，若性質(zhì)ProperlySched對Σ成立，則其一定對Σ′成立.

該策略正是之前所說的要求的形式化描述，此外，為了保證調(diào)度器確實在合適的時機起到了調(diào)度作用，還需要以下兩個定義：

定義12.釋放信號量后執(zhí)行調(diào)度

(χ├((ω,K),Σ)((ω′,K′),Σ′))→

Σ.GetSemOwner(s)≠t→HaveSched(ω′)

定義13.創(chuàng)建任務后執(zhí)行調(diào)度

(χ├((ω,K),Σ)→((ω′,K′),Σ′))→

(?s,Σ.GetSemOwner(s)≠t)→HighestPrio(Σ,t)→

其中HaveSched函數(shù)是用來在語法層面表達后續(xù)的語句中含有sched語句：

這兩個定義表達了在什么情況下操作系統(tǒng)必須要進行重新調(diào)度.實際上，只有兩種情況可能造成當前執(zhí)行的任務：1)釋放的操作—這會導致阻塞關(guān)系的變化，該操作可能導致當前任務不再阻塞某信號量；2)創(chuàng)建的操作—創(chuàng)建新任務可能導致當前任務不再是最高優(yōu)先級的任務了.當發(fā)生這兩類操作后，必須要求操作系統(tǒng)重新執(zhí)行調(diào)度.

除此之外，系統(tǒng)接口也需要符合以下規(guī)范：

定義14.信號量獨立性

(χ├((ω,K),Σ)→((ω′,K′),Σ′))→

定義15.優(yōu)先級維持

(χ├((ω,K),Σ)→((ω′,K′),Σ′))→

?t,Σ′.GetPrio(t)=Σ.GetPrio(t)

通常來說，這兩個性質(zhì)是容易保證的.信號量獨立性說的是每個任務只能通過自己主動的一個操作來嘗試獲取一個信號量.需要注意的是該定義并非要求任務必須在自己執(zhí)行時獲得信號量.在一些操作系統(tǒng)實現(xiàn)中，會在釋放操作時使另一個任務獲得信號量，該操作并不和該定義矛盾—另一個任務必定是由等待狀態(tài)轉(zhuǎn)為獲得信號量的就緒狀態(tài).

優(yōu)先級維持的性質(zhì)往往也較容易被保證.它要求任務的優(yōu)先級在執(zhí)行中不會被改變.需要注意的是該定義所要求保持不變的優(yōu)先級指的是任務的邏輯優(yōu)先級.在一些協(xié)議的實現(xiàn)中，某些操作會臨時調(diào)整任務的優(yōu)先級，但這種調(diào)整的優(yōu)先級并非任務的邏輯優(yōu)先級，而只是一種臨時優(yōu)先級.

最終，可以匯總得到以下定義及定理：

定義16.合理有限優(yōu)先級反轉(zhuǎn)系統(tǒng)接口

SchedAfterUnlock(χ,ω)∧SchedAfterCreate(χ,ω)∧

WaitIndependent(ω)∧PrioPresv(ω)

其中，suffix是用于在語法上計算可能后續(xù)語法的函數(shù)：

最后，就能夠給出本章最重要的一個定理：合理OS實現(xiàn)可以推導出有限優(yōu)先級反轉(zhuǎn).鑒于該定理的證明過程較為繁瑣，具體證明部分可以參考具體Coq代碼中的證明部分.

定理1.合理OS實現(xiàn)蘊含有限優(yōu)先級反轉(zhuǎn)

?O,WellFormedOS(O)→HOSFUPI(O)

6 底層有限優(yōu)先級反轉(zhuǎn)

至此，本文已經(jīng)展示了如何在協(xié)議規(guī)范層面證明有限優(yōu)先級反轉(zhuǎn)的方案.但這仍然與本文的最終目標—在實際的機器層面進行驗證存在差距.本章會介紹一套方案來用于解決這個問題.首先，為了能夠表達底層機器模型，下面先各處底層機器模型的定義.

6.1 底層機器及語言

圖7給出了本文中底層程序和狀態(tài)的定義.這部分定義主要參考了x86體系結(jié)構(gòu).定義中，P是底層的程序，其中A是已經(jīng)在之前提到過的客戶端代碼，O是底層的系統(tǒng)代碼.Φ則是底層的系統(tǒng)狀態(tài)，與高層類似，它包括了任務代碼執(zhí)行棧映射Π和用戶程序狀態(tài)映射Δ.除此之外，其還包含了底層的系統(tǒng)狀態(tài)σ.

圖7 底層程序和狀態(tài)Fig.7 Concrete program and state

雖然大多數(shù)的操作系統(tǒng)都是由C語言和匯編來實現(xiàn)的，但完整的刻畫這些語義過于繁瑣并且沒有必要.這是由于實際上在操作系統(tǒng)實現(xiàn)中所用到的匯編只有很特定的一部分.作為替代方案，本文將操作系統(tǒng)中常用的匯編代碼塊分別抽象為了匯編原語，與標準的C語言一起用作本文的底層語言(見圖8).

圖8 底層語法Fig.8 Concrete syntactic

跡的生成的定義類似于高層語言：

定義17.底層跡生成

定義18.底層合法跡

6.2 底層有限優(yōu)先級反轉(zhuǎn)

底層有限優(yōu)先級反轉(zhuǎn)的定義也與高層類似：

定義19.底層系統(tǒng)有限優(yōu)先級反轉(zhuǎn)

6.3 精化關(guān)系

由于本文在之前已經(jīng)在協(xié)議規(guī)范層面證明了有限優(yōu)先級反轉(zhuǎn)性質(zhì)，所以現(xiàn)在的問題可以歸結(jié)為如何證明一個具體實現(xiàn)的協(xié)議代碼確實是一個正確的規(guī)范實現(xiàn).為此，定義如下的精化關(guān)系：

定義20.精化關(guān)系

精化關(guān)系描繪了底層的所有可能生成跡與高層所有可能生成跡之間的子集關(guān)系.借此表達底層的具體協(xié)議代碼必然是一個合理的高層協(xié)議規(guī)范的實現(xiàn)——因為該底層系統(tǒng)所有可能行為均可被高層規(guī)范認可.

由精化關(guān)系和有限優(yōu)先級反轉(zhuǎn)定義，可以得到以下定理.

定理2.精化關(guān)系維持有限優(yōu)先級反轉(zhuǎn)

?OO,HOSFUPI(O)→O?O→OSFUPI(O)

6.4 CSL風格的關(guān)系程序邏輯

精化關(guān)系在驗證底層的有限優(yōu)先級反轉(zhuǎn)問題中有很大的作用.然而，證明具體高層代碼與底層代碼見的精化關(guān)系并不容易.這主要是由于并行程序的非確定性語義導致的.本文參考Liang等人[11,12]中的邏輯，設(shè)計給出了用于本文所需的邏輯.該邏輯基于將分離邏輯(CSL)運用于并行系統(tǒng)中，能夠較好的支持并行程序的驗證需求.然而，由于邏輯整體較為復雜而且繁瑣，限于篇幅的限制，在此從略.

6.5 邏輯可靠性

定理3.邏輯可靠性

?OO,├ O:O→O?O

定理中符號├ O:O即用于表達底層實現(xiàn)與高層規(guī)范間符合本文的程序邏輯.邏輯可靠性定理保證了邏輯能夠推理出兩層間的精化關(guān)系.證明這個定理并不簡單，本文根據(jù)Liang等人[11,12]中提出的思路將基于RGSim-T證明邏輯可靠性的方案延拓到多任務模型中來證明了這個定理.

圖9 邏輯有效性證明框架Fig.9 Soundness proof structure

本文展示了該定理的證明框架(見圖9).為了證明邏輯可靠性，本文定義了3層模擬關(guān)系.并通過可組合性定理建立最終的程序?qū)幽M關(guān)系，最終可以得到精化關(guān)系.

7 驗證POSIX標準協(xié)議

本章會采取上述方法來驗證POSIX標準中給出的兩種避免無限優(yōu)先級反轉(zhuǎn)的協(xié)議.這兩個協(xié)議被稱為“優(yōu)先級保護協(xié)議”(PPP)和“優(yōu)先級繼承協(xié)議”(PIP).

7.1 抽象內(nèi)核狀態(tài)實現(xiàn)

圖10給出了本章使用的高層抽象系統(tǒng)狀態(tài)的實例.狀態(tài)Σ包含了任務池T，信號量集合S和當前執(zhí)行的任務標識符tc.T將每個任務標識符映射到一個包含了任務邏輯優(yōu)先級，任務狀態(tài)及被用于調(diào)度的任務當前優(yōu)先級的三元組.S則將每個信號量標識符映射到一個由狀態(tài)和優(yōu)先級組成的二元組.這其中優(yōu)先級是優(yōu)先級保護協(xié)議中所需要用到的域.

圖10 抽象系統(tǒng)狀態(tài)實例Fig.10 Abstract kernel state

7.2 優(yōu)先級保護協(xié)議規(guī)范

優(yōu)先級保護協(xié)議會賦予每個信號量一個優(yōu)先級，并且只允許那些當前優(yōu)先級低于信號量優(yōu)先級的任務申請使用該信號量.當任務獲得某信號時，系統(tǒng)會臨時將該任務的優(yōu)先級提高到信號量的優(yōu)先級.并在釋放信號量時恢復優(yōu)先級.形式化的優(yōu)先級保護協(xié)議的定義可以參考圖11.

圖11 優(yōu)先級保護協(xié)議形式化定義Fig.11 Formal definition of PPP

規(guī)范ρPPP包括了兩個API—lock與unlock.定義中，χhp是根據(jù)臨時優(yōu)先級進行調(diào)度的調(diào)度器.原語γlocksucc描述了信號量被成功獲得的情形，并且會造成之前所說過的任務優(yōu)先級提升.γlockerr則描述了任務嘗試獲取信號量時出錯的情況.在釋放操作的定義中，γPPPunlock1描述了釋放信號量時降低任務優(yōu)先級的行為.γunlockerr則描述了釋放信號量發(fā)生錯誤的情形.限于篇幅，本文省略了定義中一些較為繁瑣的部分，其大致含義可以參考之前介紹的協(xié)議內(nèi)容.

運用定理1，可以證明以下定理.

定理4.優(yōu)先級保護協(xié)議保證有限優(yōu)先級反轉(zhuǎn)成立

HOSFUPI(OPPP)

7.3 優(yōu)先級繼承協(xié)議規(guī)范

當系統(tǒng)采用優(yōu)先級繼承協(xié)議時，如果一個低優(yōu)先級的任務阻塞了一個高優(yōu)先級的任務，系統(tǒng)會在其阻塞期間將該任務的優(yōu)先級調(diào)至高優(yōu)先級.形式化的定義可參見圖12.

與優(yōu)先級保護協(xié)議類似，可以證明得到以下定理：

定理5.優(yōu)先級保護協(xié)議保證有限優(yōu)先級反轉(zhuǎn)成立

HOSFUPI(OPIP)

7.4 精化關(guān)系證明

最后，本文用C語言實現(xiàn)了這兩個協(xié)議(OPPP和OPIP).通過運用第6章中的邏輯和定理2，得到以下兩個定理：

定理6.C語言版本的優(yōu)先級保護協(xié)議能保證有限優(yōu)先級反轉(zhuǎn)

OSFUPI(OPPP)

定理7.C語言版本的優(yōu)先級繼承協(xié)議能保證有限優(yōu)先級反轉(zhuǎn)

OSFUPI(OPIP)

至此，本文完整的證明了底層實現(xiàn)的協(xié)議能夠滿足有限優(yōu)先級反轉(zhuǎn)的要求.

圖12 優(yōu)先級繼承協(xié)議形式化定義Fig.12 Formal definition of PIP

8 總 結(jié)

本文給出了一套較為完整的方案用于驗證操作系統(tǒng)中有限優(yōu)先級反轉(zhuǎn)的方案.對比已有的工作，本文所介紹的方法的可擴展性更強，應用面也更廣.并且，這是第一個能夠在具體代碼的實現(xiàn)層面上驗證該性質(zhì)的方案.本文通過Coq實現(xiàn)了所有文中提到的定理與定義，這也確保了證明過程的正確性.

但同時，基于Coq的代碼證明任務十分的繁重.這一方面是由于使用Coq定理證明工具在驗證實際問題時所必須要面臨的局面.一方面也是由于現(xiàn)有的自動化策略與定理庫的支持不足.在這幾點上還需要更多的改善和進步.