Nuttx操作系統(tǒng)進程切換調度實時性的形式化驗證

郝英華 王 瑞 李曉娟

1(首都師范大學信息工程學院 北京 100048) 2(首都師范大學高可靠嵌入式系統(tǒng)技術北京市工程研究中心,電子系統(tǒng)可靠性技術北京市重點實驗室 北京 100048)

0 引 言

隨著我國工業(yè)的快速發(fā)展，工業(yè)機器人[1]發(fā)揮的作用越來越重要。工業(yè)機器人控制系統(tǒng)是工業(yè)機器人的重要部分，控制操作機以完成指定的任務。操作系統(tǒng)處于工業(yè)機器人控制系統(tǒng)的核心地位，但是當前的工業(yè)機器人操作系統(tǒng)面對的一個大挑戰(zhàn)就是實時性問題：目前流行的機器人操作系統(tǒng)ROS實時性不高，這在很大程度上限制了ROS的實際應用。為了滿足實時性[2]需求，越來越多的工業(yè)機器人控制器開始使用實時操作系統(tǒng)作為軟件核心。這些操作系統(tǒng)中最典型是：RTLinux[3]、Vxworks[4]、Window CE[5]、DSP/BIOS[6]等。它們都有著響應快速、穩(wěn)定的優(yōu)點，但很遺憾的是它們的源代碼不開放，價格高昂，增加了開發(fā)成本。而Nuttx操作系統(tǒng)是一款開源的實時操作系統(tǒng)：代碼完全對外開放，CPU可以被高優(yōu)先級進程完全搶占，適應變化能力極強，它有極小的內存開銷，支持多種硬件平臺。

實時調度算法對操作系統(tǒng)的實時性有很大影響,它是提高系統(tǒng)實時性的關鍵技術。在Nuttx實時系統(tǒng)的進程調度中有三種調度策略:先來先服務，時間片輪轉法以及零星調度。這三種調度策略均采用搶占式內核，使CPU總是響應優(yōu)先級最高的進程，進而提高CPU利用率。先來先服務調度是Nuttx操作系統(tǒng)默認的調度，低優(yōu)先級進程可以被高優(yōu)先級進程搶占，實現實時搶占。時間片輪轉調度中時間片被設置為20 ms，這使得CPU的切換次數以平均響應時間相對最優(yōu)，提高CPU利用率。零星調度能夠使零星任務根據服務器的預算值大小在高優(yōu)先級和低優(yōu)先級時之間進行轉換，保證了在每個補充周期T內運行C的時間，使系統(tǒng)能夠及時地響應零星任務。好的實時調度算法可以保證任務在其時限內完成，保證系統(tǒng)的實時性能。因此實時調度算法一直是人們研究的熱點領域。文獻[7]提出了一種稱為準分區(qū)調度的新算法，它能夠調度在同一個處理器上沒有明確截止時間的零星任務。為了響應系統(tǒng)負載變化，該算法使用高效的調度策略在分配的EDF和類似全局的調度規(guī)則之間實現一種切換，動態(tài)地適應了系統(tǒng)變化。模擬結果表明，該策略具有非常低的搶占和開銷，優(yōu)于現有策略。文獻[8]在調度器運行時允許修改策略的前提下，提出了四種調度策略，并使用VarySched調度器進行實驗，評估了四種策略對應用程序運行時間的影響。評估結果表明，一個好的調度策略可以加速應用程序的運行，使程序更早地完成運行。在文獻[9]中，作者提出一種搶占式操作系統(tǒng)內核的驗證框架，并將該框架成功地運用到驗證μC/OS-II操作系統(tǒng)的關鍵模塊中，模塊包括進程調度，中斷處理程序，消息隊列和互斥等。驗證結果表明，μC/OS-II操作系統(tǒng)具有實時性，但它的限制是其C子集不允許功能指針，這需要高階函數的邏輯支持。文獻[10]首先對Web服務器端3種調度策略：先進先出、優(yōu)先排隊、加權公平排隊進行簡要概述和比較評估，然后基于優(yōu)先排隊和加權公平排隊策略提出一種新的調度策略：加權公平排隊。采用測試的方法對每種調度策略的執(zhí)行時間和響應時間進行驗證，驗證結果表明：每種調度策略都有自己的優(yōu)缺點，并且它們優(yōu)勢互補。以上文獻中所用的測試方法都屬于傳統(tǒng)的測試方法，能給出準確的結果。但是，缺點是傳統(tǒng)的測試依賴于測試條件，它們的有效性取決于測試用例的數量和條件，因此，驗證結果具有不完備性。形式化驗證從數學上完備地證明系統(tǒng)是否實現某些功能的方法，所以驗證結果具有準確性和完備性。模型檢測是一種常用于驗證系統(tǒng)正確性的形式化方法之一，基本思想是用有限狀態(tài)機(FSM)表示系統(tǒng)的狀態(tài)轉移結構，用時序邏輯表示設計的性質，如計算樹邏輯和線性時序邏輯。有關模型檢測方法的運用：文獻[11]用形式化驗證方法對任務的可調度性進行分析，并采用驗證工具SCT(schedulability checking tool)與其他工具進行了比較，比較結果顯示,SCT可以提供最為精確的分析結果，但同時也具有最長的分析時間。文獻[12]采用Uppaal時間自動機對任務的可調度性進行建模與分析，結果表明，該建模方法是可擴展的，設計者可以根據它來對特定的系統(tǒng)進行設計驗證。但是以上只是提供了一種方法，并未對某種具體的實時操作系統(tǒng)進行模型檢測，我們可以借鑒為Nuttx操作系統(tǒng)的實時性進行驗證。

