这学期OS的课程挑战性实验,我尝试着对清华祖传教学OS uCore进行验证。按照验证的传统,这个项目被命名为CertiCore。但最后的结果是,我们只完成了对uCore物理页面分配器的验证。我想从某种意义上说,这次尝试算是失败了,不过既不是一败涂地,也不是功败垂成。细细想来,最主要的原因还是我们对OS验证的经验不足。我们并没有太多开发OS的经历,也许甚至搞不清楚OS的典型性质。我们对OS验证的经验,只有几篇论文而已。

验证技术是否已经变成了一种阳春白雪呢?经历这次尝试,我的最大感受是,如果你没有验证的经验,那么即使有完备的逻辑和形式理论基础也很难推进。即便是符号执行这样最为基础,最为自动化的验证方式,对刚接触的人来说一样深奥难懂。

当我们学期初阅读Serval的论文时,以为其中两周验证CertiKOS的例子确凿无疑,而且认为我们也能很快地完成uCore的验证。但事实是,你需要大量的经验,对工具的极度熟悉,才能快速地完成系统的验证。

这种必需的经验就是领域专用知识,一种独属于某个领域的约定与直觉。毫无疑问,Serval并不是给普罗大众,而是OS验证专家准备的。它提高的是精通验证者的效率,而不是OS开发者的效率。其中充斥着大量工程实践固化下的概念,如果你没有经验,就必须去读Serval的源码,而且不一定能读懂;至于论文,它只会介绍基本原理。嗯,非常象牙塔,非常学术范。

当然,除此之外Serval本身也有不少缺陷。作为一个基于Rosette的库,自然而然地,必须同时忍受Rosette带来的好处与坏处——糟糕的调试环境,为了支持符号执行而不显式处理异常,以及Lisp风格带来的不便。另外,没有文档也是一个大问题。

不过Serval的确提供了它宣称的验证方便性。只可惜这学期的大量开发精力,实际上都投入到了环境搭建和工具调整上。要说实际的验证工作,其实也就五百来行不够精炼的代码。一个页面分配器,现在看来不过几个接口,算法也不算复杂,却耗费了三个人月的时间。回忆开发过程,大部分时间都是在debug,让我感觉不是在开发验证系统,而是在和软件工程失败产物做斗争。

工具的不易用和经验的不足(也许还有懒惰),使得开发举步维艰。这个过程中最大的障碍,我们也许知道最后一刻才弄懂,那就是验证系统的边界——什么是可以被验证的,而什么是无法被验证的?我们对验证如此缺乏经验,以至于定下了验证uCore宏内核的目标。即使这个内核如此微小,其复杂度却依然远远超越了现有的大部分验证内核。我们寄希望于用符号执行的方法细粒度验证页面分配算法,从而在其上耗费了过多的时间。

这些教训都让我想到,也许验证一个系统最关键的不在于逻辑或者形式化理论,而是对被验证系统的认知和理解,从而能够清楚地选择验证的目标,使其契合使用的验证工具的表达力。系统验证本身如此,开发验证工具也是如此。没有目标,没有深思熟虑的验证是难以为继的。