μC/OS-Ⅲ任務調(diào)度器在Coq中的驗證

羅爾聰,郭 宇

(1.中國科學技術大學計算機科學與技術學院,合肥230026;

2.中國科學技術大學蘇州研究院軟件安全實驗室,江蘇蘇州215123)

μC/OS-Ⅲ任務調(diào)度器在Coq中的驗證

羅爾聰1,2,郭 宇1,2

(1.中國科學技術大學計算機科學與技術學院,合肥230026;

2.中國科學技術大學蘇州研究院軟件安全實驗室,江蘇蘇州215123)

以μC/OS-Ⅲ內(nèi)核中的任務調(diào)度器為研究對象,選取調(diào)度相關的核心代碼,驗證調(diào)度器代碼滿足優(yōu)先調(diào)度最高優(yōu)先級任務的性質(zhì)。基于分離邏輯與SCAP驗證理論,利用Coq輔助證明工具,通過定義機器模型、操作語義、邏輯斷言以及推導規(guī)則構建驗證框架。在驗證框架中,定義內(nèi)核數(shù)據(jù)結構和內(nèi)核相關性質(zhì)的邏輯描述,模塊化地對內(nèi)核代碼進行推理。驗證結果表明,μC/OS-Ⅲ任務調(diào)度器滿足可靠性要求,并且可以通過機器的自動檢查。

任務調(diào)度器;形式化驗證;分離邏輯;Coq證明工具;最高優(yōu)先級

1 概述

嵌入式操作系統(tǒng)負責管理系統(tǒng)軟硬件資源,在工業(yè)控制、移動設備等領域中處于非常關鍵的位置。為確保這部分完成任務調(diào)度的代碼能夠正確地運行,本文采用邏輯驗證的形式化方法,在輔助證明工具Coq［1］中驗證μC/OS-Ⅲ［2］內(nèi)核中的任務調(diào)度器代碼。μC/OS-Ⅲ任務調(diào)度器的形式化工作主要有以下難點:

(1)調(diào)度器代碼涉及到諸多系統(tǒng)數(shù)據(jù)結構,驗證之前需要描述其系統(tǒng)數(shù)據(jù)結構的性質(zhì)和它們相互之間應該滿足的關系。

(2)任務(Task),作為操作系統(tǒng)中運行的基本單元,具有描述其重要程度的優(yōu)先級(Priority)屬性。在任務調(diào)度過程中,內(nèi)核需要完成對最高優(yōu)先級(Highest Priority)任務的選取,然后進行任務上下文切換。驗證需要保證在執(zhí)行調(diào)度函數(shù)代碼前后,內(nèi)核中描述任務優(yōu)先級的變量能夠正確讀寫。

本文從μC/OS-Ⅲ任務調(diào)度器選取相關代碼,將其編譯后的匯編級指令進行形式化建模,然后為這部分指令給出形式化的規(guī)范(Specification)描述,并證明這部分代碼滿足最高優(yōu)先級調(diào)度性質(zhì):從任意一個合法機器狀態(tài)集合出發(fā),任務調(diào)度程序執(zhí)行調(diào)度相關代碼,之后到達一個新的狀態(tài)。在這個新狀態(tài)中,相關

全局變量記錄正確的最高優(yōu)先級與被選任務。

本文驗證的內(nèi)核調(diào)度代碼基于一個形式化的簡化機器模型,采用分離邏輯［3］描述內(nèi)核規(guī)范,同時采用SCAP［4］邏輯對內(nèi)核指令進行推理。本文的所有形式化工作都基于交互式定理證明工具Coq,主要工作如下:

(1)驗證μC/OS-Ⅲ任務調(diào)度器相關代碼以下關鍵性質(zhì)(內(nèi)存安全性、部分指令代碼的功能正確性和最高優(yōu)先級)。

