0×00 布景

形式化办法(Formal Methods)在我们一般人眼中是十分巨大上的东西，最多也便是当年在课堂上听说过罢了，在实践工作中很少有人运用。

前一阵子Reddit上的一个帖子让高冷的形式化办法也上了一次头条，故事便是国外某技能团队运用形式化办法验证了Java中一些排序算法的正确性，可是在验证Timsort排序算法时发现了Bug，所以便向Java开源社区陈述了这个Bug，一起给出了经过形式化办法验证过的修正计划。原本是个大快人心的结局，成果Java开源社区并没选用他们的修正计划，而是选用了另一个Dirty Solution……(固执，就不听你的，不服你来咬我啊)

回归到这个Bug自身，我们来看看形式化办法是怎样大显神通的

0×01 什么是Timsort

说起排序，我们比较了解的有冒泡、挑选、插入排序，当然还有奇特的快排(Quick Sort)，Timsort是个什么鬼?

Timsort算法是Tim Peters于2002年提出的一个排序算法(以自己姓名命名的……)，比较其他排序算法算是后起之秀了。我们点评一个排序算法的好坏要从许多方面衡量，看看下面这张图

其他杂乱无章的排序算法就不看了(也看不明白……)，看看那些眼熟的排序算法，快排尽管均匀时刻杂乱度十分好，可是在最优、最坏时刻杂乱度以及算法的稳定性上来说都不如Timsort

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

那么这么优异的一个算法，怎样会呈现Bug呢?当然这并非Timsort算法思维的问题，而是写程序的人犯的过错，原因便是Timsort太杂乱了(比较其他算法而言)，开端写程序的人无意中疏忽了一种比较特别的状况……

要了解这个Bug产生的原因，我们先来看看Timsort算法的原理

0×02 Timsort原理

简略来说，Timsort是一种结合了归并排序和插入排序的混合算法，它根据一个简略的现实，实践中大部分数据都是部分有序(升序或降序)的。

Timsort排序算法中界说数组中的有序片段为run，每个run都要求单调递加或严厉单调递减(确保算法的稳定性)，如下图所示

抛开一些细节，Timsort排序算法可以归纳成两步：

第一步便是把待排数组划分红一个个run，当然run不能太短，假如长度小于minrun这个阈值，则用插入排序进行扩大。

第二步将run入栈，当栈顶的run的长度不满意下列约束条件中恣意一个时，

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

则运用归并排序将其间最短的2个run兼并成一个新run，终究栈空的时分排序也就完结了。

下面以一个实例进行阐明，这个比方中我们设置minrun=4，也便是说run的最小长度不能小于4。每划分出一个run就将其入栈，如下图所示

留意，此刻栈顶的run是不满意约束条件的，因为此刻runLen[0] < runLen[1]，所以要对这两个run进行归并，当然这个进程运用的是归并排序。

假如遇到有序片段长度小于minrun，则要进行补齐，如下图所示

#p#

留意，此刻栈顶run是满意约束条件的，10 > 5 + 4，5 > 4，因而不需求进行归并。

终究数组元素个数缺乏minrun了，只能作为一个run了

此刻栈顶的run又不满意约束条件了，5 < 4 + 2，所以需求进行归并。后续进程如下图所示

这样排序进程就完结了~有的同学或许会有疑问，为什么要有那个古怪的约束条件呢?每次入栈的时分直接进行归并不行吗?这主要是考虑到归并排序的功率问题，因为将一个长序列和一个短序列进行归并排序从功率和价值的视点来看是不划算的，而两个长度均衡的序列进行归并排序时才是比较合理的也比较高效的。

当然这儿我们疏忽了许多细节问题，如minrun的长度核算，插入排序和归并排序详细完结中的一些技巧。更多关于Timsort排序算法的细节请参阅OpenJDK 源代码阅览之 TimSort

0×03 Timsort中的Bug

了解了Timsort算法的进程和原理，如同没有什么逻辑上的问题，那么这个Bug究竟出在哪呢?

这个Bug恰恰呈现在那个约束条件上，因为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
    }
  }
}

在大多数状况下，仅查看栈顶的3个run是否满意这个约束条件是可以确保整个栈内一切run均满意该约束条件。可是在一些特别的状况下就不行了，如下面这个栈(右侧为栈顶)

120, 80, 25, 20, 30

对照上面的源码，因为25 < 20 + 30，25 < 30，所以将25和20两个run进行兼并，此刻栈内的状况变为

120, 80, 45, 30

