赵翔鹏的Blog Xiangpeng's Thinkpad

Singularity：基于形式化方法的操作系统？

Singularity是微软研究院（Redmond）做的研究性操作系统，设计目标是dependable，trustworthy的OS，用了很多formal methods的技术，现在已经出了v1版。

看到Singularity的消息，很多人的第一反应是：这个会取代Windows吗？我认为暂时不会。如同开发者所说，it's a Journey not a Destination。这只是一个research性质的prototype OS，没考虑实用，完全没有考虑向后兼容性。但是，Singularity采用的很多概念都是值得我们思考的。其实Singularity在两三年前就陆续有一些paper发出来了，只是现在才进入大众的视线。

InfoQ上有一篇介绍Singularity的不错文章。建议也看看这篇已发表的paper：Singularity: Rethinking the Software Stack。读了之后感觉很震撼：原来OS还可以这样做！

下面是paper中的一些highlight：

• Singularity的绝大部分是用Spec#写的，是C#的一个变种。
  （天哪，用managed code写操作系统？garbage collection不是非常会影响性能吗？）
• Software Isolated Process（SIP）：所有的进程都跟kernel放在同一个地址空间里，靠软件验证，而不是硬件保证地址访问的正确：任何指针都只能指向进程拥有的内存，不能指向别人的内存。因为减少了kernel mode/user mode的切换，减少了context switch，所以极大地提高了性能。根据paper里的统计数据，Singularity中create process，create thread的速度比Unix, Windows都高了一个数量级。（garbage collection的影响看来不是那大。）
• 基于通道的Contract：看到了进程代数中熟悉的通道概念，还有c!, c?符号。进程之间的通讯完全通过通道，而不是共享变量。据作者说，这借鉴了Web service verification的思想，做一些static conformance checking，让compiler来确保程序（Web server，device driver……）按照预先设计的protocol运行，太牛了。（Tony Hoare提出的Grand Challenges其中就包括verifying compiler）而且，paper中还举了一个channel传channel的例子。（pi演算的实际应用？）
• Manifest-based Programs：每个程序都要带一个manifest说清楚自己做什么（就像java applet那样），这样在安装之前就知道这个程序会不会干坏事。怎么知道的？因为有static checking。因为程序在安装前就知道它是安全的，所以安装时可以做更多的事：比如，把kernel级的代码inline嵌入到程序中，这样又减少了context switch的负担。安装时还会把字节码编译到native code，而不是JIT即时编译，这样又能提高速度。最终，Sing#代码也可以跟C++的代码比比速度了。（不知道static checking的效率如何。）

因为用了很多formal methods的技术，所以程序都是出乎意料的健壮。InfoQ的文章里提到，File System的作者写好代码之后……没有任何测试，竟然直接就可以运行了，没有发现任何bug。

不过还是有一些问题我不太清楚。比如scheduler的实现，跟传统的OS不同，把ready list分成了unblocked list和preempted list两个list，说是有利于频繁地等待的线程的调度。不知道为什么以前的OS没有这样做？

我觉得Singularity最神奇的地方是，能把这样一个概念性的东西给实现出来了，要知道formal methods向来是好看不好用。

可以想象，在实现的过程中肯定遇到了无数的困难，做了无数的trade-off。比如他们提到在实现channel时，为了防止出现unbounded channel，要求contract每次变迁至少包含一个发送“!”和一个接收“?”，以保证channel不会被一大串发送动作撑爆。还好，这个看似严格的要求并没有导致太大的麻烦。garbage collection的算法也有很多细微的问题，文章第3.4节提到了一些。看了paper里列举的种种困难和解决办法，更让人觉得这是个很牛的操作系统了。：）