(2)使用證明輔助工具Coq實現(xiàn)邏輯系統(tǒng)和驗證選取代碼,所有定義和證明都可以接受機器自動檢查。

2 相關工作

文獻［5］提出了一種基于C語言的FreeRTOS任務調(diào)度器的自動化證明方法。本文統(tǒng)一使用匯編語言進行建模,使得程序斷言能夠?qū)崿F(xiàn)對機器狀態(tài)的精確描述,且稍加擴展便可驗證操作系統(tǒng)底層代碼。

使用Coq交互式驗證工作量巨大,文獻［6-7］提供了可供參考的自動化或半自動化驗證策略。文獻［8］以SCAP框架為基礎提出一種含有模擬關系的虛擬機構造和驗證方案,可以作為本文改進的借鑒。

3 驗證方法

本文選取μC/OS-Ⅲ任務調(diào)度器中的2個重要函數(shù)OSSched()和OSIntExit()進行實現(xiàn)代碼級驗證。本節(jié)介紹它們所涉及的內(nèi)核數(shù)據(jù)結構及其執(zhí)行流程。

3.1 系統(tǒng)就緒表與系統(tǒng)優(yōu)先級表

在μC/OS-Ⅲ中,任務通過任務控制塊(TCB)來描述其狀態(tài)。TCB含有前向指針、后向指針和優(yōu)先級3個域。通過前2個域,優(yōu)先級相同的TCB構成雙鏈表。系統(tǒng)就緒表將分離的具有不同優(yōu)先級的TCB雙鏈表組織起來,在內(nèi)存中由一個全局的一維數(shù)組表示。數(shù)組元素由頭指針、尾指針和元素計數(shù)3個域構成,如圖1所示。

圖1 系統(tǒng)就緒表與系統(tǒng)優(yōu)先級表

系統(tǒng)優(yōu)先級表是另外一個全局一維數(shù)組,其設立的目的是為了快速獲得系統(tǒng)就緒表中的狀態(tài),數(shù)組元素取值與系統(tǒng)就緒表中對應TCB雙鏈表元素數(shù)量相關。

為了確保調(diào)度過程的正確執(zhí)行,調(diào)度代碼對兩表進行操作時必須滿足以下4個關鍵性質(zhì):

性質(zhì)1(良形雙鏈表) 雙鏈表中的每一個節(jié)點都正確地指向其前驅(qū)和后繼節(jié)點,此外雙鏈表中的TCB還擁有共同的優(yōu)先級。本文將此類雙鏈表稱之為良形雙鏈表。

性質(zhì)2(良形系統(tǒng)就緒表數(shù)組元素) 以良形雙鏈表共同優(yōu)先級為系統(tǒng)就緒表索引,獲得的數(shù)組元素的頭指針指向雙鏈表隊首,尾指針指向雙鏈表隊尾,元素計數(shù)與雙鏈表中TCB數(shù)量相等。本文稱之為良形數(shù)組元素。

性質(zhì)3(系統(tǒng)就緒表與系統(tǒng)優(yōu)先級表的一致性)

以系統(tǒng)就緒表任意數(shù)組元素都是良形為前提,對于任意索引,指向雙鏈表的元素數(shù)量與系統(tǒng)優(yōu)先級表對應元素取值存在雙射關系:元素數(shù)量為0(不為0),當且僅當系統(tǒng)優(yōu)先級表對應元素為0(為1)。本文稱之為一致性。

性質(zhì)4(最高優(yōu)先級) 優(yōu)先級p是最高優(yōu)先級,當且僅當系統(tǒng)就緒表中索引為p的數(shù)組元素指向的雙鏈表元素數(shù)量不為0(系統(tǒng)優(yōu)先級表對應元素為1),索引小于p的數(shù)組元素指向的雙鏈表元素數(shù)量為0(系統(tǒng)優(yōu)先級表對應元素為0)。

3.2 任務調(diào)度函數(shù)驗證

