0×00 背景

形式化方法(Formal Methods)在我們一般人眼中是非常高大上的東西，最多也就是當年在課堂上聽說過而已，在實際工作中很少有人使用。

[[131154]]

前一陣子Reddit上的一個帖子讓高冷的形式化方法也上了一次頭條，故事就是國外某技術團隊利用形式化方法驗證了Java中一些排序算法的正確性，但是在驗證Timsort排序算法時發(fā)現(xiàn)了Bug，于是便向Java開源社區(qū)報告了這個Bug，同時給出了經過形式化方法驗證過的修復方案。本來是個皆大歡喜的結局，結果Java開源社區(qū)并沒采納他們的修復方案，而是采用了另一個Dirty Solution……(任性，就不聽你的，不服你來咬我啊)

回歸到這個Bug本身，我們來看看形式化方法是如何大顯身手的

0×01 什么是Timsort

說起排序，我們比較熟悉的有冒泡、選擇、插入排序，當然還有神奇的快排(Quick Sort)，Timsort是個什么鬼?

Timsort算法是Tim Peters于2002年提出的一個排序算法(以自己名字命名的……)，相比其他排序算法算是后起之秀了。我們評價一個排序算法的好壞要從許多方面衡量，看看下面這張圖

 其他亂七八糟的排序算法就不看了(也看不懂……)，看看那些眼熟的排序算法，快排雖然平均時間復雜度非常好，但是在最優(yōu)、最壞時間復雜度以及算法的穩(wěn)定性上來說都不如Timsort

所以Timsort成為了Python內置的排序算法，后來Java SE 7、Android和GNU Octave都引入了Timsort排序算法。

那么這么優(yōu)秀的一個算法，怎么會出現(xiàn)Bug呢?當然這并非Timsort算法思想的問題，而是寫程序的人犯的錯誤，原因就是Timsort太復雜了(相比其他算法而言)，當初寫程序的人無意中忽略了一種比較特殊的情況……

要理解這個Bug產生的原因，我們先來看看Timsort算法的原理

0×02 Timsort原理

簡單來說，Timsort是一種結合了歸并排序和插入排序的混合算法，它基于一個簡單的事實，實際中大部分數(shù)據(jù)都是部分有序(升序或降序)的。

Timsort排序算法中定義數(shù)組中的有序片段為run，每個run都要求單調遞增或嚴格單調遞減(保證算法的穩(wěn)定性)，如下圖所示

 拋開一些細節(jié)，Timsort排序算法可以概括成兩步：

第一步就是把待排數(shù)組劃分成一個個run，當然run不能太短，如果長度小于minrun這個閾值，則用插入排序進行擴充。

第二步將run入棧，當棧頂?shù)膔un的長度不滿足下列約束條件中任意一個時，

1. runLen[n-2] > runLen[n-1] + runLen[n]
2. runLen[n-1] > runLen[n]

 則利用歸并排序將其中最短的2個run合并成一個新run，最終棧空的時候排序也就完成了。

下面以一個實例進行說明，這個例子中我們設置minrun=4，也就是說run的最小長度不能小于4。每劃分出一個run就將其入棧，如下圖所示

 注意，此時棧頂?shù)膔un是不滿足約束條件的，因為此時runLen[0] < runLen[1]，所以要對這兩個run進行歸并，當然這個過程使用的是歸并排序。

如果遇到有序片段長度小于minrun，則要進行補齊，如下圖所示

#p#

注意，此時棧頂run是滿足約束條件的，10 > 5 + 4，5 > 4，因此不需要進行歸并。

最后數(shù)組元素個數(shù)不足minrun了，只能作為一個run了

 此時棧頂?shù)膔un又不滿足約束條件了，5 < 4 + 2，所以需要進行歸并。后續(xù)過程如下圖所示

 這樣排序過程就完成了~有的同學可能會有疑問，為什么要有那個奇怪的約束條件呢?每次入棧的時候直接進行歸并不行嗎?這主要是考慮到歸并排序的效率問題，因為將一個長序列和一個短序列進行歸并排序從效率和代價的角度來看是不劃算的，而兩個長度均衡的序列進行歸并排序時才是比較合理的也比較高效的。