因为80 > 45 + 30，45 > 30，满意约束条件，此刻归并就停止了。可是留意栈里的其他run，120 < 80 + 45，这是不满意约束条件的，而因为我们只判别了栈顶的run，因而在这儿就留下了“危险”。

在大多数状况下，这个问题没什么大不了，不影响我们平常一般的排序操作，因为我们的数据没有那么多，更不会很多呈现上述状况。可是这个国外技能团队精心结构了一个Array，成功的让Timsort算法报了java.lang.ArrayIndexOutOfBoundsException这个过错。他们还把复现这个过错的代码放在了github上，代码请戳这儿

为什么是这个古怪的过错?这就和Timsort算法的Java完结中恳求栈空间的巨细有关系了，看看原始代码

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

其间len表明输入的Array的长度，stackLen表明恳求的栈的巨细。那么上面的那些边界条件和古怪的数字是怎样核算出来的呢?#p#

其实很简略，考虑这样一个问题：怎样结构一个序列使其每个元素均满意Timsort算法的约束条件呢?可以设序列中的元素为E(n)，只需满意E(n) = E(n-1) + E(n-2) + 1即可，是不是和Fibonacci数列十分相似?用程序完结一下

# -*- coding: utf-8 -*-
# 栈顶之上加一个辅佐空run，栈顶的run长度设置为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个区间呢?为什么挑选minrun=16呢?我个人认为是为了省劲，横竖能确保栈空间够用就行。

可是请留意这是在抱负条件下，也便是栈内每个run都有必要满意这个约束条件。而我们方才给出了一个反例，那么在反例呈现的状况下，用到栈的巨细会比我们料想的要大一些。

国外的这个技能团队在论文中算出了最坏状况下用到栈的巨细，并画出了一张表

第二行表明最坏状况下需求用到栈的巨细，第三行表明Timsort算法实践给出的栈巨细(见上文JDK源码)。有意思的是在Array长度为65536时，开端Java中Timsort设定栈的长度为19，可是后来有人陈述了Bug，也便是说这个Bug在实践中是呈现过的。可是Java开源社区的程序员或许无法定位这个Bug的本源，只好从外表处理这个问题，在后来的更新中把栈的巨细改成了24……(不过的确也处理了问题)可是危险仍然存在的，可以看到在Array长度为67108864时，最坏状况下用到的栈巨细41，而Java中Timsort设定的长度为40。所以只需精心结构一个Array，就能触发这个Bug。可是如本文最初所说，Java开源社区的程序员仍然不从根本上处理问题，仍是用老办法，添加栈的巨细……(老子就会这一个技能，不服你来咬我啊)

0×04 怎样发现这个Bug

这个Bug是十分隐晦的，除非脑洞大开，不然很少人能从代码上来看出问题。那么测验呢?如同也不太可行，依托自动化生成的测验集好像很难生成一个可以触发这个Bug的Array(尤其是在Array长度较大的状况下)，这个团队也是在深入研讨了这个Bug的基础上才结构出一个能触发Bug的Array。这又回到了一个老问题上，怎样证明一个程序的正确性?程序运转1万次、100万次不犯错并不能阐明程序没有问题(请参阅各类缝隙)，因为测验集不能确保掩盖一切履行途径，要证明一个程序的正确性我们有必要要选用其他手法。

这就需求用到形式化办法了，现实上有关程序正确性证明的研讨早在图灵和冯·诺依曼时期就开端了，当然要实在把握这个理论需求太多逻辑和演算的常识(什么程序规约、前置断语、后置断语，横竖我也不明白)……我们就简略看看这个国外技能团队是怎样用形式化东西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为什么能掩盖一切的履行途径而软件测验不能?因为KeY并没有生成实践的测验数据集，而是把程序符号化，经过符号逻辑和演算就可以考虑一切或许的履行途径。(此处省掉一万字……)

当然即便是运用KeY进行程序正确性证明工作量也不小，原始的Timsort.java文件大约900多行，而参加了JML之后大约1400多行……简直每个函数、循环、条件句子前面都要参加很多断语。当然这也并非无用功，至少我们发现了这个反程序猿的Bug

当然他们还给出了一个经过KeY验证过的正确的处理计划，业界良知啊，感受一下