函數(shù)OSSched()和OSIntExit()是任務調(diào)度器的核心代碼,前者實現(xiàn)任務級任務調(diào)度,后者實現(xiàn)中斷級任務調(diào)度。OSSched()在任務實現(xiàn)代碼里被主動調(diào)用,OSSched與OSIntExit的函數(shù)流程如下:

函數(shù)入口是一系列任務調(diào)度條件判斷語句,以及關中斷進入臨界區(qū)的指令,之后函數(shù)通過系統(tǒng)優(yōu)

先級表和系統(tǒng)就緒表分別獲取最高優(yōu)先級與待切換任務,最后在退出臨界區(qū)之前進行任務級上下文切換。OSIntExit()通常在系統(tǒng)中斷服務程序中被調(diào)用,函數(shù)主體都在臨界區(qū)內(nèi)。

對比上述執(zhí)行流程可知,2個函數(shù)采用相同代碼實現(xiàn)獲取最高優(yōu)先級與待切換任務。在形式化過程中,性質(zhì)3描述的一致性是這段代碼正確性的保證。同時驗證被調(diào)用的OS_PrioGetHighest()函數(shù)時需要使用性質(zhì)4的內(nèi)容。

4 硬件機器模型與推理邏輯系統(tǒng)

本文選取Intel i386架構的一個簡化子集作為運行μC/OS-Ⅲ內(nèi)核的硬件平臺,并采用程序邏輯SCAP推理本文所研究的任務調(diào)度器代碼。

4.1 機器模型與操作語義

機器配置(mach)在Coq中被定義為四元組:

其中,代碼code是地址到機器指令的映射;內(nèi)存mem是地址到機器字的映射,寄存器文件regfile是從寄存器到機器字的映射;pc表示指令指針。

Inductive reg:Set:=eax:reg|edx:reg|ebp:reg|esp:reg |irf:reg|zf:reg.

注意這里的寄存器不僅包括通用寄存器eax和edx等,還包含一個中斷寄存器irf和獨立的標志位寄存器zf。在Coq中,寄存器通過歸納定義reg實現(xiàn)。

機器模型中指令集是i386機器指令集的一個子集,包含常見的指令,包括移位、算數(shù)、比較等指令。在Coq中,指令instruction也采用歸納定義:

指令的執(zhí)行指令語義采用2個關系謂詞來定義,NextS與NextPC。前者描述在指令執(zhí)行前后,內(nèi)存與寄存器的改變,而后者描述控制流的走向。

以MOV指令為例,謂詞NextS首先從寄存器文件R中獲取寄存器單元rs的值,暫存到變量x,然后通過函數(shù)rf_update更新R中的rd寄存器,新的寄存器文件為R′。

謂詞NextPC定義了指令指針的變化:在執(zhí)行MOV指令之后,指令指針加一,指向下一條指令。

限于篇幅,這里不再贅述其余的指令。其形式化語義大部分遵守Intel手冊中的描述。

4.2 斷言語言與推理邏輯系統(tǒng)

為了描述函數(shù)規(guī)范,本文采用分離邏輯的斷言語言來描述。后文中將要使用到的部分邏輯連接詞如下:

其中,p??q表示分離合取;為了描述不依賴于任何存儲的斷言,本文用!標記純斷言(pure assertion); l|-＞w表示地址為l的內(nèi)存單元存儲值為w。在Coq實現(xiàn)時,本文采用淺嵌入［9］的方式來定義斷言語言。

程序邏輯SCAP(Stack-based Certified Assembly Language)是用來推理帶有結構化堆棧操作的機器指令的類似Hoare邏輯［10］的推理系統(tǒng)。SCAP邏輯的推理過程以指令序列為單位。函數(shù)由一些指令序列構成,程序規(guī)范以函數(shù)為單位定義。程序規(guī)范是一個二元組,包含一個前條件與一個描述函數(shù)前后狀態(tài)變化的二元關系:

程序規(guī)范集合PSpec是一個從一個指令序列的起始地址到函數(shù)規(guī)范的定義。下面列出SCAP推理規(guī)則在Coq中的定義框架:

可以看出,推理規(guī)則被定義成一個多元關系WFcomm,根據(jù)接受的指令進行分情況展開,每一個分支對應不同指令的推導規(guī)則。

5 驗證實現(xiàn)

本節(jié)介紹符合性質(zhì)1和性質(zhì)2的內(nèi)核數(shù)據(jù)結構,以及符合性質(zhì)3和性質(zhì)4的內(nèi)核性質(zhì)的斷言構

造過程。

5.1 內(nèi)核數(shù)據(jù)結構的表示

為表示相同元素組成的有序序列,本文以Coq標準庫中多態(tài)list作為形式化的基礎歸納構造類型,以實現(xiàn)核心數(shù)據(jù)與特定數(shù)據(jù)結構的分離。以圖1中OSPrioTbl索引0～4的片段為例,定義抽象優(yōu)先級表如下:

Definition l:list TID:=(0::0::1::1::0::nil).

由前文可知系統(tǒng)就緒表中TCB存在2種序關系:優(yōu)先級上有序和優(yōu)先級內(nèi)有序。因此,本文以list復合構建抽象系統(tǒng)就緒表。圖1中OSRdyList索引0～4片段的具體定義如下所示(設TCB地址為1～5):

在定義抽象內(nèi)核數(shù)據(jù)之后,本文通過4個步驟實現(xiàn)針對μC/OS-Ⅲ系統(tǒng)特定數(shù)據(jù)結構斷言的構造。

(1)TCB斷言。其中,PrevPtr,NextPtr和Prio為相對TCB起始地址的偏移常量。任意TCB起始地址不能為0。

(2)良形雙鏈表斷言。根據(jù)性質(zhì)1描述,通過具有同一優(yōu)先級的抽象系統(tǒng)就緒表進行歸納構造:

(3)良形系統(tǒng)就緒表數(shù)組元素斷言。根據(jù)性質(zhì)2描述進行構造,其中函數(shù)length的作用是返回list長度。

(4)系統(tǒng)就緒表斷言。參數(shù)p為系統(tǒng)就緒表內(nèi)存起始地址(相鄰單元地址偏移為12),參數(shù)ll為抽象系統(tǒng)就緒表,參數(shù)prio為優(yōu)先級迭代的起始值,通常為0。

系統(tǒng)優(yōu)先級表斷言的定義過程與系統(tǒng)就緒表類似,在此不再贅述。

5.2 內(nèi)核性質(zhì)的表示

性質(zhì)3描述了具有同一索引的系統(tǒng)就緒表數(shù)組元素與系統(tǒng)優(yōu)先級表元素的一一映射關系。利用上一節(jié)定義的抽象內(nèi)核數(shù)據(jù),本文采用斷言函數(shù)Correspondence描述一致性:

Correspondence的核心規(guī)則是當兩表不為空時,取得各表頭元素,遞歸構造滿足性質(zhì)3的合取范式。根據(jù)性質(zhì)4,本文通過函數(shù)HighestPriority實現(xiàn)優(yōu)先級p是否為抽象系統(tǒng)就緒表最高優(yōu)先級的判斷:

HighestPriority本質(zhì)為系統(tǒng)就緒表從O～p索引元素斷言的合取范式。同理,本文構造系統(tǒng)優(yōu)先級表的最高優(yōu)先級斷言函數(shù)HighestPriorityHash如下:

以上描述內(nèi)核性質(zhì)的3個斷言函數(shù),滿足關系如下:

引理1 對于任意抽象系統(tǒng)就緒表與系統(tǒng)優(yōu)先級表,若滿足一致性,那么對于任意優(yōu)先級p,它是系統(tǒng)就緒表最高優(yōu)先級當且僅當亦是系統(tǒng)優(yōu)先級表最高優(yōu)先級。

