Can you summarize the following document?
        
  由於意識到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被證明是一個安全的作業系統核心。<br> 在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). 當前存在一個目標為致力於在L4框架下最小的實現Mach的設計,開發者們正在它的實現上工作。  2009年,Data61/CSIRO實現了對於其L4核心的形式化證明,並創造出世界上第一個此類的實用作業系統seL4。他們在2013年進一步證明了核心的資訊流安全性,使得該系統成為最安全的作業系統之一。
L4是一種微核心構架的作業系統核心,最初由約亨·李德克(Jochen Liedtke)設計,前身為L3微核心。在最開始,L4只是一個由約亨·李德克設計並實現的單一的產品,用於Intel i386上的一個高度優化核心。L4微核心系統由於其出色的效能和很小的體積而開始被計算機工業所認知。隨後,L4的系統在多個方面上有了高速的發展,值得提及的是一個更加獨立於硬體平臺的版本,被稱為Pistachio,之後又被移植到了許多不同的硬體構架上。現在已經形成一個微核心家族,包括Pistachio,L4/MIPS,與Fiasco。