綜上，為了保證驗證結果的完備性，本文采用模型檢測的方法對Nuttx操作系統(tǒng)的調度策略進行實時性驗證。首先提出在三種調度策略之間實行一種新的切換策略，使任務到達時能夠根據自身的特點選擇更適合的調度策略：讓優(yōu)先級相同的周期性任務選擇時間片輪轉調度，零星任務采用零星調度，其他的周期性任務默認先來先服務調度。同時采用模型檢測的方法對Nuttx操作系統(tǒng)的三種調度策略之間的切換建立時間自動機模型，然后運用計算樹邏輯公式描述需要驗證的屬性，最后在模型檢測Uppaal[13-14]中進行驗證。

1 時間自動機及CTL[15]公式

定義1Uppaal中的CTL公式

時間自動機[16-17]Uppaal使用計算樹邏輯(CTL)公式來描述屬性。該公式主要分為：狀態(tài)公式和路徑公式。其中，路徑公式描述的是模型中路徑或者軌跡，如表1所示。

表1 Uppaal 中路徑公式

其中，公式inf{表達式}:y用來計算滿足表達式所需要的最小時間y。公式sup:Task().response表示遍歷系統(tǒng)模型的整個狀態(tài)空間后得到的最小上界,也就是最壞響應時間。

2 Nuttx操作系統(tǒng)進程調度簡介

Nuttx是一款實時開源的操作系統(tǒng)[18]。實時操作系統(tǒng)的核心是任務調度。只有保證進程能夠在給定的時間內執(zhí)行完成，才能保證Nuttx的實時性。在Nuttx操作系統(tǒng)中，總體上進程調度的過程如圖1所示。

圖1 進程調度過程示意圖

? 當進程到來時，發(fā)送相應信號啟動調度器。

? 調度器接收到該信號時，會根據不同的調度策略對進程進行相應的處理。

? 進程根據自己的調度策略運行，當運行完成后，會發(fā)送相應的信號通知調度器。

? 調度器接收到該信號，完成調度。

先來先服務調度：系統(tǒng)將先到達的進程調度到運行狀態(tài)。在運行過程中，低優(yōu)先級的進程是可以被高優(yōu)先級的進程搶占，它是默認調度策略。

