Micronucleus L4

Az L4 egy második generációs mikronukleus , amelyet Jochen Liedtke  (en) tervezett . Mivel az 1990-es évek eleje mikromagjai rendkívül lassúak voltak monolitikus versenytársaikhoz képest , Liedtke úgy döntött, hogy saját mikrotagokat fejleszt ki. Így fejleszti az L3, majd az L4 mikrotagokat. Az ezek és utódaik számos fejlesztése azóta lehetővé tette ezen régi magok sebességének jelentős növelését, majd a jelenlegi mikrotagok elérését.

Az L4 általános gondolatát tehát maga Liedtke foglalja össze: „egy koncepció csak akkor tolerálható a mikrotag belsejében, ha annak a magon kívüli elmozdulása, vagyis alternatív megvalósítások engedélyezése megakadályozná a megvalósítást. a rendszer. "

Motivációk

A mikrokernelek minimalizálják a kernel által biztosított funkcionalitást: a kern általános mechanizmusokat kínál, míg a felhasználói módú kiszolgálók az operációs rendszer szolgáltatásait valósítják meg. A monolit kernellel rendelkező operációs rendszerek és a mikrokerneles operációs rendszerek eltérő típusú művelettel rendelkeznek, így két különböző operációs rendszer lesz belőlük . A monolit kernelen alapuló operációs rendszerek nagyobb hangsúlyt fektetnek a nagy teljesítményre, míg a mikrokernek nagyobb hangsúlyt fektetnek a biztonságra és a stabilitásra. A korai mikrotag-alapú operációs rendszerek azonban lassúak voltak, így hatékonyságuk nem volt olyan magas.

Jochen Liedtke a minimalista kerneken alapuló operációs rendszerek teljesítményének javítása céljából kezdte el fejleszteni az L3 , majd az L4 kerneleket . Ezeknek a kerneleknek az alapelve egyszerűen a következő: "egy koncepció csak akkor engedélyezett a kernelben, ha az nem valósítható meg a felhasználói térben" . Ez a fajta kern tehát kizárólag azokat az alapvető funkciókat látja el, mint a kommunikáció, a térképezés  stb. Politikákat is előír. A mikrokernel nem végez valódi munkát (a mikrokernel csak az a feladata van, hogy ellenőrizze és kezelje azokat a feladatokat, amelyeket a felhasználói térben folyamatokra delegál).

Történelem

Húsz évvel ezelőtt Jochen Liedtke az L4-es kerneljével bebizonyította, hogy a folyamatok közötti mikrotagok kommunikációja 10-20-szor gyorsabb lehet, mint amire akkor számítani lehetett. Az L4-et egy korábbi L3 nevű verzióból tervezték, és John Liedtke fejlesztette ki az 1980-as évek elején i386 platformokon. Kereskedelemben több ezer létesítményen telepítették (főleg iskolákban). Mint az akkori összes mikrotag, az L3 is szenvedett a processzek közötti kommunikáció 100 mikrosekundum nagyságrendű költségeitől .

Liedtke kezdetben az L3-at használta új ötletek kísérletezésére. Ez először használta az "L4" nevet, az ABI  v2 pedig már 1995 óta jelen van a közösségben . Ezt követően teljesen átírják az i486 számítógépek összeszerelésében , és gyorsan portolták a Pentiumokhoz.

Ez a kezdeti munka egy 20 éves fejlődést váltott ki, amelyet az ABI-k többszöri felülvizsgálata , valamint új megvalósítás követett . Ez kezdődött a újraírását ABI Dresden és UNSW a 64 bit az Alpha és MIPS processzorok , miután az utóbbi integrált lassabb műveleteket C nyelven . Ez a két kern tehát képes volt egy mikroszekundumnál rövidebb folyamatközi kommunikációt elérni, amit megkönnyített az a tény, hogy nyílt forráskódú kernek voltak . Az UNSW Alpha kernel volt az első többprocesszoros L4 kernel.

Liedtke, aki a GMD-t az IBM Watson számára hagyta el , egy BIT megvalósításakor szerezte tapasztalatait, amelyet az eredmény X-verzióként fog tudni . A GMD és az IBM nagyon korlátozó szellemi tulajdonjogi politikát vezetett be más kutatókkal szemben, ami arra késztette a „ drezdai  ” projektet  , hogy a semmiből induljon egy új, „Fiasco” nevű változat bevezetésével, utalva rossz tapasztalataikra, és megpróbálva jobban kezelni a szellemi tulajdon kérdését.

