首页 >> 数学 >> 文章

计算无处不在。

走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动。从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃。计算机能做的事情越来越多,甚至超越了它们的制造者。上个世纪末,深蓝凭借前所未有的搜索和判断棋局的能力,成为第一台战胜人类国际象棋世界冠军的计算机,但它的胜利仍然仰仗于人类大师赋予的丰富国际象棋知识;而仅仅十余年后,Watson却已经能凭借自己的算法,先“理解”问题,然后有的放矢地在海量的数据库中寻找关联的答案。长此以往,工具将必在更多的方面超越它的制造者。而这一切,都来源于越来越精巧的计算。

计算似乎无所不能,宛如新的上帝。但即使是这位“上帝”,也逃不脱逻辑设定的界限。

第一位发现这一点的,便是图灵。

相信每个人都见识过Windows那令人忧郁的蓝屏或者黑屏吧。有时因为它,一个上午的工作一瞬间毁于一旦,这就不仅是令人忧郁而是令人抓狂了。在这个时候,你是否会在心中大声咒骂那帮写程序不小心让蓝屏一而再再而三出现的程序员呢?但程序员也不是铁打的,他们也会犯错误。而且对于商业软件来说,在上市之前会进行大量的测试,即使有程序错误溜过去了,大多也可以通过打补丁来修复。

但是对于某些软件来说,情况就麻烦得多了。

无妄之灾

在1996年的一个不能说的日子,欧洲航天局第一次发射了新研制的Ariane 5运载火箭。在起飞37秒之后,新火箭很想不开地开花了。这令砸了几亿欧元进去的欧洲航天局非常不爽。经过调查,专家组发现,事故的罪魁祸首竟然是短短的一段代码。

803a

Ariane 5爆炸场景

在Ariane 5的软件中,有一部分代码是直接来自它的前辈Ariane 4。由于Ariane 4当时非常成功,所以大家觉得这样做没什么问题,根据新的参数稍微修改一下代码就好了。问题是,修改并不完全。有一行代码需要将64位浮点数转换成16位整数,他们认为不会出现什么问题,所以没有进行修改。也没有测试这段代码。

就是这行代码,因为Ariane 5比前辈Ariane 4强力得多,于是在Ariane 4上没有问题的这行代码,在Ariane 5上发生了溢出错误:那个64位的浮点数代表的数值超出了16位整数可以表达的范围。在出错后,备用代码系统被启动,其中包含着同样的一行代码。结果就是整个系统被锁死了。更为讽刺的是,这行代码所在的函数,对于Ariane 5来说是不必要的。这场事故完全就是人祸。

经过这场事故之后,欧洲航天局大为震怒,决定要一劳永逸地解决Ariane 5的问题。他们的要求相当大胆:Ariane 5的软件代码,正式使用前要证明它们不会出现毁灭性的错误,比如不会溢出,不会死循环等等。

这其实并非易事。

停机定理

我们复习一下停机问题:是否存在一种算法,给定任意的程序和输入,都能在有限的时间内判断该程序在给定的输入下是否会停止?正是图灵,证明了这一点是不可能做到的。于是,要编写一个能判断程序会不会进入死循环的算法,这是不可能的。但对于其他类型的程序错误,能否用算法判定呢?

很可惜,这也是不可能的。实际上,我们可以将停机问题规约为检测错误的问题。假设我们有一个程序P,能检测某段代码是否会出现除以零的错误,而我们想要借助这个程序判断某个图灵机在给定的输入下会不会停止。我们可以怎么做呢?首先,对于给定的图灵机和输入,我们可以机械化地将它们转化为一段不用除法但能够模拟该图灵机的代码,然后在模拟结束之后,强行计算1/0。我们将这段代码称为T。代码T在执行时会出现除以零的错误,当且仅当图灵机会停机。然后,我们将代码T输入程序P。于是,既然程序P能判定任意的代码会不会出错,那么就相当于它能判定任意的图灵机会不会停机,而这是不可能的。停机问题不存在普遍的算法,也就是说证明代码无误同样没有普遍算法。

