三个微内核和四个名字的故事

译者注：本文摘取下面博客的一部分内容说明。因为OKL4和seL4这些概念比较乱，作者的说明能帮我们稍微理清一下。

http://microkerneldude.wordpress.com/2012/10/02/giving-it-away-part-2-on-microkernels-and-the-national-interes/

L4

在OK Labs公司成立之前曾有一个NICTA的L4微内核版本。这是开源的Pistachio微内核的演变，最早主要是在德国的卡尔斯鲁厄大学开发的。我们已经把它移植到了一些架构，包括ARM，针对在资源受限的嵌入式系统做了一些优化，并设计和实现了一些非常酷的方式来进行快速的上下文切换（比Linux快50倍）。我们也将Linux移植到它上面运行（即使用L4作为一个管理程序来支持虚拟化的Linux）。得益于快速上下文切换技术，虚拟化的Linux比原生的Linux跑的还要快。

正如我所说，该微内核从一开始就是开源的（BSD许可证），并一直保持开源。而BSD许可证将允许我们fork出一个封闭源代码的版本（同时承认原作者），这将是一件愚蠢的事。我们希望我们的研究成果尽可能被广泛的使用。

高通

在2004年，L4微内核获得高通的关注。他们有两个具体的（而且相当不同的）的技术问题，因此他们正在寻找解决方案。一个需要快速，具有内存保护功能的实时内核。另一个是要求ARM上的Linux虚拟化。我们的L4提供了这两个问题的解决方案，这就是全部的内容。

高通公司聘请NICTA以帮助他们在他们的无线通信芯片部署L4。最初的评估和原型进行得很顺利，他们决定用L4作为其固件的基础。

这就是OK Labs公司成立所发生的一切。事实上，在我们创建了OK Labs公司时，第一台内置L4的手机已经在日本开始发售了！所有都是基于开源的内核。

OKL4 Microkernel

与高通合作开发的工作量变得太多了而无法在研究机构内部完成。事实上，税务局开始威胁NICTA的免税地位！此外，我们看到商业机会需要承担经营风险，这是你不能用纳税人的钱去做的。这就是为什么我们决定将相关的业务分拆出去成立OK
Labs公司。 OK Labs公司以“OKL4微内核”名义下销售L4，并继续发展成为一个商业级的平台。

OK Labs公司最初做为一个服务企业运营，服务于高通，同时也有其他的客户。需要注意的是，OK Labs甚至不需要NICTA的授权去做到这一点，因为它采取了一个开放源码的发布和技术支持。任何人都可以这样做了（不过，当然，谁先创造了该技术也最适合这么做）。这些都意味着，从来就没有涉及到NICTA版税的任何问题。

另外，需要注意的是如果L4不是开源的话，高通几乎肯定不会采用，这是很重要的。他们的风格是在内部自己弄一套，重新实现L4将是他们自然的方法。我们的承诺对他们来说是不寻常的，却使得NICTA的技术被部署在超过15亿的台设备上。

OKL4 Microvisor

OK Labs公司后来决定要成为一家产品公司，并寻求风险投资来实现这个目标。他们开发了自己的产品，OKL4 Microvisor。这是OKL4微内核的下一代，并是在OK
Labs公司从无到有开发出来的，NICTA（或其他人）对它没有所有权。它是（并且提供）在特许的基础上授权的，而这正是你期望一个产品公司做的。

seL4

然后就是第三个微内核了，seL4。这是由NICTA从头开始开发的，它的实现在数学上被证明是规范正确的。

正确性的证明是世界各地的头条大新闻事件。它是真正突破性的，但主要是作为一项科学成果：自上世纪70年代一些人曾试图证明但都没有成功。但是，按我的原子弹的比喻，一旦人们知道这是可能的，他们可以弄清楚自己如何去做。特别是自我们公布了该方法的基本知识之后（毕竟，做研究是NICTA的首要工作，如果不公布就不是研究了）。而且seL4的开发（和所有验证其可行的开发）花了25人一年的时间。这来自很长一段时间内澳大利亚最大的ICT研究的努力。公平地说，这已经使NICTA登上了国际舞台。

seL4的商业化

seL4可以变成一个令人兴奋的产品，但需要进一步的工作。这不是你在实验室做一些事情，这是公司的业务。这就是为什么NICTA需要一个商业化的渠道。

他们决定做的方式是专门授权seL4给OK Labs公司，在达到某些里程碑时有买断的选项（即获取IP买断的选项）。作为交换，NICTA获取了OK
Labs公司的股权，以此来作为商业化成功的回报。通过OK Labs公司做为商业化的加速是一个显而易见的选择：首先，OK Labs公司开发市场和销售这种技术。其次，OK
Labs公司在澳大利亚执行其所有工程，其他任何替代的企业都在海外。这是一个合理的交易。