A "Fiasco" az L4 kernel első verziója, amelyet teljesen magas szintű nyelven ( C ++ ) írtak, és az L4 kernelek alapkódjának legrégebbi változata továbbra is aktívan karbantartott. Ez volt az első jelentős módon forgalomba hozott L4 mag (becslés szerint: több mint 100 000 eladás).

Amikor Liedtke megérkezett a németországi Karlsruhe-ba , tanítványával A C-ben írt új verzióban " Mogyoró  " néven adaptálták  , ez volt az első L4-es kernel , amelyet más architektúráknak hordoztak ( Pentium  I- től ARM-ig ).

Karlsruhe az ABI X verzióval és az L4Ka :: Hazelnut tapasztalataival az ABI  V4 jelentős átalakításához vezetett a kernel hordozhatóságának javítása érdekében. Liedtke 2001- es halála után tanítványai új ingyenes kernelt hajtottak végre  : az L4Ka :: Pisztáciát az L4Ka-val . C ++ nyelven írták, és először az x86 és a PowerPC , majd az UNSW / NICTA , majd nem sokkal később a MIPS , az Alpha , a  64 bites PowerPC és az ARM portokra helyezték .

A NICTA  (in) -ben azonnal átcsoportosították telepítésüket a beágyazott rendszerek korlátozott erőforrásaiban való használatra . Ennek eredményeként született meg a kernel új verziója a "Pisztácia" kód másolatából, amelyet NICTA :: Pisztácia-beágyazottnak ("L4-beágyazott") hívtak . Nagy tömegben került forgalomba, amikor a Qualcomm úgy döntött, hogy operációs rendszerként használja vezeték nélküli modemjeinek firmware- jében. A NICTA Open Kernel Labs  (en) leányvállalata az OKL4  névre keresztelt kern támogatása és fejlesztése lett   . Telepítettek egy másik verziót, a PikeOS-t , a SYSGO  által forgalmazott klónot (in) , amelyet tanúsítottak az űrhajózás kritikus rendszereiben, valamint repülőgépekben és vonatokban történő használatra.

Néhány alapfogalom

Az L4 fő gondolata, hogy javítsa a mikrotagok sebességét, különös tekintettel a folyamatok közötti kommunikációra, miközben megtartja a mikrotagok fogalmait, egyes fogalmakat át kellett állítani, másokat bevezetni. Az alábbiakban bemutatjuk azokat a koncepciókat, amelyek lehetővé tették Liedtke számára, hogy megfeleljen a kihívásának.

Minimális

Az L4 mikrotagok egy egyszerű API-t, minimumot és absztrakciót biztosítanak, amelyek támogatják a szálak közötti létrehozást, végrehajtást és folyamatok közötti kommunikációt (IPC), valamint lehetővé teszik a különböző feladatok elkülönítését és kezelését .

A Liedtke fő tervezői a minimalizmusra és a folyamatok közötti kommunikáció teljesítményére összpontosítottak, szilárd meggyőződéssel az L3 gyengeségeinek javításában. A mikrotag minimális elvét a következőképpen fogalmazta meg: „A koncepciót csak akkor fogadják el a mikronukleuszban, ha a magon kívüli mozgás megakadályozná a rendszer által megkövetelt funkcionalitás megvalósítását. "

Ez az elv volt az alapja az L4 magok tervezésének. Kevin Elphinstone és Gernot Heiser szerint azonban egyetlen mikronukleusz-tervező sem állíthatja, hogy tiszta mikronukleust hozott létre, szigorúan betartva a minimalitás elvét. Bizonyításként mindannyiuknak van egy ütemezője a kernelben, amely egy adott ütemezési házirendet hajt végre. Abban az időben úgy gondolták, hogy senki sem tervezhet olyan mikrorakót, amelyben minden tervezési politika a felhasználói térre hárulna, hatalmas költségek nélkül.

Címterek

Hardver szinten a címtér egy olyan leképezés, amely minden virtuális oldalt egy fizikai oldalhoz társít , vagy másként "nem hozzáférhetőként" jelöl. A leképezést a TLB és az oldaltábla hajtja végre .