證明過程略。

此外,本文還定義了判斷某一TCB是否在抽象系統(tǒng)就緒表中的斷言函數(shù)InRL:

InRL本質(zhì)為依次對每個元素判斷的析取范式。存在關系斷言與系統(tǒng)就緒表最高優(yōu)先級斷言存在如下關系:

引理2 對于任意TCB與抽象系統(tǒng)就緒表,如果TCB存在于抽象系統(tǒng)就緒表中,那么此抽象系統(tǒng)就緒表存在最高優(yōu)先級。

5.3 內(nèi)核實現(xiàn)代碼的推理

本文3.2節(jié)中兩函數(shù)共有的調(diào)度代碼(下劃線部分),轉換成匯編指令后形式化推理過程如下:

調(diào)度代碼的推理過程如下:

關于調(diào)度代碼的驗證工作,有以下3點需要補充說明:

(1)當前任務指針和當前優(yōu)先級分別由全局變量OSTCBCurPtr和OSPrioCur記錄,被選取的任務指針和最高優(yōu)先級分別由全局變量OSTCBHighRdyPtr和

OSPrioHighRdy記錄。對比調(diào)度代碼執(zhí)行前后斷言可以發(fā)現(xiàn)后兩者的變化。

(2)斷言函數(shù)K描述任務棧上的存儲,有3個參數(shù):第1個參數(shù)為基地址b,第2個和第3個參數(shù)都為list。其功能是分別將兩list映射到b-4n至b-4和b至b+4(m-1)的內(nèi)存地址空間(n,m分別為兩list長度)。

(3)函數(shù)OS_PrioGetHighest()獲取最高優(yōu)先級,保存在eax寄存器中返回。以一致性和存在關系為前提,OS_PrioGetHighest()前斷言中的系統(tǒng)優(yōu)先級表最高優(yōu)先級性質(zhì)可以通過引理1、引理2推導出來。

5.4 驗證結果

根據(jù)以上內(nèi)容,本文形式化定義并驗證了最高優(yōu)先級調(diào)度性質(zhì)如下:

以本文定義的機器模型為基礎,從任一滿足一致性與存在性質(zhì)的合法狀態(tài)(C,M,R,pc)出發(fā),系統(tǒng)在運行任務調(diào)度相關代碼后,到達一個新狀態(tài)(C,M′,R′,pc′),新狀態(tài)里全局變量OSPrioHighRdy記錄最高優(yōu)先級,全局指針OSTCBHighRdyPtr記錄待切換的TCB。

除此之外,本文還形式化驗證了內(nèi)存安全性、部分指令代碼的功能正確性,以及推理規(guī)則可靠性等性質(zhì)。表1展示了本文驗證的內(nèi)核調(diào)度函數(shù)列表。整個證明工作共花費數(shù)月時間,Coq代碼總量為5萬多行。

表1 內(nèi)核調(diào)度相關函數(shù)

6 結束語

操作系統(tǒng)任務調(diào)度器由于其結構復雜是驗證工作難點。本文以嵌入式內(nèi)核μC/OS-Ⅲ的任務調(diào)度器為研究對象,基于相關框架和模型,利用Coq輔助證明工具,最終形式化驗證了調(diào)度代碼滿足相關性質(zhì),并且得到可以經(jīng)過機器自動檢查的證明。

本文對μC/OS-Ⅲ任務調(diào)度器的關注重點集中在最高優(yōu)先級如何被正確選取,利用文獻［11］提出的相關邏輯和文獻［12］提出的上下文切換驗證框架,將μC/OS-Ⅲ任務級和中斷級上下文切換整合進μC/OS-Ⅲ任務調(diào)度器形式化工作,是下一步的研究方向。