但是,欧洲航天局的任务是否完全不可能完成呢?那倒也不是。停机定理只是说明了不存在程序能正确判定所有程序是否会停止,但欧洲航天局只需要证明Ariane 5的软件代码这一个程序不会出错,所以这条路也没有完全被堵死。

那么,有什么办法呢?

抽象释义

虽然我们不能判定所有程序是否不会出错,但我们能有效判定某些程序不会出错。比如说,如果一个程序没有任何循环语句或者跳转语句,那么这个程序最终肯定停止。但如果程序有循环语句又怎么办?这时,我们并不能确定程序会不会停止,而最保险的办法就是说“我不知道”。

这就是抽象释义(Abstract Interpretation)方法的根本:先抽象出程序的某些信息,再对这些信息进行自动分析,来尝试确定程序是否有着我们想要的性质,比如说不会死循环、不会溢出等等。我们不强求完美的分析,不强求能够识别出所有不出错程序。但为了安全起见,我们要求这种分析是可靠的,也就是说,如果分析的结果认为程序有着我们想要的性质,那么这个结论就不会出错。正是因为这样的权衡取舍,抽象释义方法才能正确有效地实行。

galois-connection

Galois connection,来自Cousot课件

根据抽象出来的信息多少,不同的抽象释义方法判断同一种性质的效果也不一样。一般来说,抽象出的信息越详细,能识别的拥有某种性质的程序就越多,相应地计算时间也越长。如何在性能和识别率之间做取舍,也是一门复杂的学问,对于不同的应用和数据结构,需要开发不同的抽象方法和自动分析算法。

多种抽象方法还有另一个优点。如果某个程序有着我们想要的性质,但是手头上的抽象释义方法又不能确定时,我们可以换用更精细的、利用更多信息的抽象方法。直接改写代码也是一种规避分析失败的方法。例如,我们想要证明某段代码不会出错,但某种抽象释义方法指示在某句代码上可能会有问题,那么我们可以通过修改代码,换用更加谨慎的处理方法,来保证抽象释义方法能确认新的代码不出问题。

抽象释义方法的奠基者是法国的Patrick Cousot和Radhia Cousot。这对夫妻档总结了一些对程序进行自动形式证明的方法,在此之上提出了抽象释义方法,将其形式化严格化。他们对抽象释义方法的推广也功不可没。除了Ariane 5的代码之外,在别的一些关键应用处的代码也利用抽象释义方法进行了至关重要的验证。一个例子是空中客车A380的控制代码,经过Patrick Cousot的一个小组开发的抽象释义软件Astrée验证,证明了这些控制代码运行时,不会产生像死循环、溢出或者被零除之类的一些软件问题,从而也给安全系数多加了一层保险。

768px-Patrick_Cousot_0743-cRadhiaCousot--Picture

Cousot夫妇,图片来自Wikipedia

不过,抽象释义方法只能证明程序有着某种我们想要的性质,不能说明程序是否完成了我们希望的任务。有没有办法做到这一点呢?

形式证明

有一种激进的做法:让程序员在编写代码的同时,给出这段代码确实完成了给定任务的数学证明

要给出这种证明,首先要解决的就是如何将“代码完成了给定任务”转换成数学命题。程序代码可以相当容易用逻辑表达,但代码需要完成什么任务,这只有程序员才知道。所以,要让程序员在编写代码的同时给出证明,为的是让程序员能用逻辑的形式确定这个函数的功能,如此才能得到要证明的命题。这种想法不仅仅是数学家的纸上谈兵。对于某些关键系统,多么微小的疏失都会导致极其严重的后果,人们愿意几乎不惜一切代价防止错误的发生,而对于计算机程序而言,又有什么比数学更坚实的基础呢?

要贯彻这种想法,在编写程序之前,必须先选择一种逻辑体系以及描述它的一种形式语言。这种形式语言必须贯穿整个代码编写的过程:先用形式语言描述程序的输入、输出、功能与限制,然后利用这种与形式语言相近的编程语言去具体编写代码,最后还要利用形式语言给出编写的代码能完美无瑕疵地实现所需功能的数学证明。这种做法又被称为演绎验证,是所谓的“形式化验证”的手段之一。