/*@ 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

原先只判别了栈顶的3个run，现在我们判别栈顶4个run，经过这样改动之后即可确保栈内一切run均满意约束条件了，并且请放心大胆的运用，因为这是经过形式化办法验证过的~#p#

0×05 玉兔月球车中的Bug

那么形式化办法这么杂乱，花这么大力气只发现了一个小Bug，并且他人压根就不配合，投入和报答有点不成正比啊……没错，形式化办法有时分便是这么吃力不讨好，并且平常也没有哪个程序员会用形式化办法来验证自己的程序。那么究竟什么人在用形式化办法呢?就现在来看要么是有钱的大公司，如Amazon、Facebook，要么是有钱的国家级工程项目，也便是我们下面要说的玉兔月球车。

航空航天技能向来都是国家归纳实力的一个重要表现，我们都是不计成本的往里砸钱……当然航空航天技能一起也以高危险著称，一个小零件毛病也有或许形成严重后果，挑战者号升空后爆破便是因为一个O型环失效引发的连锁反应，12亿美元的航天飞机瞬间荡然无存，7名机组人员罹难……正因为其危险如此之高，所以哪怕多花点钱能进步1%的安全性也是值得的。

所以形式化办法一个十分重要的商场便是航空航天范畴，去年在新加坡举办的第19届形式化办法世界研讨会上，有两个来自我国的团队进行了陈述，偶尔的是他们陈述的标题都与玉兔月球车相关，一个与月球软着陆操控相关，另一个与玉兔月球车操控体系相关。而我有幸在其他场合聆听过其间用形式化办法验证玉兔操控体系那个团队的陈述，实在感受到形式化办法的强壮与杂乱。

下图是玉兔月球车操控体系的一个简化版别(实在体系中有30多个使用使命)，这儿只列出6种

图中左边主要是一些使命，中心的是音讯行列(包含发送行列和接纳行列)，右侧是CAN bus总线，操控指令和传感器数据都是经过它传递的。详细的意义见下表：

留意从Task1到Task6的优先级是顺次递减的，Task1的优先级为6，Task6的优先级为1。

Task5是一个周期性恳求数据的使命，预期能4ms接纳到完好的遥测数据，如下图所示

在正常状况下，发送数据1帧，接纳数据6帧。这一进程耗时1×0.192(Task3Send)+0.5(IMU呼应时刻)+6×0.192(Task5)=1.844ms，预设的4ms等待时刻是满意的。可是在几年的开发和测验进程中，开发人员偶尔调查到几回“遥测超时过错”：即估计可以在4ms内完结的Task5产生超时，未能获取到完好数据。

因为这个体系十分杂乱，且操作体系的使命调度具有随机性，多使命体系的某次履行难以重现，要调查实时操作体系对使命的调度十分困难。更重要的是，这个过错呈现的次数很少，一年或许才呈现一次，很难总结过错呈现的条件。

然后又是形式化办法进场了，我们请看下面几张图

关于这些图不想说太多(此处省掉一万字……)，有人说这不是自动机嘛，没错，自动机原本便是形式化办法中十分重要的一部分。第一个图是抢占式使命的时刻自动机模型，对应Task1，第二个图是周期性使命的时刻自动机模型，对应是Task2、Task5和Task6，第三个图是偶发使命的时刻自动机模型，对应Task3、Task4#p#

据该团队的女博士介绍，画这几张图花了她半年的时刻，并且仍是在有东西辅佐的状况下!

当然终究问题的原因找到了，在T时刻，满意以下条件时，呈现遥测过错：

1. Task6在T时刻安排妥当，Task2和Task5在8ms后安排妥当
2. T+7ms后，有地上指令（Task1）

在这种状况下，因为Task1和Task2优先级均高于Task5，分别向SendQueue写入4帧和8帧数据，尔后Task5才被调度，向SendQueue写入1帧数据，此刻SendQueue中现已累积了13帧数据，耗时13×0.192+0.5+6×0.192=4.148ms，超过了4ms，因而产生了超时过错。处理办法也很简略，进步Task3的优先级，让其及时将数据发送出去即可防止此类过错。

别看我们说起来轻描淡写的，这个问题困扰了工程师们好几年，用形式化办法验证也花了半年多的时刻，并且仅仅对其间6个进程进行了形式化验证!假如要对悉数30多个进程进行正确性验证，那画面太美我不敢看……

0×06 总结

其实写到这儿发现有点跑题，本文并没有讲太多关于形式化办法自身的东西……从我个人的视点来看，我们一般人的确也没有必要花大力气去研讨它，可是却有了解它的必要，当你遇到怪异却又无法处理的问题而失望时，无妨找找研讨形式化办法的专业人士，或许会有起色。

就现在而言，形式化办法的门槛过高，很难将其大规模使用。但可以想像，假如有一天，形式化办法可以在缝隙发掘、互联网安全等范畴遍及，必将引发席卷核算机安全范畴的风暴。

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. 信息物理交融体系操控软件的计算模型查验

5. OpenJDK 源代码阅览之 TimSort