時間片輪轉調度：在Nuttx操作系統(tǒng)中，時間片輪轉法是為具有相同優(yōu)先級的進程服務的。它將所有優(yōu)先級相同的任務放到一個隊列中，然后每個進程運行20 ms的時間片后，CPU進行上下文切換，當前進程放到隊尾，新的隊首進程進行一個時間片的運行。在切換過程中，運行完一個時間片的進程會放到blocklist隊列中，直到下一次運行時才被移除blocklist隊列。

零星調度：零星調度[19]服務器有一個補充周期、一個預算和兩個優(yōu)先級。當服務器有某些預算時，它處于高優(yōu)先級，從預算時間中減去消耗的時間，預算用盡后立即進入低優(yōu)先級，當服務器的時間被補充后，又重新進入高優(yōu)先級。在一個周期T內：當時間小于預算budget_time時間時，進程每運行一段時間each_time就會丟失lost_time時間，并且這段時間該進程會一直處于高優(yōu)先級。如果時間等于budget_time時，進程就會進入低優(yōu)先級。若時間等于convert_time時，進程會補充前面丟失的lost_time時間。每補充一次lost_time，進程的優(yōu)先級就會回到高優(yōu)先級，并且這段時間可以看作是前半個周期T的對稱運行。這就是Nuttx操作系統(tǒng)零星調度與其他調度不同的地方。它保證了每個進程在每個補充周期T內運行budget_time的時間，保證了系統(tǒng)的實時性。在每一個周期T中，其時間大小值如下所示：lost_time

圖2 零星調度過程示意圖

三種調度之間的切換：我們把所有的任務分為周期性任務和零星任務，讓所有的優(yōu)先級相同的周期性任務采用時間片輪轉調度，零星任務采用零星調度，其他周期性任務默認先來先服務調度。當一個任務到達時，如果是同優(yōu)先級周期任務，將其對應的變量m2設置為1，表示優(yōu)先級相同任務，然后通過中間調度器找到它所對應的時間片輪轉法；如果是零星任務，m3設置為1，對應到零星調度；將如果是普通的周期任務，m1設置為1，對應到先來先服務調度。不管處于哪種調度策略下的任務，都會發(fā)出一個信號，讓當前正在運行的任務暫停，判斷新來的任務優(yōu)先級是否更高，若是，則切換到新來的任務，對CPU加鎖，讓其只運行當前優(yōu)先級最高的任務，直至任務完成再執(zhí)行暫停的任務，這就是實現切換策略的關鍵；若非，則執(zhí)行當前的任務。具體切換過程如圖3所示。

圖3 切換過程示意圖

3 Nuttx中切換調度的形式化建模

本部分對Nuttx系統(tǒng)的三種進程調度之間的切換過程進行了形式化描述。根據Nuttx系統(tǒng)進程間的調度過程建立了8個時間自動機模型，分別是任務模型(4個)、切換模型、先來先服務調度器模型、時間片調度器模型、零星調度器模型。我們給出了部分模型。這里我們重點介紹時間片輪轉調度以及先來先服務調度策略之間的切換，其他調度過程間的切換此相似，不再贅述。

我們把任務標記為三種：把優(yōu)先級相同的任務標記為m2，調用時間片輪轉法；把零星任務標記為m3，采用零星調度法；其他任務標記為m1,默認調度先來先服務算法。

切換模型：如圖4所示，當一個任務到達時，并且滿足總的調度次數大于0時，發(fā)出ready!信號，如果m1等于1，它代表此任務采用先來先服務調度，立即發(fā)出fifo!信號,啟動先來先服務調度器，m1立刻置0，代表該任務已成功找到對應的調度算法；如果m2等于1，它代表此任務采用時間片輪轉調度，立即發(fā)出rr!信號,啟動時間片輪轉法調度器，m2立刻置0，代表該任務已成功找到對應的調度算法；如果m3等于1，它代表此任務采用零星調度，立即發(fā)出ss!信號,啟動零星調度器，m2立刻置0，代表該任務已成功找到對應的調度算法。不管每種調度，任務到達時都會發(fā)出一個ready!信號，讓當前正在運行的任務暫停，判斷新來的任務優(yōu)先級是否更高，若是，則切換到新來的任務，直至任務完成再執(zhí)行暫停的任務；若非，則執(zhí)行當前的任務。

