L4微内核系列
L4是一種微内核构架的作業系統内核,最初由約亨·李德克(Jochen Liedtke)设计,前身為L3微內核。在最开始,L4只是一个由約亨·李德克设计并实现的单一的产品,用于Intel i386上的一个高度优化内核。L4微内核系统由于其出色的性能和很小的体积而开始被计算机工业所认知。随后,L4的系统在多个方面上有了高速的发展,值得提及的是一个更加独立于硬件平台的版本,被称为Pistachio[1] ,之后又被移植到了许多不同的硬件构架上。现在已经形成一个微内核家族,包括Pistachio,L4/MIPS,与Fiasco。
歷史
[编辑]由于意识到Mach微内核在设计和性能上的缺陷,许多开发人员在90年代中期开始重新审视整个微内核的概念。Mach为了支持一些除了Unix环境以外并不是特别有用的概念,而在进程间通讯(IPC)中增加了大量的额外开销。IPC系统本身就是一个分布式开销的经典案例。在单用户系统中,比如说手机,许可和权限的检查就显得不是那么重要。虽然Mach宣称自己是一个微内核,但是看起来实际上它包含了远超过它所必需的东西。
約亨·李德克想要证明更薄的IPC层、对性能更关注并与硬件特性相关(和与平台无关相对)的设计,会更贴近现实世界中的性能改进。相对于Mach的复杂的IPC系统,他的L3仅简单的传递消息,而没有任何额外的开销。安全和权限被视为同其它用户空间所必需的服务器一样。L3也使用了各种硬件的特性来传递消息,让每个调用都最大化的利用硬件特性,像寄存器。相对而言,Mach则使用的是one-size-fits-all的通用机制,以牺牲性能为代价而获取可移植性。这些改变大量减少IPC中额外的开销。在同样的系统中,Mach需要114毫秒来发送即使是最短的消息,而L3可以用少于10毫秒的时间来发送同样的消息。一次系统调用的时间比Unix所花费的一半还少,而Mach执行同样的系统调用需要5倍于Unix的时间。通过在TÜV SÜD中使用多年,L3被证明是一个安全的操作系统内核。
在L3之后,約亨·李德克开始意识到其它的一些Mach的概念也存在同样的问题。这导致了更简单地L4的诞生,由于太简单了,随后L4被证明是具有高可移植性的。
回顾历史,大多数Mach的性能问题似乎只能以重新设计来解决。例如,在Mach微内核与宏内核的比较中的另一个主要的瓶颈是在一个真实的"服务器"集系统中内核无法知道怎样有效地进行分页内存。开发者们使用宏内核可以,并且已经投入了可观的时间以试图了解内核的内存使用的精确性质,然后调整他们的系统来利用这些优点。在微内核上开发者无法知道是什么组成系统,而且除了一些特例之外无法更近地监视内存使用。
Liedtke决定这个问题的解决方案是简单地从内核中移除全部分页工作,并允许每个应用程序应用以前只能应用于宏内核的调整形式。在L4系统下,操作系统(相对于内核)被期望提供分页服务,潜在地可以以很多种形式,允许开发者选取最适合于他们的工作的方式。内核的角色减少到知道这样的系统存在并提供一个支持它们的机制。在L4下,这总共需要三个函数:Grant,Map和Unmap。
结果设计哲学变成了最小化的。就像L4/MIPS的作者们所表述的:“一项特性当且仅当安全需要它在特权模式被实现时才应该在微内核里”。Mach关注于跨平台的可移植性,多处理器支持和其它“下一件大事”的主机。
一个基于L4的操作系统必须提供那些上一代宏内核内部所内置的服务。例如,为了实现一个类Unix的安全系统,服务器必须提供像Mach内核所内置的权限管理。进一步说,消息在多数情况下必须检查其有效性。但仍不清楚的是,在L4之上运行的真实的操作系统的端对端性能是否会显著快于一个基于Mach建立的系统。在一个移植到L4之上运行的Linux,和另一个移植到Mach之上运行的MkLinux,与基本的Linux系统本身之间的测试清楚地表明了L4的性能的优势。即使在最好的情况下MkLinux运行得比宏内核慢15%,而同时L4只慢大约5-10%。更进一步移植Linux系统的开发,而不是为测试而实现,有可能提高(性能)到一定程度。
当前开发情况
[编辑]Liedtke的L4原始版本是为速度而建立的。为了榨干每一滴性能,许多关键段落是以汇编语言写成的。他的工作在操作系统设计圈引起了一场小小的革命。很快它被一些大学所研究,然后很快是IBM,就是Liedtke所迁往的地方。在IBM一个L4的新版本被创造出来,Lemon Pip,紧接着是使用C++创造一个跨平台版本的努力,Lime Pip。
Karlsruhe大学也选择L4进行开发,在那里他们开发了L4Ka::Hazelnut,一个计划运行于所有32位机器上C++的版本。他们试图判断像C++这种高级语言的额外开销是否会抹杀掉其所提供的编程便利性。这份努力很成功,性能仍然是极好的,在它发布时IBM的Lime Pip项目终止了。Hazelnut最终为了可移植性、64位支持和更好的性能被全部重写,由此而产生了L4Ka::Pistachio。
新南威尔士大学也同样进行着开发,在那里开发者在多种64位平台上实现了L4。他们开发了L4/MIPS和L4/Alpha,而Liedtke的原始版本被追认为L4/x86。像Liedtke的最初的内核那样,UNSW内核是不可移植的并且是分别从头重写的。在高度可移植的Pistachio发行时,UNSW研究组放弃了他们自己的内核转而支持产生高度优化的Pistachio移植。
最近UNSW研究组在他们的新家National ICT Australia (NICTA),创造了一个新的L4版本称为L4-embedded。就像名称所暗示的那样,这是着眼于在商业嵌入式环境中的使用,因此这个实现在较小的内存印记与减少复杂度的目标之间的进行了权衡。还有正在进行中的如下工作,L4 API的正式化,正规的证明一个实现的正确性,以及为了在L4之上开发良好结构化的系统的框架。
Fiasco是对最初的L4的进一步的开发,包含了硬实时支持,并且被作为DROPS操作系统的基础。对于实时系统使用"快"是不够的,所以Fiasco内核是完全重入的,允许在任何时间被中断。就像其它由最初的L4的发展出来的版本一样,为了可读性和可移植性的原因,Fiasco也是使用C++写成的。
今天几乎所有的开发者出现在Pistachio内核上。新南威尔士大学现在使用Pistachio继续他们的可移植性实验,并且Pistachio内核现在在广泛的硬件上都有提供。其它的研究组在探索实时支持,对像Fiasco那样的概念继续深入研究。基本内核的开发也在Karlsruhe大学继续,朝向新的"Version 4" API而工作(Pistachio 当前只实现了beta版).
GNU Hurd项目在考虑采用L4微内核以取代Mach (GNU Hurd/L4).[2] 当前存在一个目标为致力于在L4框架下最小的实现Mach的设计,开发者们正在它的实现上工作。
2009年,Data61/CSIRO实现了对于其L4内核的形式化证明,并创造出世界上第一个此类的实用操作系统seL4[3]。他们在2013年进一步证明了内核的信息流安全性,使得该系统成为最安全的操作系统之一[4]。
參見
[编辑]- Haiku – 开源桌面操作系统
- FreeRTOS – 微内核,实时操作系统(RTOS)
- Redox - Rust实现的微内核操作系统
- QNX – 符合POSIX,微内核实时操作系统(RTOS)
- INTEGRITY – 微内核实时操作系统(RTOS)
- 貝爾實驗室九號計畫 – 为了接替UNIX的分布式操作系统
- MINIX 3 – 类Unix微内核操作系统
来源
[编辑]- ^ http://l4ka.org/projects/pistachio/. [2006-04-16]. (原始内容存档于2006-04-21). 外部链接存在于
|title=
(帮助) - ^ http://www.gnu.org/software/hurd/hurd-l4.html. [2006-04-16]. (原始内容存档于2010-12-23). 外部链接存在于
|title=
(帮助) - ^ Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch , Simon Winwood. seL4: Formal Verification of an OS Kernel (PDF). 2009 ACM SIGOPS Symposium on Operating Systems Principles. [2018-09-14]. (原始内容存档 (PDF)于2018-04-12).
- ^ Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein. seL4: from General Purpose to a Proof of Information Flow Enforcement. 2013 IEEE Symposium on Security and Privacy.
外部链接
[编辑]- L4Hq – L4 总部,L4项目的社区站点。
- The L4 microkernel family (页面存档备份,存于互联网档案馆) – L4实现的简介、文档和项目
- L4Ka(页面存档备份,存于互联网档案馆) – L4Ka::Pistachio 和 L4Ka::Hazelnut 的实现
- The Performance of µ-Kernel-Based Systems (页面存档备份,存于互联网档案馆) – 一个出色的关于微内核和单一内核的性能分析比较,比较了Linux单内核情况,还有Linux运行在Mach3上和L4上。本文中的很多数据都取自这个来源。
- Fiasco (页面存档备份,存于互联网档案馆) – 一个自由的C++实现x86 和 ARM 处理器。
- UNSW (页面存档备份,存于互联网档案馆) – DEC Alpha 和 MIPS architecture 的实现
- NICTA(页面存档备份,存于互联网档案馆) – 移植到 ARM,MIPS,Alpha,PowerPC-64 and L4-嵌入式内核
- Wombat – Linux移植到上L4/Iguana 操作系统
- L4Linux (页面存档备份,存于互联网档案馆) – Linux 在L4的微内核上运行
- DROPS (页面存档备份,存于互联网档案馆) – The Dresden 实时操作系统项目
- GNU Hurd/L4(页面存档备份,存于互联网档案馆) – 移植 GNU Hurd/Mach 到 L4 上
- L3的信息 (页面存档备份,存于互联网档案馆),L4的前身
- seL4 (页面存档备份,存于互联网档案馆),第一个完成全内核形式化证明的实用操作系统