當然這里我們忽略了許多細節(jié)問題，如minrun的長度計算，插入排序和歸并排序具體實現(xiàn)中的一些技巧。更多關于Timsort排序算法的細節(jié)請參考OpenJDK 源代碼閱讀之 TimSort

0×03 Timsort中的Bug

了解了Timsort算法的過程和原理，好像沒有什么邏輯上的問題，那么這個Bug到底出在哪呢?

這個Bug恰恰出現(xiàn)在那個約束條件上，因為Timsort算法設置這個約束條件的是為了保證歸并排序時兩個子序列長度是均衡的，隱含的一層意思是棧內所有run都應該滿足該約束條件(即使不在棧頂)，即對2 <= i <= StackSize-1，也必須滿足

1. runLen[i-2] > runLen[i-1] + runLen[i]
2. runLen[i-1] > runLen[i]

 JDK源碼中的注釋也說明了這一點

/**
 * Examines the stack of runs waiting to be merged and merges adjacent runs
 * until the stack invariants are reestablished:
 *
 *     1. runLen[i - 3] > runLen[i - 2] + runLen[i - 1]
 *     2. runLen[i - 2] > runLen[i - 1]
 *
 * This method is called each time a new run is pushed onto the stack,
 * so the invariants are guaranteed to hold for i < stackSize upon
 * entry to the method.
 */
private void mergeCollapse() {
  while (stackSize > 1) {
    int n = stackSize - 2;
    if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) {
      if (runLen[n - 1] < runLen[n + 1])
         n--;
      mergeAt(n);
    } else if (runLen[n] <= runLen[n + 1]) {
      mergeAt(n);
    } else {
      break; // Invariant is established
    }
  }
}

 在大多數(shù)情況下，僅檢查棧頂?shù)?個run是否滿足這個約束條件是可以保證整個棧內所有run均滿足該約束條件。但是在一些特殊的情況下就不行了，如下面這個棧(右側為棧頂)

120, 80, 25, 20, 30

 對照上面的源碼，因為25 < 20 + 30，25 < 30，所以將25和20兩個run進行合并，此時棧內的情況變?yōu)?/p>

120, 80, 45, 30

 由于80 > 45 + 30，45 > 30，滿足約束條件，此時歸并就終止了。但是注意棧里的其他run，120 < 80 + 45，這是不滿足約束條件的，而由于我們只判斷了棧頂?shù)膔un，因此在這里就留下了“隱患”。

在大多數(shù)情況下，這個問題沒什么大不了，不影響我們平時一般的排序操作，因為我們的數(shù)據(jù)沒有那么多，更不會大量出現(xiàn)上述情況。但是這個國外技術團隊精心構造了一個Array，成功的讓Timsort算法報了java.lang.ArrayIndexOutOfBoundsException這個錯誤。他們還把復現(xiàn)這個錯誤的代碼放在了github上，代碼請戳這里

為什么是這個奇怪的錯誤?這就和Timsort算法的Java實現(xiàn)中申請?？臻g的大小有關系了，看看原始代碼

int stackLen = (len <    120  ?  5 :
                len <   1542  ? 10 :
                len < 119151  ? 19 : 40);
runBase = new int[stackLen];
runLen = new int[stackLen];

其中l(wèi)en表示輸入的Array的長度，stackLen表示申請的棧的大小。那么上面的那些邊界條件和奇怪的數(shù)字是怎么計算出來的呢?#p#

其實很簡單，考慮這樣一個問題：怎樣構造一個序列使其每個元素均滿足Timsort算法的約束條件呢?可以設序列中的元素為E(n)，只要滿足E(n) = E(n-1) + E(n-2) + 1即可，是不是和Fibonacci數(shù)列非常類似?用程序實現(xiàn)一下

