For faster navigation, this Iframe is preloading the Wikiwand page for L4微内核系列.

L4微内核系列

本条目存在以下问题,请协助改善本条目或在讨论页针对议题发表看法。 此条目翻译品质不佳。 (2018年4月20日)翻译者可能不熟悉中文或原文语言,也可能使用了机器翻译。请协助翻译本条目或重新编写,并注意避免翻译腔的问题。明显拙劣的翻译请改挂((d|G13))提交删除。 此条目需要补充更多来源。 (2017年5月8日)请协助补充多方面可靠来源改善这篇条目无法查证的内容可能会因为异议提出而被移除。致使用者:请搜索一下条目的标题(来源搜索:"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/MIPSL4/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]

参见

[编辑]

来源

[编辑]
  1. ^ http://l4ka.org/projects/pistachio/. [2006-04-16]. (原始内容存档于2006-04-21).  外部链接存在于|title= (帮助)
  2. ^ http://www.gnu.org/software/hurd/hurd-l4.html. [2006-04-16]. (原始内容存档于2010-12-23).  外部链接存在于|title= (帮助)
  3. ^ 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). 
  4. ^ 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. 

外部链接

[编辑]
{{bottomLinkPreText}} {{bottomLinkText}}
L4微内核系列
Listen to this article

This browser is not supported by Wikiwand :(
Wikiwand requires a browser with modern capabilities in order to provide you with the best reading experience.
Please download and use one of the following browsers:

This article was just edited, click to reload
This article has been deleted on Wikipedia (Why?)

Back to homepage

Please click Add in the dialog above
Please click Allow in the top-left corner,
then click Install Now in the dialog
Please click Open in the download dialog,
then click Install
Please click the "Downloads" icon in the Safari toolbar, open the first download in the list,
then click Install
{{::$root.activation.text}}

Install Wikiwand

Install on Chrome Install on Firefox
Don't forget to rate us

Tell your friends about Wikiwand!

Gmail Facebook Twitter Link

Enjoying Wikiwand?

Tell your friends and spread the love:
Share on Gmail Share on Facebook Share on Twitter Share on Buffer

Our magic isn't perfect

You can help our automatic cover photo selection by reporting an unsuitable photo.

This photo is visually disturbing This photo is not a good choice

Thank you for helping!


Your input will affect cover photo selection, along with input from other users.

X

Get ready for Wikiwand 2.0 🎉! the new version arrives on September 1st! Don't want to wait?