圖4 切換時間自動機

先來先服務模型：如果該任務采用先來先服務調度算法，如圖5、圖6所示。它主要有Task模型和Scheduler模型。Task模型主要有Idle、Ready、Running、Blocked、End、Error幾種狀態(tài)。當任務到達時，發(fā)出ready!信號，調用add()函數，該函數功能是將任務按照到達的先后順序依次放到queue()隊列中，時間t和響應時間response置0，m1置1，目的是通過切換器找到對應的先來先服務調度模型，同時任務的狀態(tài)從Idle狀態(tài)轉換到Ready狀態(tài)。先來先服務調度器模型接收到fifo?信號，首先會判斷queue()隊列的len值是否為1，如果為1，那說明當前只有該任務到達，滿足numnber1大于0的條件，立即發(fā)出run!信號讓該任務運行。任務接收到run?信號后，滿足queue()隊列的首元素時，會立即運行，并轉換到Running狀態(tài)，如果此時再有其他同類型任務到達，即滿足m1等于1并且接收到fifo?信號后,調度器立即發(fā)出wait1!信號。任務接收到wait1?信號后，立即從Running狀態(tài)轉換為Blocked狀態(tài)，此時調度器立刻發(fā)出run!信號。任務接收到run?信號，并且滿足是queue()隊列的首元素時，會重新運行轉換到Running狀態(tài)，實現高優(yōu)先級搶占；如果不為1，那說明目前到達的任務不止1個，還會有其他非同類型任務已經到達，立即發(fā)出lock!信號。其他正在運行的任務接收lock?信號后，立即發(fā)出inform!信號。對應的調度器接收到inform?信號后，會一直等到高優(yōu)先級非同類型任務運行完成后接收到unlock1?信號后，重新發(fā)出run!讓目前queue()隊列首元素運行，目的是實現同一時刻CPU只能運行一個任務。當先來先服務的任務數number1等于0時，如果其他非同類型任務還沒有執(zhí)行完，則發(fā)出unlock2!。其他非同類型接收到unlock?信號后，會立即運行，而當前調度器回到Init狀態(tài)。當執(zhí)行時間ax大于最好情況執(zhí)行時間并且小于最壞情況執(zhí)行時間時，任務運行完畢，發(fā)出done!信號，并調用remove()函數，將該任務從queue()隊列移除，同時將success[]置1，表示該任務已經完成，響應時間response置0，此時任務進入到End狀態(tài)，響應時間不變化。當時間t等于任務周期時，立即發(fā)出ready!信號，表示任務周期性來到，同時將時間t和response置0，success[]置0，并且調用add()函數，開始新一輪的調度。在任務模型中，只要時間t大于等于Deadlines[]，任務就會進入Error狀態(tài)。

圖5 先來先服務任務時間自動機

圖6 先來先服務調度器時間自動機

時間片輪轉模型：如果該任務采用時間片輪轉調度算法，如圖7、圖8所示。在Nuttx系統(tǒng)中，時間片輪轉調度是針對相同優(yōu)先級的任務而進行的調度。所以在模型中，每個任務的優(yōu)先級都是相同的，設計了兩個跟圖7一樣的優(yōu)先級相同的任務模型。它主要有Task模型和Scheduler模型。Task模型主要有Idle、Ready、Running、Blocked、End、Error幾種狀態(tài)。其他調度情況與先來先服務模型一致，這里不再贅述。重點介紹當運行時間ticks等于時間片值，任務運行一個時間片并且CPU允許上下文切換時，調度器發(fā)出stop!信號。任務接收到stop?信號后，調用change()函數。change()函數的作用是按照優(yōu)先級大小將任務放到queue()隊列的對應位置，讓新的隊首元素運行一個時間片的時間，并且任務從Running態(tài)轉換到Blocked狀態(tài)，cpu進行一次切換。若此時再有新的同類型任務到達，接收到rr?信號并且滿足m2等于1的條件時，會立即發(fā)出wait!信號。任務接收到wait?信號后調用change()函數，進入到Blocked態(tài),當滿足隊首元素時，再重新運行一個時間片的時間。