A memóriakezelő egység biztosítja a térbeli elkülönítést. Minden olyan adatot tartalmaz, amely egy szálon keresztül közvetlenül elérhető . Az L4 címtere rekurzívan szerkeszthető. Egy szál leképezheti a címterének közös részeit egy másik szálra, és így megoszthatja az adatokat a memóriaterületének ezen részeiről.

A feladat fogalma egyenértékű a címtérével. Az L4- ben a feladat szálak halmaza, amely megosztja a címteret.

Szálak és IPC

A processzek közötti üzenetküldés az egyik paradigma, amelyet a mikrotagok és más kliens-szerver alkalmazások használnak . Segít javítani a modularitást, a rugalmasságot, a biztonságot és a méretezhetőséget .

A különböző címtartományú szálak közötti kommunikációhoz a klasszikus módszer abból áll, hogy a szálak között üzeneteket továbbítanak a kernelen keresztül. Az IPC mindig magában foglal valamilyen megállapodást a két fél között: a feladó úgy dönt, hogy információt küld, és meghatározza annak tartalmát, míg a címzett meghatározza, hogy hajlandó-e információt fogadni és szabadon értelmezheti-e az üzenet tartalmát.

Liedtke szerint „sokkal fontosabb a folyamatok közötti kommunikáció teljesítménye” . Kétféle IPC létezik  : szinkron és aszinkron IPC. Az első generációs mikromagok aszinkron IPC-ket (pl. Mach ) használtak. A kern puffermemóriában tartja az üzenetet, amíg a vevő készen áll az üzenet fogadására; ez az üzenet dupla másolatát eredményezi, és ez késztette Machet sok teljesítmény elvesztésére. A második generációs mikrotagok (például az L4) szinkron IPC-ket fogadtak el a szálak közötti kommunikációhoz . Ezekben a kommunikációkban az első kommunikátor megvárja, amíg a másik készen áll: az üzenetet aztán közvetlenül át lehet másolni e szálak közé , elkerülve a felesleges ideiglenes másolást a kernelben. A szinkron IPC-k tehát kielégítik a hatékony és szükséges megvalósítást.

Megszakítások

A megszakítások természetes absztrakciója a folyamatok közötti kommunikáció . Hardver minősül gyűjteménye szálak , amelyek különleges azonosítókat és üzeneteket küldeni, amely csak a küldő azonosítója a szoftver szálak velük kapcsolatban. A fogadó szál ellenőrzi az üzenetküldő azonosítóját, és ha az üzenet hardveres megszakítás, akkor azt azonnal megszakítja. A megszakítás üzenetgé történő átalakítását a kernel végzi, de a kernel nem vesz részt a megszakítás feldolgozásában. A valóságban a kernel teljesen figyelmen kívül hagyja a megszakításkezelés szemantikáját.

Pilóták a felhasználói térben

Az eszközillesztő olyan folyamat, amely közvetlen hozzáféréssel rendelkezik a közvetlenül a címterébe leképezett I / O portokhoz, és üzeneteket (megszakításokat) fogad a hardvertől a szokásos IPC mechanizmusokon keresztül. Az L4 mikrotagok filozófiájában soha nem szabad őket integrálni a mikrotagba. A bejövő megszakítások üzenetekké alakulnak a kapcsolódó szálakká . Ez az eszközmeghajtók felhasználói térkiszolgálóként történő megvalósításának alapja.

L4 micronucleus család

Mivel Liedtke fejlődése L4 több implementáció követte többek kudarc , L4Ka :: Pisztácia , P4 , L4 PowerPC , L4Ka :: mogyoró , L4 / MIPS , L4 / Alpha , L4 / x86 ,  stb

Kudarc

Kudarc fejlesztette ki a fiaskó csapat a Drezdai Műszaki Egyetem 1999-ben , és a kezdeményező a cseppek ( Dresden Real-Time Operating System Project ) rendszer. Gyakran mondjuk, hogy "L4 / Fiasco", hogy Fiascóról beszéljünk , ami kiemeli az L4-hez fűződő viszonyát .

A mikrokernel biztosítja a nélkülözhetetlen mechanizmusokat, de nem érvényesíti azokat a házirendeket, amelyeket többnyire a felhasználói térben hajtanak végre . Az L4 / Fiasco rendszerben van egy L4 környezet ( L4Env ), amely programozási környezet az alkalmazások számára, amelyeknek egy L4 / Fiasco kernel tetején kell futniuk .

