本條目存在以下問題 ，請協助
改善本條目 或在
討論頁 針對議題發表看法。
此條目需要补充更多来源 。(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 被证明是一个安全的操作系统 内核。
回顾历史，大多数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]
2009年，Data61/CSIRO实现了对于其L4内核的形式化证明，并创造出世界上第一个此类的实用操作系统seL4[3] [4]
參見 编辑 来源 编辑 ^ . [2006-04-16 ] . （原始内容存档于2006-04-21）. ^ http://www.gnu.org/software/hurd/hurd-l4.html. [2006-04-16 ] . （原始内容于2010-12-23）. ^ 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. 外部链接 编辑 – 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-嵌入式内核 – Linux 移植到上L4/ 操作系统 L4Linux （页面存档备份，存于互联网档案馆 ） – Linux 在L4的微内核上运行 DROPS （页面存档备份，存于互联网档案馆 ） – The Dresden 实时操作系统项目 GNU Hurd/L4（页面存档备份，存于互联网档案馆 ） – 移植 GNU Hurd/Mach 到 L4 上 L3的信息 （页面存档备份，存于互联网档案馆 ），L4的前身 seL4 （页面存档备份，存于互联网档案馆 ），第一个完成全内核形式化证明的实用操作系统
l4微内核系列, 本條目存在以下問題, 請協助改善本條目或在討論頁針對議題發表看法, 此條目翻譯品質不佳, 2018年4月20日, 翻譯者可能不熟悉中文或原文語言, 也可能使用了機器翻譯, 請協助翻譯本條目或重新編寫, 并注意避免翻译腔的问题, 明顯拙劣的翻譯請改掛, href, template, html, class, redirect, title, template, href, wikipedia, html, class, redirect, title, wikipedia, 提交刪除, 此條目需要. 本條目存在以下問題 請協助改善本條目或在討論頁針對議題發表看法 此條目翻譯品質不佳 2018年4月20日 翻譯者可能不熟悉中文或原文語言 也可能使用了機器翻譯 請協助翻譯本條目或重新編寫 并注意避免翻译腔的问题 明顯拙劣的翻譯請改掛 a href Template D html class mw redirect title Template D d a a href Wikipedia CSD html G13 class mw redirect title Wikipedia CSD G13 a 提交刪除 此條目需要补充更多来源 2017年5月8日 请协助補充多方面可靠来源以改善这篇条目 无法查证的内容可能會因為异议提出而被移除 致使用者 请搜索一下条目的标题 来源搜索 L4微内核系列 网页 新闻 书籍 学术 图像 以检查网络上是否存在该主题的更多可靠来源 判定指引 此條目需要編修 以確保文法 用詞 语气 格式 標點等使用恰当 請按照校對指引 幫助编辑這個條目 幫助 討論 L4是一種微内核构架的作業系統内核 最初由約亨 李德克 Jochen Liedtke 设计 前身為L3微內核 在最开始 L4只是一个由約亨 李德克设计并实现的单一的产品 用于Intel i386上的一个高度优化内核 L4微内核系统由于其出色的性能和很小的体积而开始被计算机工业所认知 随后 L4的系统在多个方面上有了高速的发展 值得提及的是一个更加独立于硬件平台的版本 被称为Pistachio 1 之后又被移植到了许多不同的硬件构架上 现在已经形成一个微内核家族 包括Pistachio L4 MIPS 与Fiasco 目录 1 歷史 2 当前开发情况 3 參見 4 来源 5 外部链接歷史 编辑由于意识到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的时间 通过在TUV SUD中使用多年 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 页面存档备份 存于互联网档案馆 第一个完成全内核形式化证明的实用操作系统 取自 https zh wikipedia org w index php title L4微内核系列 amp oldid 68789157, 维基百科，wiki ，书籍，书籍，图书馆，
文章 ，阅读，下载，免费，免费下载，mp3，视频，mp4，3gp， jpg，jpeg，gif，png，图片，音乐，歌曲，电影，书籍，游戏，游戏。