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 （頁面存檔備份，存於網際網路檔案館），第一個完成全核心形式化證明的實用作業系統