實時操作系統中有限優先級反轉的驗證

張 嘯 然

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

1 引 言

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

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

圖1 無限優先級反轉Fig.1 Unbounded priority inversion

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

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

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

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

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

圖2 概覽Fig.2 Overview

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

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

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

2 相關工作

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

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

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

總的來說，相比以前的工作，本文的工作具有以下優點：

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

2)本文的方案可以被運用于多種保證有限優先級反轉性質的協議中.

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

3 優先級反轉的形式化定義

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

3.1 抽象內核模型和優先級反轉

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

定義1.優先級反轉

狀態Σ對于任務t是優先級反轉的，當且僅當該狀態中任務t的優先級高于正在被調度執行的任務.

3.2 跡和有限優先級反轉

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

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

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

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

由于無限優先級反轉是在表達系統未來的行為.為了便于表達和理解，定義中使用了線性時態邏輯進行表達.關于線性時態邏輯的定義可以參考圖3.

圖3 線性時態邏輯Fig.3 Linear temporal logic

定義2.無限優先級反轉

自然地，有限優先級反轉的定義可以被定義如下：

定義3.有限優先級反轉

需要注意的是，有限優先級反轉的成立與否并不僅僅取決于調度算法及各操作系統接口的實現.該性質與用戶對于操作系統接口的正確使用也是息息相關的.

具體的，考慮如下情形：

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

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

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

2)系統不會發生死鎖.

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

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

定義4.有限臨界區假設

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

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

定義5.無死鎖假設

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

無死鎖假設也是必要的，由于當死鎖發生時系統實際上難以正確運行，討論有限優先級反轉也就什么意義了.

定義6.正確嵌套假設

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

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

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

定義7.用戶正確操作

4 高層機器與語言的刻畫

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

4.1 高層程序

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

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

4.2 高層機器狀態

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

圖6 抽象狀態Fig.6 Abstract state

4.3 語義及跡的生成

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

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

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

定義8.跡的生成

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

定義9.所有合法跡

其中：

高層系統滿足有限優先級反轉定義如下：

定義10.高層系統有限優先級反轉

5 在抽象規范層面證明有限優先級反轉

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

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

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

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

定義11.合理調度策略

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

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

其中

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

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

合理調度策略成立當且僅當對任意初始狀態Σ，根據代碼ω執行一步后變為狀態Σ′時，若性質ProperlySched對Σ成立，則其一定對Σ′成立.

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

定義12.釋放信號量后執行調度

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

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

定義13.創建任務后執行調度

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

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

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

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

除此之外，系統接口也需要符合以下規范：

定義14.信號量獨立性

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

定義15.優先級維持

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

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

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

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

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

定義16.合理有限優先級反轉系統接口

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

WaitIndependent(ω)∧PrioPresv(ω)

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

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

定理1.合理OS實現蘊含有限優先級反轉

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

6 底層有限優先級反轉

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

6.1 底層機器及語言

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

圖7 底層程序和狀態Fig.7 Concrete program and state

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

圖8 底層語法Fig.8 Concrete syntactic

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

定義17.底層跡生成

定義18.底層合法跡

6.2 底層有限優先級反轉

底層有限優先級反轉的定義也與高層類似：

定義19.底層系統有限優先級反轉

6.3 精化關系

由于本文在之前已經在協議規范層面證明了有限優先級反轉性質，所以現在的問題可以歸結為如何證明一個具體實現的協議代碼確實是一個正確的規范實現.為此，定義如下的精化關系：

定義20.精化關系

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

由精化關系和有限優先級反轉定義，可以得到以下定理.

定理2.精化關系維持有限優先級反轉

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

6.4 CSL風格的關系程序邏輯

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

6.5 邏輯可靠性

定理3.邏輯可靠性

?OO,├ O:O→O?O

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

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

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

7 驗證POSIX標準協議

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

7.1 抽象內核狀態實現

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

圖10 抽象系統狀態實例Fig.10 Abstract kernel state

7.2 優先級保護協議規范

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

圖11 優先級保護協議形式化定義Fig.11 Formal definition of PPP

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

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

定理4.優先級保護協議保證有限優先級反轉成立

HOSFUPI(OPPP)

7.3 優先級繼承協議規范

當系統采用優先級繼承協議時，如果一個低優先級的任務阻塞了一個高優先級的任務，系統會在其阻塞期間將該任務的優先級調至高優先級.形式化的定義可參見圖12.

與優先級保護協議類似，可以證明得到以下定理：

定理5.優先級保護協議保證有限優先級反轉成立

HOSFUPI(OPIP)

7.4 精化關系證明

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

定理6.C語言版本的優先級保護協議能保證有限優先級反轉

OSFUPI(OPPP)

定理7.C語言版本的優先級繼承協議能保證有限優先級反轉

OSFUPI(OPIP)

至此，本文完整的證明了底層實現的協議能夠滿足有限優先級反轉的要求.

圖12 優先級繼承協議形式化定義Fig.12 Formal definition of PIP

8 總 結

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

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