开源意识流

观点与事件:科技、开源、商业化

谷歌做操作系统上瘾


By Forsaken

尽管每个人(不包括我)都会告诉你,这个年代写新操作系统意义不大,然而谷歌还是隔三岔五地在折腾新的操作系统——钱多得花不完的大厂不止谷歌,为什么只有谷歌爱写新操作系统?

最近,谷歌某团队在博客上宣布了 KataOS 计划,值得注意的是它选用了 seL4 和 Rust。seL4 是目前唯一产业界公认可以通过形式化验证(目前仅限 ARM 平台可过测试)的操作系统内核,Rust 则是目前产业界幻想可以获得安全的语言——这听起来简直就是双剑合璧天下无敌。当然,这样的组合并不是什么全新的尝试,早在若干年前,某自动驾驶厂商就试图用 seL4 + Rust 的组合来给自己的下一代产品增加一些震撼人心的特性。很明显,倘若这样的组合真能够轻松征服世界,那么这家厂商就不再是“某自动驾驶厂商”了,但我们也许还是应该记住这位先行者的名字 Polysync

实际上,谷歌在作出这样的计划前,也曾经考察过 Rust 当前 对于 seL4 的支持,不料却发现主要的支持库 seL4-sys(由 Polysync 开发且维护)早就不再活跃。并且 seL4-sys 的处理方式也不太合谷歌的胃口,它通过自动生成 seL4 函数的绑定来跟 Rust 对接。谷歌这么财大气粗讲究底层的公司,当然是通过汇编直接跟底层函数对接,这样无非就是不能像生成函数绑定那样跨平台,每个 CPU 平台都要写一组支持。但是这种多招几个工程师就能搞定的事情,对谷歌不叫事儿——尽管如此,目前主要还是支持了 RiscV。

作为微内核操作系统,安全方面主要就得靠 capabilities,对于 seL4 来说采用的是 capDL,一套方便定义 capabilities 的定制语言(DSL)。总体来说,seL4 本身确实比较激动人心,seL4 的问题也非常明显,那就是太小。而正是因为小(一万行左右的代码)才有机会完全通过形式化验证,问题也就来了,seL4 相当于一个小萝莉,你要基于她打造一个工业级的完整操作系统,需要大量的工程化。GNU 曾经讨论过是否用 L4 来替换 Mach 来构造下一代的 GNU Hurd,在讨论的时候第一个就淘汰的便是 seL4(seL4 是 L4 微内核家族的实现之一),因为要补充的部分实在太多了。这么来想像,即便你有一个完整的微内核,要打造一个像 GNU Hurd 这样的通用操作系统仍需极大量的工程化开发,而如果你选用了 seL4,那么光是先打造一个完整的微内核就需要大量工程化开发。

当然,谷歌有的是钱,这些都不是问题,问题在于计划的持续性,对吧 Fuchsia?谷歌会是那种长期坚持一个项目直到成功的那种公司吗?

大家自有结论。