［1]Micriμm.μC/OS-Ⅲ用戶手冊［EB/OL］.［2014-05-01］.https://doc.micrium.com/pages/viewpage.action?pageId= 10753180.

［2]Coq開發(fā)團隊.Coq證明輔助工具參考手冊［EB/OL］.［2014-05-01］.http://coq.inria.fr.

［3]Reynolds J C.Separation Logic:A Logic for Shared Mutable Data Structures［C］//Proceedings of the 17th AnnualIEEESymposiumonLogicinComputer Science.［S.l.］:IEEE Computer Society,2002:55-74.

［4]Feng X,Shao Z,Vaynberg A,et al.Modular Verification of Assembly Code with Stack-based Control Abstractions［J］.ACMSIGPLANNotices,2006,41(6): 401-414.

［5]Ferreira J F,He G,Qin S.Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK［C］//Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering.［S.l.］:IEEE Press,2012:51-58.

［6]Berdine J,CalcagnoCO,HearnPW.Symbolic Execution with Separation Logic［M］//Jhala R,Igarashi A.ProgrammingLanguagesandSystems.Berlin, Germany:Springer,2005:52-68.

［7]McCreight A.Practical Tactics for Separation Logic［M］// Seidenberg A.Theorem Proving in Higher Order Logics.Berlin,Germany:Springer,2009:343-358.

［8]董 淵,任 愷,王生原,等.字節(jié)碼虛擬機的構造和驗證［J］.軟件學報,2010,21(2):305-317.

［9]Garillot F,Werner B.Simple Types in Type Theory: Deep andShallowEncodings［M］//SchneiderK, Brandt J.Theorem Proving in Higher Order Logics.Berlin,Germany:Springer,2007:368-382.

［10]Hoare C A R.AnAxiomaticBasisforComputer Programming［J］.Communications of the ACM,1969, 12(10):576-580.

［11]Feng X,Shao Z,Dong Y,et al.Certifying Low-level Programs withHardwareInterruptsandPreemptive Threads［J］.ACM SIGPLAN Notices,2008,43(6): 170-182.

［12]Guo Y,Feng X,Shao Z,et al.Modular Verification of Concurrent Thread Management［M］//Jhala R,Igarashi A.Programming Languages and Systems.Berlin,Germany: Springer,2012:315-331.

編輯 金胡考

Verification of μC/OS-ⅢTask Scheduler in Coq

LUO Ercong1,2,GUO Yu1,2
(1.College of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China;
2.Software Security Laboratory,Suzhou Institute for Advanced Study, University of Science and Technology of China,Suzhou 215123,China)

This paper studies the task scheduler in a widely used embedded μC/OS-Ⅲkernel.After selecting core parts from the scheduler,it specifies the properties of the scheduler formally.Based on the separation logic and SCAP,it builds a verification framework including a machine model,operational semantics,assertion languages,and inference rules.In the framework,assertions specifying system data structures and properties are defined,and system code is able to be reasoned about modularly.Finally,the properties of the task scheduler in μC/OS-Ⅲare formally proved,and the entire proof provided by the work are machine checkable.

task scheduler;formal verification;separation logic;Coq proof tool;highest priority

羅爾聰,郭 宇.μC/OS-Ⅲ任務調(diào)度器在Coq中的驗證［J］.計算機工程,2015,41(3):53-58.

英文引用格式:Luo Ercong,Guo Yu.Verification of μC/OS-ⅢTask Scheduler in Coq［J］.Computer Engineering, 2015,41(3):53-58.

1000-3428(2015)03-0053-06

:A

:TP309

10.3969/j.issn.1000-3428.2015.03.010

國家自然科學基金資助青年項目(61202052);國家自然科學基金海外及港澳學者合作研究基金資助項目(61229201)。

羅爾聰(1989-),男,碩士研究生,主研方向:形式化驗證,軟件安全;郭 宇,副教授。

2014-05-05

:2014-05-28E-mail:ecluo@mail.ustc.edu.cn