Az „L4 / Fiasco” programozási modell kliens-szerver architektúrán alapszik . Az ütemező megelőző jellegű, alacsony prioritással és rotációs típusú ütemezéssel az azonos tulajdonossal rendelkező feladatok között .

L4Ka :: Pisztácia

Pisztácia fejlesztette ki a System Architecture Group csapata a Karlsruhe Technológiai Intézet (Németország) együttműködve a DiSy csoport a University of New South Wales (Ausztrália). A terjesztése a BSD licenc alatt történik .

A következő architektúrákra portolták: Alpha (21164 és 21264), AMD64 ( Opteron 242 , Simics ), ARM (SA1100, XScale, ARM925T), IA32 (Pentium és kompatibilis), IA-64 (Itanium1, Itanium2, Ski), 64 bites MIPS ( R4000 , R5000  (en) ),  32 bites PowerPC ( IBM 750 ) és 64 bites ( POWER3 , POWER4 ). Támogatja a többprocesszoros rendszereket.

A legújabb verzió, az X.2, 2008 - ban jelent meg 2009. május.

seL4

A seL4 micronucleus az L4 micronucleus család tagja, amelyet úgy terveztek, hogy erős biztonsági mechanizmusokat biztosítson, miközben megtartja az L4 családban megszokott és a tényleges felhasználás szempontjából elengedhetetlennek tartott magas teljesítményt . Ez egy harmadik generációs mikronukleusz, amely teljes egészében egy L4 típusú magra épül . Az utóbbihoz hasonlóan az absztrakciókat használja virtuális címterekhez, szálakhoz , folyamatok közötti kommunikációhoz….

A virtuális címtereket az alapvető objektumok kifejezett manipulálásával alakítják ki: oldal elérési útja, oldal táblája  stb. Nincs meghatározott alapstruktúrájuk (eltekintve azoktól, amelyeket magának a seL4 kernelnek tartanak fenn).

A szálak SEL4 aktív entitások . A Kérdéses csomópont  és a virtuális címtér szálhoz társításával a felhasználó által kezelt házirendek magas szintű absztrakciót hoznak létre, mint például folyamatok vagy virtuális gépek .

A folyamatok közötti kommunikációt  kétféleképpen támogatják: szinkron üzenetek használatával paraméterek (port, tehát rendeltetési hely, a pufferelés használata nélkül a kernelben) továbbításával és aszinkron értesítésekkel aszinkron paramétereken keresztül (objektum- kinevezések csak egy szóból állnak a kernelben ).

Az eszközillesztőket olyan felhasználói módú alkalmazásokként futtatják, amelyek hozzáférnek az eszközregiszterekhez és a memóriához, akár az eszköz leképezésével a folyamat virtuális címterébe, akár az eszközhöz való hozzáférés vezérlésével (azaz különösen az x86-os architektúrák esetében) ). A "  Sel4  " biztosítja a megszakítási értesítések (aszinkron IPC-k útján) fogadásának és a nyugtázások kezelésének mechanizmusait.

A Nuclei SEL4 az ARM  és az x86 processzorokon dolgozik , de a SEL4 jelenleg létező tanúsított verziói az ARMv6  (in)  és az ARMv7 verziókra vonatkoznak . Az x86 platformokra  való hordozást jelenleg  nem támogatják hivatalosan , De még mindig létezik a seL4 x86 kísérleti többmagos verziója .

L4-et használó projektek

• (en + de) "  DROPS - Drezdai valós idejű operációs rendszer projekt  " , http://os.inf.tu-dresden.de ,2013(hozzáférés: 2013 ) .
• L 4 Linux  (in) , a rendszermag portolja a Linuxot az L4Ka-ba és a Fiasco-ba .
• A GNU Hurd kikötője az L4Ka számára :: Pisztácia  : A projekt célja annak a mikrokernelnek a cseréje, amelyen a GNU Hurd fut . 2014 -ben a  Mach GNU verzióját futtatta , és még mindig kísérleti stádiumban volt.

Megjegyzések és hivatkozások