# -*- coding: utf-8 -*-
# 棧頂之上加一個輔助空run，棧頂?shù)膔un長度設置為minrun=16
known = {0: 0, 1: 16}
def fib(n):
    if n in known:
        return known[n]
    res = fib(n - 1) + fib(n - 2) + 1
    known[n] = res
    return res
ns = [5,10,19,39,40]
for n in ns:
    fibsum = 0
    for i in range(n):
        fibsum += fib(i)
    print "n={0},sum={1}".format(n,fibsum)
# 輸出
# n=5,sum=119
# n=10,sum=1541
# n=19,sum=119150
# n=39,sum=1802926565
# n=40,sum=2917196495
# ps:Java中int的最大值為2147483648，1802926565 < 2147483648 < 2917196495

 那么為什么只選取4個區(qū)間呢?為什么選擇minrun=16呢?我個人認為是為了省事，反正能保證?？臻g夠用就行。

但是請注意這是在理想條件下，也就是棧內每個run都必須滿足這個約束條件。而我們剛才給出了一個反例，那么在反例出現(xiàn)的情況下，用到棧的大小會比我們預想的要大一些。

國外的這個技術團隊在論文中算出了最壞情況下用到棧的大小，并畫出了一張表

 第二行表示最壞情況下需要用到棧的大小，第三行表示Timsort算法實際給出的棧大小(見上文JDK源碼)。有意思的是在Array長度為65536時，最初Java中Timsort設定棧的長度為19，但是后來有人報告了Bug，也就是說這個Bug在實際中是出現(xiàn)過的。然而Java開源社區(qū)的程序員可能無法定位這個Bug的根源，只好從表面解決這個問題，在后來的更新中把棧的大小改成了24……(不過確實也解決了問題)但是隱患依然存在的，可以看到在Array長度為67108864時，最壞情況下用到的棧大小41，而Java中Timsort設定的長度為40。所以只要精心構造一個Array，就能觸發(fā)這個Bug。然而如本文開頭所說，Java開源社區(qū)的程序員依然不從根本上解決問題，還是用老辦法，增加棧的大小……(老子就會這一個技能，不服你來咬我啊)

0×04 如何發(fā)現(xiàn)這個Bug

這個Bug是非常隱晦的，除非腦洞大開，否則很少人能從代碼上來看出問題。那么測試呢?好像也不太可行，依靠自動化生成的測試集似乎很難生成一個能夠觸發(fā)這個Bug的Array(尤其是在Array長度較大的情況下)，這個團隊也是在深入研究了這個Bug的基礎上才構造出一個能觸發(fā)Bug的Array。這又回到了一個老問題上，怎樣證明一個程序的正確性?程序運行1萬次、100萬次不出錯并不能說明程序沒有問題(請參考各類漏洞)，因為測試集不能保證覆蓋所有執(zhí)行路徑，要證明一個程序的正確性我們必須要采用其他手段。

這就需要用到形式化方法了，事實上有關程序正確性證明的研究早在圖靈和馮·諾依曼時期就開始了，當然要真正掌握這個理論需要太多邏輯和演算的知識(什么程序規(guī)約、前置斷言、后置斷言，反正我也不懂)……我們就簡單看看這個國外技術團隊是怎樣用形式化工具KeY來驗證Timsort算法的

KeY是為Java平臺設計的程序正確性證明工具，使用Java Modeling Language(JML)在程序中加入一些斷言，就像這樣

/*@ private normal_behavior
  @ requires
  @   n >= MIN_MERGE;
  @ ensures
  @   \result >= MIN_MERGE/2;
  @*/