但数理逻辑毕竟不是一门容易的学科,数学证明对于很多人来说大概比编写代码要困难得多。所以,演绎验证多数也只会用在那些不容有失的关键系统,比如说牵涉人数众多的公共交通设施。例如,在1998年开始运营的巴黎地铁14号线,就是一条全自动的地铁,列车上没有司机,安全行驶也全靠传感器和软件,调度也只需要在控制室点点鼠标就能增加或减少投入运营的列车数量。于是,安全在很大程度上在于软件的可靠性。在控制列车的计算机中,某些与乘客安全休戚相关的关键代码是利用演绎验证编写的。在2012年,巴黎历史最悠久的地铁1号线也从人工运营转到与14号线同系列的全自动化系统。现在,这两条地铁线每天接待的人数加起来超过一百万,但从未因为自动化系统的错误导致乘客伤亡。从笔者的经验来说,它们可以算是巴黎最可靠的地铁线。

800px-Metro-Paris-Ligne-4-2-Stati

巴黎地铁14号线,图片来自Wikipedia

但仅有代码的正确性可能还不足以保证程序同样正确,因为代码毕竟不是程序,计算机不能直接执行代码。我们需要另一种名为“编译器”的程序。编译器是将程序员写的代码翻译成计算机能读懂的、用机器语言写就的程序。即使代码是正确的,如果编译器有问题,得出的程序还是可能出错。要避免这个问题,我们同样需要利用数学方法加固编译器这一环。

贯彻这种设计理念的一个例子是一个叫CompCert的C编译器,它由法国计算机科学家Xavier Leroy和他的小组编写。编译器的任务就是进行忠实的代码翻译,确保源代码和目标代码的行为一致。这一点至关重要,否则即使代码是正确的,也不能保证编译生成的程序不出问题。然而,现代的编译器在优化模式下,其实并不能确保忠实的编译。CompCert要解决的就是这个问题。在编写CompCert的时候,对于编译程序的每一步操作,都附带一个数学证明,确保代码的语义不变。因此,数学证明的正确性保证了CompCert编译器会完全忠实地将代码翻译成机器语言。

但即使机器语言是正确的,也还不能完全保证最后执行结果的正确性,因为程序总需要输入输出,而这些功能是由操作系统保证的。如果操作系统本身有错误,即使执行的程序本身是正确的,由于操作系统的问题,也不能保证我们看到的结果是正确的。如果想将数学证明的保证贯彻到底,还需要对操作系统下工夫。这就是seL4所做的事情。seL4是一个微内核,可以看成操作系统的核心。它的每一个功能都附带一个数学证明,在对硬件做一定的假设之后,数学证明的正确性可以保证它提供的功能都会产生我们预先设定的行为。只要硬件不出错,seL4就会正确运行。

当然,一个自然的问题是,如果硬件出错怎么办?硬件的错误可以分为逻辑性错误和物理性错误。前者例如Intel当年在芯片上除法的错误,现在主流硬件厂商早已吸取教训,用演绎验证的方法加固他们的硬件设计;后者例如宇宙射线令硬盘数据出错,这即使是多复杂的证明也避免不了,只能自求多福。尽管数学方法不能保证错误不存在,但至少将可以避免的问题全数避免,这本身就有着莫大的价值。

real_programmers

(或者可以利用宇宙射线……?)(图片来自xkcd)

关于

本文改写自果壳网文章《不会出错的程序,是这样炼成的》。

0
相关文章

