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

羅爾聰,郭 宇

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

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

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

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

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

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

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

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

1 概述

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

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

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

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

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

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

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

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

2 相關(guān)工作

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

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

3 驗證方法

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

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

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

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

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

為了確保調(diào)度過程的正確執(zhí)行,調(diào)度代碼對兩表進行操作時必須滿足以下4個關(guān)鍵性質(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)先級表對應(yīng)元素取值存在雙射關(guān)系:元素數(shù)量為0(不為0),當且僅當系統(tǒng)優(yōu)先級表對應(yīng)元素為0(為1)。本文稱之為一致性。

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

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

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

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

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

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

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

本文選取Intel i386架構(gòu)的一個簡化子集作為運行μC/OS-Ⅲ內(nèi)核的硬件平臺,并采用程序邏輯SCAP推理本文所研究的任務(wù)調(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個關(guān)系謂詞來定義,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)是用來推理帶有結(jié)構(gòu)化堆棧操作的機器指令的類似Hoare邏輯［10］的推理系統(tǒng)。SCAP邏輯的推理過程以指令序列為單位。函數(shù)由一些指令序列構(gòu)成,程序規(guī)范以函數(shù)為單位定義。程序規(guī)范是一個二元組,包含一個前條件與一個描述函數(shù)前后狀態(tài)變化的二元關(guān)系:

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

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

5 驗證實現(xiàn)

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

造過程。

5.1 內(nèi)核數(shù)據(jù)結(jié)構(gòu)的表示

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

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

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

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

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

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

(3)良形系統(tǒng)就緒表數(shù)組元素斷言。根據(jù)性質(zhì)2描述進行構(gòu)造,其中函數(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)先級表元素的一一映射關(guān)系。利用上一節(jié)定義的抽象內(nèi)核數(shù)據(jù),本文采用斷言函數(shù)Correspondence描述一致性:

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

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

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

引理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ì)為依次對每個元素判斷的析取范式。存在關(guān)系斷言與系統(tǒng)就緒表最高優(yōu)先級斷言存在如下關(guān)系:

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

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

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

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

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

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

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

(2)斷言函數(shù)K描述任務(wù)棧上的存儲,有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寄存器中返回。以一致性和存在關(guān)系為前提,OS_PrioGetHighest()前斷言中的系統(tǒng)優(yōu)先級表最高優(yōu)先級性質(zhì)可以通過引理1、引理2推導(dǎo)出來。

5.4 驗證結(jié)果

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

以本文定義的機器模型為基礎(chǔ),從任一滿足一致性與存在性質(zhì)的合法狀態(tài)(C,M,R,pc)出發(fā),系統(tǒng)在運行任務(wù)調(diào)度相關(guān)代碼后,到達一個新狀態(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)度相關(guān)函數(shù)

6 結(jié)束語

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

本文對μC/OS-Ⅲ任務(wù)調(diào)度器的關(guān)注重點集中在最高優(yōu)先級如何被正確選取,利用文獻［11］提出的相關(guān)邏輯和文獻［12］提出的上下文切換驗證框架,將μC/OS-Ⅲ任務(wù)級和中斷級上下文切換整合進μC/OS-Ⅲ任務(wù)調(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é)碼虛擬機的構(gòu)造和驗證［J］.軟件學(xué)報,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-Ⅲ任務(wù)調(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

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

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

2014-05-05

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