圖7 時間片輪轉任務間自動機

圖8 時間片輪轉調度器時間自動機

4 屬性驗證

在本節(jié)中，我們使用CTL公式描述這些屬性，并且在Uppaal中對它們進行驗證。Uppaal軟件運行的計算機環(huán)境為：2.60 GHz的雙核CPU，內存為4.00 GB。一級緩存為128 KB，二級緩存為512 KB，三級緩存為3.0 MB，內存工作頻率為1 198 MHz。驗證結果如表2、表3所示。

表2 屬性描述以及驗證結果 ms

表3 CPU最壞響應時間與截止時間 ms

屬性1：對于任何一個待驗證的系統(tǒng)而言，保證系統(tǒng)能夠正常運行，不發(fā)生死鎖是一個基本的前提，對于操作系統(tǒng)而言也是如此，它可以用如下CTL公式證明：A[ ] not deadlock。如表2所示，該屬性被滿足，這說明：說明整個系統(tǒng)不會出現死鎖，該系統(tǒng)可以正常運行。

屬性2：在進程調度過程中，同一時刻CPU只允許一個進程占用，不能允許多個進程同時運行：A[]Task(0).Running+Task(1).Running<=1。如表2所示，該屬性被滿足。這說明：整個系統(tǒng)在同一時刻CPU只允許一個任務運行。

屬性3：進程在調度過程中，不超出截止時間，表明進程能夠在不超出截止時間內完成，屬性如下：A[] forall(i: pid_t ) not Task(i).Error。如表2所示，該屬性在切換前不被滿足，切換后得到滿足。這說明：切換使得原本不能在截止時間內完成的任務完成了相應的操作，優(yōu)化了實驗結果。

屬性4：每個進程，只要到達，就要在不超出截止時間內成相應的操作，這也是操作系統(tǒng)進程調度的實時性體現。屬性用CTL公式可描述為：Task(i).Ready-->Task(i).End。如表2所示，該屬性在切換前不被滿足，切換后得到滿足。這說明：切換使每個到達的任務都能完成相應的操作。

屬性5：計算出每個進程從到達到完成的時間。該屬性描述為：inf{success[i]==1}:time。如表2所示，我們根據該屬性計算出CPU的平均響應時間，然后對切換前后的CPU平均響應時間進行比較，結果顯示，切換后的平均響應時間小于切換前的平均響應時間。這說明：切換提高了CPU的平均響應時間。

屬性6：計算出每個任務的最壞響應時間，與截止時間進行比較，進而保證任務在最壞情況下不超出截止時間而被完成，滿足實時性。屬性CTL描述如下：

sup:Task(0).response,Task(1).response,Task(2).response,Task(id).response。根據表3，我們對切換后的調度進行最壞響應時間與截止時間的比較，可以看出每種任務的最壞響應時間都不大于截止時間，這說明：切換使得任務能夠在不超出給定的時間內完成相應的操作，滿足了系統(tǒng)的實時性。

5 結 語

Nuttx是一款實時開源的操作系統(tǒng)，它能保證系統(tǒng)的實時性。因此對Nuttx系統(tǒng)的實時性進行驗證很有必要。本文首次提出對以上三種調度策略進行切換，使得任務到達時能夠根據自身的特點去選擇適合自己的調度策略，以便得到更快的響應。首先對調度的切換過程進行了時間自動機建模，然后用計算樹邏輯(CTL)公式描述了進程調度實時性的相關屬性，最后在模型驗證工具Uppaal中進行了驗證。驗證結果表明新的切換策略使得Nuttx操作系統(tǒng)在給定的時間內能夠完成相應的操作，滿足了實時性需求。本文對于測試和評估實時操作系統(tǒng)性能有一定的借鑒作用。Nuttx操作系統(tǒng)能夠滿足工業(yè)機器人控制系統(tǒng)的實時性需求，因此在工業(yè)機器人控制領域有著很好的應用前景。