26 Responses to “计算的极限(十二):不会出错的程序”

  1. a说道:

    文中的[pic: ]等文字是表示一张图片吗?是图挂了?

  2. 蛤蛤说道:

    不能说的日子,秒懂。。

  3. Peter说道:

    问一个很简单的问题:使用"演绎验证"作为关键词在 Google 上搜索,第一页根本就没有任何相关的结果。作为一个程序猿,我很想研究一下相关的东西啊。请问怎么才能查到相关的资料啊(英文也行)?

    • bobcy说道:

      建议抽空看下一本大概5万字的薄书《牛津通识读本:科学哲学》,你就能彻底搞懂“演绎验证”这个概念了。

      • Peter说道:

        书厚我都不怕(只要不是像《GEB》那么厚就行),有过来人愿意给我推荐书比什么都好。

        • gundamfire说道:

          GEB... 我想这本东西的副标题应该是OMG或者WTF……

    • 方弦说道:

      演绎验证是deductive verification,形式化验证是formal verification。

      • Peter说道:

        Thanks . 正好以后深造的时候准备拿无错化程序设计当作研究方向。

        • 方弦说道:

          华东师大在这方面做得不错的,不过我不清楚他们具体集中在什么方面。我只知道他们有做Abstract interpretation和Model checking,形式证明似乎还没有开始做,不过我的消息不算灵通。

  4. 卅二日说道:

    三个硬盘并行

  5. 卅二日说道:

    三个硬盘并行,少数服从多数。

    • 方弦说道:

      那不凑巧其中两个硬盘同一个地方恰好几乎同时被宇宙射线打中怎么办?概率的确很微小,但毕竟不像逻辑错误那样可以完全排除。

      • Wei说道:

        如果一个硬盘被击中的概率是1%,那两个同时被击中的概率就是0.01%,以此类推,可以把概率小到可接受的程度。没人会要求概率上100%不出错,在下一秒钟太阳也有一定的几率会爆炸

        • 方弦说道:

          但毕竟有些时候这个“可接受”的概率非常非常小,尤其是人命关天的时候,而这就是形式化方法的优势:它不是减少出错的概率,而是从逻辑上保证不会出错。

  6. wxd356说道:

    那么,我们可以先在程序结尾添加一个死循环,让它永远不能停止运行,然后在程序中每一处除法前,先检测除数是否为零,在除数为零时,强行停止程序。那么,原本的程序不会出现错误,当且仅当改动后的程序不会停机。于是,我们就将证明某段代码不存在某种错误,规约为停机问题。
    ————————————————————————
    这里有问题吧,前面的结论是“通用的证明任意程序是否可停机的程序不存在”,但是用这种方法(添加一个死循环)得到的程序只是所有程序的一个子集,前面的停机问题的结论不能证明这种程序是否停机的程序是否存在吧

    • wxd356说道:

      也许恰好那样构造出来的程序的集合是总的集合里可以判断是否停机的程序的子集

    • wxd356说道:

      而且你还要证明构造前的这个程序是可以停机的,之后的不能停机,才能证明是因为要验证的那个条件错误

    • wxd356说道:

      作者至少还要指出这个子集上也是不可判断是否停机的

    • 方弦说道:

      谢谢你的回复,这里的确是我把规约方向搞反了。我很快会改正这一部分(15号之前),谢谢指出错误!

  7. 兔巴哥1985说道:

    看到那对法国夫妻和巴黎14号地铁线,我怎么突然想起法国机场那台 Windows 3.1 的电脑。。。

  8. azbo说道:

    程序稍微大一点,就跪了

  9. foundout说道:

    skylake在测试Prime95时特殊的死机问题算是没加固成功么ಠ౪ಠ

    • 方弦说道:

      他们也不是每项功能都用形式验证的,毕竟成本太高。这次Prime95的事情我猜是超线程在同一个流水线下内存访问的某种竞态条件。这一部分是形式验证大概不会涉及到的,因为一般做的加固就是对硬件模型的关键处进行model checking,而内存访问的调度大概不包含在里边。

  10. gundamfire说道:

    那张图最后一格笑点没领悟到……是因为我不懂EMACS的原因么?

  11. Enzojz说道:

    又看到巴黎m14跑十年没发现bug的梗了。每做一次50128培训就会被提一次的fm梗

  12. 赵明毅说道:

    一开始看到更新了很兴奋,过了一会发现很熟悉,还以为是我自己的即视感,结果看到最后才发现……果然是我看过的啊