1. (in) Jochen Liedtke (1995 decemberében). “  On µ -Kernel Construction  ” (pdf) Proc. 15. ACM Symposium on Operating Systems Principles (SOSP) : 237–250 p. Hozzáférés: 2017. szeptember 28. 
2. Kevi Elphinstone, Gernot Heiser 2013 , p.  133.
3. Qingguo ZHOU, Canyu LI, Ying DING, Ganghui CHENG, Hu BIN 1996 , p.  133.
4. kevin Elphinstone, Gernot Heiser 2013 , p.  133.
5. kevin Elphinstone, Gernot Heiser 2013 , p.  134.
6. Lucyantie Mazalan, Raja Mariam Ruzila, Raja Ahmed Sufian, Ahmad Kamal Abdul Aziz, Mohd Saufy Rohmad, D r  Jamalul-lail Ab. Manan 2008 , p.  1.
7. Kevin Elphinstone, Gernot Heiser 2013 , p.  136.
8. Jochen Liedtke 1995 , p.  238.
9. Qingguo ZHOU, Canyu LI, Ying DING, Ganghui CHENG, Hu BIN, Nicholas McGuire 2009 , p.  134.
10. Jochen Liedtke 1993 , p.  175.
11. Jochen Liedtke 1995 , p.  239.
12. Jochen Liedtke 1995 , p.  240.
13. Dong-Guen Kim, Sang-Min Lee, Dong-Ryeol Shim 2008 , p.  307.
14. Qingguo ZHOU, Canyu LI, Ying DING, Ganghui CHENG, Hu BIN, Nicholas McGuire 2009 , p.  133.
15. Qingguo ZHOU, Canyu LI, Ying DING, Ganghui CHENG, Hu BIN, Nicholas McGuire 2009 , p.  135.
16. (in) '  L4Ka projekt hivatalos weboldala  " az l4ka.org oldalon ,2013. július 12(megtekintve 2017. szeptember 28-án ) .
17. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, Tobby Murray, Dhammika Elkaduwe, Kolanski Rafal, Thomas Sewell , p.  1.
18. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, Tobby Murray, Dhammika Elkaduwe, Kolanski Rafal, Thomas Sewell , p.  4.
19. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, Tobby Murray, Dhammika Elkaduwe, Kolanski Rafal, Thomas Sewell , p.  2.
20. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, Tobby Murray, Dhammika Elkaduwe, Kolanski Rafal, Thomas Sewell , p.  5.

Bibliográfia

 : a cikk forrásaként használt dokumentum.