private static int /*@ pure @*/ minRunLength(int n) {
  assert n >= 0;
  int r = 0;      // Becomes 1 if any 1 bits are shifted off
  /*@ loop_invariant n >= MIN_MERGE/2 && r >=0 && r<=1;
    @ decreases n;
    @ assignable \nothing;
    @*/
  while (n >= MIN_MERGE) {
    r |= (n & 1);
    n >>= 1;
  }
  return n + r;
}

 那些前面有一個奇怪的@符號的就是斷言了，其實無非就是定義輸入要滿足哪些條件，輸出要滿足哪些什么條件。比如對于一個排序算法而言，輸入的斷言就是一個非空的Array，輸出的斷言應該是一個有序的Array且元素集合與輸入一致。

有人說這樣就能保證程序的正確性嗎?KeY為什么能覆蓋所有的執(zhí)行路徑而軟件測試不能?因為KeY并沒有生成實際的測試數(shù)據(jù)集，而是把程序符號化，通過符號邏輯和演算就可以考慮所有可能的執(zhí)行路徑。(此處省略一萬字……)

當然即便是使用KeY進行程序正確性證明工作量也不小，原始的Timsort.java文件大約900多行，而加入了JML之后大約1400多行……幾乎每個函數(shù)、循環(huán)、條件語句前面都要加入大量斷言。當然這也并非無用功，至少我們發(fā)現(xiàn)了這個反程序猿的Bug

當然他們還給出了一個經過KeY驗證過的正確的解決方案，業(yè)界良心啊，感受一下

