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]。
參見
來源
- ^ 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 （頁面存檔備份，存於網際網路檔案館），第一個完成全內核形式化證明的實用操作系統