• (en) Qingguo Zhou , Canyu LI , Ying DING , Ganghui Cheng és Hu BIN , „  A budakalászi L4 Linux megvalósítása az oktatás  ” , IEEE Párhuzamosság , vol.  1,2009. augusztus, P.  137–140 ( ISBN  978-1-4244-3928-7 , DOI  10.1109 / ITIME.2009.5236446 ). 
• (en) kevin Elphinstone és Gernot Heiser : „Az  L3-tól a seL4-ig mit tanultunk az L4 mikrokernelek 20 éve alatt?  " , ACM ,2013. november, P.  133–150 ( ISBN  978-1-4503-2388-8 , DOI  10.1145 / 2517349.2522720 ). 
• (en) Qingguo Zhou , Canyu LI , Ying DING , Ganghui Cheng , Hu BIN és Nicholas McGuire , „  esettanulmány mikrokernel Oktatási  ” , IEEE Párhuzamosság , vol.  1,2009. augusztus, P.  133–136 ( ISBN  978-1-4244-3928-7 , DOI  10.1109 / ITIME.2009.5236445 ). 
• en) Hironao Takahashi , Kinji Mori és Hafiz Farooq Ahmad , „  L4 szintű gyorsítótárat használó hatékony I / O intenzív többbérlős SaaS rendszer  ” , IEEE Concurrency ,2010. június, P.  222–228 ( ISBN  978-1-4244-7327-4 , DOI  10.1109 / SOSE.2010.14 ).
• (en) Jochen Liedtke , „  Improving IPC by Kernel Design  ” , ACM , vol.  25,1993. december, P.  175–188 ( ISBN  0-89791-632-8 , DOI  10.1145 / 168619.168633 ). 
• (en) Tae-You Lee , Hyung-Rok Seo és Dong-Ryeol Shim : „  Hibák elkülönítése a hontalan szervermodell használatával az L4 mikrokernelben  ” , IEEE , vol.  2,2010. február, P.  518–522 ( ISBN  978-1-4244-5585-0 , DOI  10.1109 / ICCAE.2010.5451638 ).
• (en) Peter Druschel , Larry L. Peterson és Norman C. Hutchinson , „  Beyond Micro-Kernel Design: Decoupling Modularity and Protection in Lipto  ” , IEEE , vol.  2,1992. június, P.  512–520 ( ISBN  0-8186-2865-0 , DOI  10.1109 / ICDCS.1992.235002 ).
• (en) Jochen Liedtke , „  A mikrokernek felépítéséről  ” , ACM , vol.  29,1995. december, P.  237-250 ( ISBN  0-89791-715-4 , DOI  10,1145 / 224.056,224075 ). 
• (en) Ki-Seok Bang , Su-Young Lee , Ki-Hyuk Nam , Wan-Yeon Lee és Young-Woung Ko , „  Az L4 mikrokernel alapú mobiltelefon viselkedésének ellenőrzése  ” , IEEE , vol.  1,2007. február, P.  113–115 ( ISBN  978-89-5519-131-8 , DOI  10.1109 / ICACT.2007.358317 ).
• (en) Amaury Gauthier , Clément Mazin , Julien Iguchi-Cartigny és Jean-Louis Lanet , „  Fuzzing technika fejlesztése az OKL4 syscalls teszteléséhez  ” , IEEE , vol.  1,2011. augusztus, P.  728–733 ( ISBN  978-1-4577-0979-1 , DOI  10.1109 / ARES.2011.116 ).
• (en) S. Hessel , F. Bruns , A. Lackorzynski , H. Härtig és J. Hausner , „  Az L4 / Fiasco mikrokernel gyorsulása a Scratchpad memória használatával  ” , ACM ,2008. június, P.  6–10 ( ISBN  978-1-60558-328-0 , DOI  10.1145 / 1622103.1622106 ).
• (en) Dohun Kim , Jugwan Eom és Chanik Park , „  L4oprof: Teljesítményfigyelő egység alapú szoftverprofil keretrendszer az L4 mikrokernelhez  ” , ACM , vol.  41,2007. július, P.  69–76 ( ISSN  0163-5980 , DOI  10.1145 / 1278901.1278911 ).
• (en) Chen Tian , Daniel Waddington és Jilong Kuang , „  Skálázható fizikai memóriaallokációs rendszer az L4 mikrokernelhez  ” , IEEE ,2012. július, P.  488-493 ( ISBN  978-1-4673-1990-4 , DOI  10,1109 / COMPSAC.2012.85 ).
• en) Jianjun Shen , Sihan Qing és Qingni Shen , „  Mikrokern alapú biztonságos rendszerarchitektúra kialakítása  ” , IEEE ,2006. június, P.  384–385 ( ISBN  1-4244-0130-5 , DOI  10.1109 / IAW.2006.1652123 ).
• en) Dong-Guen Kim , Sang-Min Lee és Dong-Ryeol Shin , „  Az operációs rendszer virtualizációjának tervezése az L4 mikrokernelen  ” , IEEE ,2008. szeptember, P.  307–310 ( ISBN  978-0-7695-3322-3 , DOI  10.1109 / NCM.2008.165 ).
• (en) Lucyantie Mazalan , Raja Mariam Ruzila Raja Ahmed Sufian , Ahmad Kamal Abdul Aziz , Mohd Saufy Rohmad és D r  Jamalul-lail Ab. Manan , „  Tapasztalat az AES256 megvalósításáról az L4 mikrokernelen a DROPS (BID) környezet használatával  ” , IEEE , vol.  3,2008. augusztus, P.  1–5 ( ISBN  978-1-4244-2327-9 , DOI  10.1109 / ITSIM.2008.4632027 ). 
• (en) Gerwin Klein , Kevin Elphinstone , Gernot Heiser , June Andronick , Tobby Murray , Dhammika Elkaduwe , Kolanski Rafal és Thomas Sewell , „  OS Kernel átfogó formális ellenőrzése  ” , ACM Transactions on Computer Systems , vol.  32,2014 február, P.  1–70 ( ISSN  0734-2071 , DOI  10.1145 / 2560537 ). 

Külső linkek

• (de) „  Az L4 mikromagvak családja  ” .
• (en) Az L4Ka projekt helyszíne .