/*@ private normal_behavior
@ requires
@      \dl_elemInv(runLen, (\bigint)stackSize-4, MIN_MERGE/2)
@   && \dl_elemBiggerThanNext(runLen, (\bigint)stackSize-3)
@   && stackSize > 0;
@ ensures
@    (\forall \bigint i; 0<=i && i<(\bigint)stackSize-2;
@        \dl_elemInv(runLen, i, MIN_MERGE/2))
@ && \dl_elemBiggerThanNext(runLen, (\bigint)stackSize-2)
@ && (   (\sum int i; 0<=i && i

 原先只判斷了棧頂?shù)?個run，現(xiàn)在我們判斷棧頂4個run，經過這樣改動之后即可保證棧內所有run均滿足約束條件了，而且請放心大膽的使用，因為這是經過形式化方法驗證過的~#p#

0×05 玉兔月球車中的Bug

那么形式化方法這么復雜，花這么大力氣只發(fā)現(xiàn)了一個小Bug，而且別人壓根就不買賬，投入和回報有點不成正比啊……沒錯，形式化方法有時候就是這么吃力不討好，而且平時也沒有哪個程序員會用形式化方法來驗證自己的程序。那么到底什么人在用形式化方法呢?就目前來看要么是有錢的大公司，如Amazon、Facebook，要么是有錢的國家級工程項目，也就是我們下面要說的玉兔月球車。

航空航天技術歷來都是國家綜合實力的一個重要表現(xiàn)，大家都是不計成本的往里砸錢……當然航空航天技術同時也以高風險著稱，一個小零件故障也有可能造成嚴重后果，挑戰(zhàn)者號升空后爆炸就是因為一個O型環(huán)失效引發(fā)的連鎖反應，12億美元的航天飛機瞬間化為烏有，7名機組人員遇難……正因為其風險如此之高，所以哪怕多花點錢能提高1%的安全性也是值得的。

所以形式化方法一個非常重要的市場就是航空航天領域，去年在新加坡舉行的第19屆形式化方法國際研討會上，有兩個來自中國的團隊進行了匯報，巧合的是他們匯報的題目都與玉兔月球車相關，一個與月球軟著陸控制相關，另一個與玉兔月球車控制系統(tǒng)相關。而我有幸在其他場合聆聽過其中用形式化方法驗證玉兔控制系統(tǒng)那個團隊的報告，切實感受到形式化方法的強大與復雜。

下圖是玉兔月球車控制系統(tǒng)的一個簡化版本(真實系統(tǒng)中有30多個應用任務)，這里只列出6種

 圖中左側主要是一些任務，中間的是消息隊列(包括發(fā)送隊列和接收隊列)，右側是CAN bus總線，控制命令和傳感器數(shù)據(jù)都是通過它傳遞的。具體的含義見下表：

 注意從Task1到Task6的優(yōu)先級是依次遞減的，Task1的優(yōu)先級為6，Task6的優(yōu)先級為1。

Task5是一個周期性請求數(shù)據(jù)的任務，預期能4ms接收到完整的遙測數(shù)據(jù)，如下圖所示

 在正常情況下，發(fā)送數(shù)據(jù)1幀，接收數(shù)據(jù)6幀。這一過程耗時1×0.192(Task3Send)+0.5(IMU響應時間)+6×0.192(Task5)=1.844ms，預設的4ms等待時間是足夠的。但是在幾年的開發(fā)和測試過程中，開發(fā)人員偶然觀察到幾次“遙測超時錯誤”：即預計能夠在4ms內完成的Task5發(fā)生超時，未能獲取到完整數(shù)據(jù)。

由于這個系統(tǒng)十分復雜，且操作系統(tǒng)的任務調度具有隨機性，多任務系統(tǒng)的某次執(zhí)行難以重現(xiàn)，要觀察實時操作系統(tǒng)對任務的調度非常困難。更重要的是，這個錯誤出現(xiàn)的次數(shù)很少，一年可能才出現(xiàn)一次，很難總結錯誤出現(xiàn)的條件。

然后又是形式化方法出場了，大家請看下面幾張圖

 關于這些圖不想說太多(此處省略一萬字……)，有人說這不是自動機嘛，沒錯，自動機本來就是形式化方法中非常重要的一部分。第一個圖是搶占式任務的時間自動機模型，對應Task1，第二個圖是周期性任務的時間自動機模型，對應是Task2、Task5和Task6，第三個圖是偶發(fā)任務的時間自動機模型，對應Task3、Task4#p#

據(jù)該團隊的女博士介紹，畫這幾張圖花了她半年的時間，而且還是在有工具輔助的情況下!

當然最終問題的原因找到了，在T時刻，滿足以下條件時，出現(xiàn)遙測錯誤：

1. Task6在T時刻就緒，Task2和Task5在8ms后就緒
2. T+7ms后，有地面命令（Task1）

 在這種情況下，由于Task1和Task2優(yōu)先級均高于Task5，分別向SendQueue寫入4幀和8幀數(shù)據(jù)，此后Task5才被調度，向SendQueue寫入1幀數(shù)據(jù)，此時SendQueue中已經累積了13幀數(shù)據(jù)，耗時13×0.192+0.5+6×0.192=4.148ms，超過了4ms，因此發(fā)生了超時錯誤。解決方法也很簡單，提高Task3的優(yōu)先級，讓其及時將數(shù)據(jù)發(fā)送出去即可避免此類錯誤。

別看我們說起來輕描淡寫的，這個問題困擾了工程師們好幾年，用形式化方法驗證也花了半年多的時間，而且只是對其中6個進程進行了形式化驗證!如果要對全部30多個進程進行正確性驗證，那畫面太美我不敢看……

0×06 總結

其實寫到這里發(fā)現(xiàn)有點跑題，本文并沒有講太多關于形式化方法本身的東西……從我個人的角度來看，咱們一般人確實也沒有必要花大力氣去研究它，但是卻有了解它的必要，當你遇到詭異卻又無法解決的問題而絕望時，不妨找找研究形式化方法的專業(yè)人士，或許會有轉機。

就目前而言，形式化方法的門檻過高，很難將其大規(guī)模應用。但可以想像，如果有一天，形式化方法能夠在漏洞挖掘、互聯(lián)網安全等領域普及，必將引發(fā)席卷計算機安全領域的風暴。

0×07 參考資料

1. Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it)

2. OpenJDK’s java.utils.Collection.sort() is broken: The good, the bad and the worst case

3. Formal Verification of Lunar Rover Control Software Using UPPAAL

4. 信息物理融合系統(tǒng)控制軟件的統(tǒng)計模型檢驗

5. OpenJDK 源代碼閱讀之 TimSort