L4 (microkernel)

L4
Tip de microkernel
Autor Jochen Liedtke
Dezvoltator Jochen Liedtke
Scris in limbaj de asamblare
Site-ul web l4hq.org

L4  este un microkernel de a doua generație dezvoltat de Jochen Liedtke în 1993 [1] .

Arhitectura microkernel-ului L4 sa dovedit a fi de succes. Au fost create multe implementări ale microkernel-ului L4 ABI și API . Toate implementările au devenit cunoscute ca familia L4 de microkernel-uri. Implementarea lui Liedtke a fost denumită informal „L4/x86” [2] .

Istorie

L1

În 1977, Jochen Liedtke și-a susținut proiectul de diplomă în matematică la Universitatea din Bielefeld (Germania). Ca parte a proiectului, Liedtke a scris un compilator pentru limbajul ELAN ( ing. ). Limbajul ELAN a fost creat în 1974 pe baza limbajului Algol 68 pentru predarea programarii [3] . Liedtke și-a numit lucrarea „L1”: litera „L” este prima literă a numelui de familie al autorului ( L iedtke ); numărul „1” este numărul de serie al lucrării.

L2

În 1977, Liedtke a absolvit ca matematician, a rămas la Universitatea din Bielefeld și a început să creeze un mediu de rulare pentru limbajul ELAN.

Microcontrolerele pe 8 biți au devenit disponibile pe scară largă. Era necesar un sistem de operare care să poată rula pe stații de lucru mici din licee și universități. CP/M nu se potrivea. Centrul Național de Cercetare pentru Informatică și Tehnologie din Germania GMD și Universitatea din Bielefeld au decis să dezvolte de la zero un nou sistem de operare [4] .

În 1979, Jochen Liedtke a început să dezvolte un nou sistem de operare și l-a numit „ Eumel ” ( în engleză ) din engleză.  microprocesor extensibil multi user m EL AN - system . Sistemul de operare „Eumel” a fost numit și „L2”, adică „ a doua lucrare a lui L iedtke ”. Noul sistem de operare a suportat procesoare Zilog Z80 pe 8 biți , a fost multi-utilizator și multitasking a fost construit pe un microkernel a suportat persistența ortogonală Suportul pentru persistența ortogonală a fost după cum urmează: sistemul de operare și-a salvat periodic starea pe disc (conținutul memoriei , registrele procesorului etc.); după întreruperi de curent, sistemul de operare a fost restabilit dintr-o stare salvată; programele au continuat să funcționeze ca și cum eșecul nu ar fi avut loc; s-au pierdut doar modificările efectuate de la ultima salvare. Eumel OS a fost inspirat de Multics OS și a împărtășit multe asemănări cu kernel -urile Accent și Mach 4

Sistemul de operare Eumel a fost ulterior portat pe procesoarele Zilog Z8000 , Motorola 68000 și Intel 8086 . Aceste procesoare erau pe 8 și 16 biți, nu conțineau un MMU și nu suportau un mecanism de protecție a memoriei . Eumel OS a emulat o mașină virtuală cu adresare pe 32 de biți și un MMU [4] . În ciuda utilizării emulării, până la cinci terminale ar putea fi conectate la o stație de lucru care rulează Eumel OS [4] .

La început, a fost posibil să scrieți programe pentru sistemul de operare Eumel doar în limbajul ELAN. Compilatoare pentru CDLPascal Basic și DYNAMO au fost adăugate mai târziu dar nu au fost utilizate pe scară largă 4

Din 1980, a început utilizarea Eumel OS, mai întâi pentru predarea programării și procesării de text, iar apoi în scopuri comerciale. Așadar, la mijlocul anilor 1980, sistemul de operare Eumel rula deja pe peste 2000 de computere din casele de avocatură și alte firme [4] .

L3

Odată cu apariția procesoarelor care suportă memoria virtuală (datorită MMU-ului) și a mecanismelor de protecție a acesteia, nevoia de a emula o mașină virtuală a dispărut.

În 1984 [5] Jochen Liedtke a plecat să lucreze la centrul de cercetare GMD pentru a crea un sistem de operare similar cu cel al lui Eumel, dar fără emulare. GMD face parte în prezent din Societatea Fraunhofer .

Din 1987 [4] Jochen Liedtke și echipa sa de la Institutul SET , parte a GMD, au început să dezvolte un nou microkernel, numit „L3” („L3” din „ a treia lucrare a lui L iedtke ”).

Jochen Liedtke a vrut să vadă dacă este posibil să se obțină o performanță ridicată a componentei IPC prin alegerea arhitecturii potrivite pentru kernel și folosind caracteristicile platformei hardware în implementare . Implementarea mecanismului IPC sa dovedit a fi de succes (comparativ cu implementarea complexă a IPC în microkernel-ul Mach). Ulterior, a fost implementat un mecanism pentru a izola zonele de memorie pentru procesele care rulează în spațiul utilizatorului .

În 1988, dezvoltarea a fost finalizată și a fost lansat sistemul de operare cu același nume. Microkernel-ul L3 a fost scris în limbaj de asamblare , a folosit caracteristicile procesoarelor cu arhitectură Intel x86 , nu a acceptat alte platforme și a depășit performanța microkernel-ului Mach. L3 OS era compatibil cu Eumel OS: programele create pentru Eumel OS rulau sub L3 OS, dar nu invers [4] .

Componente microkernel L3:

Din 1989 [4] sistemul de operare a fost utilizat:

L4

În timp ce lucra la microkernel-ul L3, Jochen Liedtke a descoperit defecte în microkernel-ul Mach. Dorind să îmbunătățească performanța, Liedtke a început să codifice noul microkernel în limbaj de asamblare folosind caracteristicile arhitecturii procesorului Intel i386 . Noul microkernel a fost numit „L4” (din „ A patra lucrare a lui L iedtke ”).

În 1993, implementarea microkernel-ului L4 a fost finalizată. Componenta IPC sa dovedit a fi de 20 de ori mai rapidă decât IPC din microkernel-ul Mach [1] .

Sistemele de operare construite pe microkernel-uri de prima generație (în special, pe microkernel-ul Mach) au fost caracterizate de performanțe scăzute. Din această cauză, la mijlocul anilor 1990, dezvoltatorii au început să reconsidere conceptul de arhitectură micronucleară. În special, performanța slabă a microkernel-ului Mach a fost explicată prin mutarea componentei responsabile pentru IPC în spațiul utilizatorului.

Unele componente ale microkernel-ului Mach au fost returnate înapoi - în interiorul microkernel-ului . Acest lucru a încălcat însăși ideea de microkernel (dimensiune minimă, izolarea componentelor), dar a permis creșterea performanței sistemului de operare.

Cercetătorii au căutat motivele performanței slabe a microkernel-ului Mach și au analizat cu atenție componentele care sunt importante pentru o performanță bună. Analiza a arătat că nucleul a alocat proceselor un set de lucru prea mare (multă memorie), drept urmare erorile de cache au apărut constant atunci când nucleul a accesat memorie [ 6 ] . Analiza a făcut posibilă formularea unei noi reguli pentru dezvoltatorii de microkernel - microkernel-ul trebuie proiectat astfel încât componentele importante pentru asigurarea performanței înalte să fie plasate în memoria cache a procesorului (de preferință primul nivel (nivel de engleză 1 , L1) și este de dorit. că a mai rămas ceva spațiu în cache ).   

Din cauza creșterii performanței componentei IPC, sistemele de operare existente nu au putut face față afluxului crescut de mesaje IPC. Mai multe universități (de exemplu , Universitatea Tehnică Dresden , Universitatea din New South Wales ), instituții și organizații (de exemplu, IBM ) au început să creeze implementări ale L4 și să construiască noi sisteme de operare în jurul lor.

În 1996, Liedtke și-a susținut teza de doctorat [7] la Universitatea Tehnică din Berlin pe tema „tabele de pagini protejate” [8] .

Din 1996, la de Cercetare și colegii săi au continuat cercetările privind microkernel-ul L4, microkernel-urile în general și sistemul de operare Sawmill OS în special [9] . Din cauza lipsei de succes comercial, sistemul de operare " IBM Workspace OS ", construit pe a treia versiune a microkernel-ului Mach de la CMU și dezvoltat de IBM din ianuarie 1991 până în 1996 [10] , în locul conceptului de " Microkernel L4" a folosit conceptul de "Lava Nucleus" sau "LN" pe scurt.

De-a lungul timpului, codul de microkernel L4 a fost eliberat de a fi legat de platformă, mecanismele de securitate și izolare au fost îmbunătățite.

În 1999, Liedtke a început să lucreze ca profesor de sisteme de operare la Institutul de Tehnologie din Karlsruhe (Germania) [7] .

Microkernel L4Ka::Alune

În 1999, Jochen Liedtke a fost admis la Systems Architecture Group (SAG), lucrând la Institutul de Tehnologie din Karlsruhe (Germania) și a continuat cercetările privind sistemele de operare micronucleare. Grupul SAG este cunoscut și ca grupul „L4Ka”.

Dorind să demonstreze că un microkernel poate fi implementat într-un limbaj de nivel înalt , grupul SAG a dezvoltat microkernel-ul „L4Ka::Hazelnut”. Lucrarea a fost realizată la Institutul de Tehnologie din Karlsruhe cu sprijinul DFG [11] . Implementarea a fost scrisă în C++ și a suportat procesoare cu arhitectură IA-32 și ARM . Performanța noului microkernel s-a dovedit a fi acceptabilă, iar dezvoltarea nucleelor ​​în limbaj de asamblare a fost întreruptă.

Microkernel L4/Fiasco

În 1998, Grupul de Sisteme de Operare a Universității Tehnice din Dresda a început să dezvolte propria sa implementare a microkernel-ului L4, denumit „L4/Fiasco”. Dezvoltarea a fost realizată în C++ în paralel cu dezvoltarea microkernel-ului L4Ka::Hazelnut.

La acel moment, microkernel-ul L4Ka::Hazelnut nu suporta concurența kernel-space, iar microkernel-ul „L4Ka::Pistachio” suporta doar întreruperi kernel-space la anumite puncte de preempțiune. Dezvoltatorii microkernel-ului „L4/Fiasco” au implementat multitasking preventiv complet (cu excepția unor operațiuni atomice). Acest lucru a făcut ca arhitectura kernelului să fie mai complexă, dar a redus latențe de întrerupere, ceea ce este important pentru un sistem de operare în timp real.

Microkernel-ul „L4/Fiasco” a fost folosit în sistemul de operare „DROPS” [12]  - OS de „hard” real time (când este extrem de important ca evenimentul să fie răspuns în intervale de timp stricte), dezvoltat tot la Universitatea Tehnică din Dresda.

Datorită complexității arhitecturii microkernel-ului în versiunile ulterioare ale sistemului de operare Fiasco, dezvoltatorii au revenit la abordarea tradițională - pornind nucleul cu întreruperi dezactivate (cu excepția câtorva puncte de preempțiune).

Independenta platformei

Microkernel L4Ka::Pistachio

Implementările microkernel-ului L4, create înainte de lansarea microkernel-ului L4Ka::Pistachio și versiunile ulterioare ale microkernel-ului „Fiasco”, au folosit caracteristicile arhitecturii computerului (au fost „legate” de arhitectura procesorului). A fost dezvoltat un API independent de arhitectură. În ciuda adăugării de portabilitate , API-ul a oferit performanțe ridicate. Ideile care stau la baza arhitecturii microkernel nu s-au schimbat.

La începutul anului 2001, a fost publicat un nou API L4, foarte diferit de API-ul L4 al versiunii anterioare, având versiunea numărul 4 ("versiunea 4", cunoscută și ca "versiunea X.2") și diferită:

După lansarea noii versiuni a API-ului, echipa SAG a început să creeze un nou microkernel, numit „L4Ka::Pistachio” [13] [14] . Codul a fost compilat de la zero în C++ folosind experiența proiectului L4Ka::Hazelnut. A fost acordată atenție performanței ridicate și portabilității.

Pe 10 iunie 2001, dr. Jochen Liedtke a murit [7] într-un accident de mașină. După aceea, rata de dezvoltare a proiectului a scăzut considerabil.

În 2003 [15] , lucrarea a fost finalizată datorită eforturilor studenților lui Liedtke: Volkmar Uhlig, Uwe Dannowski și Espen Skoglund. Codul sursă a fost lansat sub licența BSD cu două clauze .

Versiuni noi de Fiasco

În paralel, dezvoltarea microkernel-ului L4/Fiasco a continuat. A fost adăugat suport pentru mai multe platforme hardware ( x86 , AMD64 , ARM ). În special, o versiune de Fiasco numită „FiascoUX” ar putea rula în spațiul utilizatorului care rulează sistemul de operare Linux .

Dezvoltatorii microkernel-ului L4/Fiasco au implementat mai multe extensii la API-ul L4v2.

În plus, microkernel-ul „Fiasco” a oferit mecanisme de gestionare a drepturilor de comunicare. Au existat aceleași mecanisme pentru gestionarea resurselor consumate de kernel.

A fost dezvoltat „L4Env”, un set de componente care rulează peste microkernelul „Fiasco” în spațiul utilizatorului. „L4Env” a fost folosit în „L4Linux”, o implementare a paravirtualizării (ABI de virtualizare) pentru versiunile 2.6.x ale nucleelor ​​Linux .

Universitatea din New South Wales și NICTA

Dezvoltatorii de la Universitatea din New South Wales au creat microkernel-urile L4/MIPS și L4/Alpha, implementări ale L4 pentru procesoarele din seria MIPS pe 64 de biți și DEC Alpha . Microkernel-ul original L4 a suportat doar procesoare cu arhitectură x86 și a devenit cunoscut în mod informal ca „L4/x86”. Implementările au fost scrise de la zero în C și limbaj de asamblare și nu au fost portabile. După lansarea microkernel-ului independent de platformă L4Ka::Pistachio, grupul UNSW a încetat să își dezvolte microkernel-urile și a început să porteze microkernel-ul L4Ka::Pistachio. Implementarea mecanismului de transmitere a mesajelor sa dovedit a fi mai rapidă decât alte implementări (36 de cicluri pe procesoare cu arhitectură Itanium ) [16] .

Grupul UNSW a arătat că un driver de spațiu utilizator se poate executa în același mod ca un driver de spațiu kernel [17] .

Ea a dezvoltat componente pentru paravirtualizarea nucleelor ​​Linux. Componentele au rulat deasupra microkernel-ului L4. Rezultatul a fost numit " Wombat OS ". Wombat OS ar putea rula pe arhitecturi x86, ARM și MIPS. Pe procesoarele Intel XScale , Wombat OS a efectuat o schimbare de context de 30 de ori mai lent decât un nucleu Linux monolitic [18] .

Grupul UNSW sa mutat apoi la NICTA, a creat un furk al microkernel-ului L4Ka::Pistachio și l-a numit „NICTA::L4-embedded”. Noul microkernel a fost scris pentru sisteme încorporate comerciale , a necesitat puțină memorie și a implementat un API L4 simplificat. Cu un API simplificat, apelurile de sistem au fost făcute atât de „scurte” încât nu au necesitat puncte multitasking preventive și au permis implementarea sistemului de operare în timp real [19] .

Utilizare comercială

Qualcomm rula implementarea de către NICTA a microkernel-ului L4 pe un chipset numit „Mobile Station Modem” (MSM) Acest lucru a fost raportat în noiembrie 2005 [20] de către reprezentanții NICTA, iar la sfârșitul anului 2006, chipset-urile MSM au intrat în vânzare. Deci implementarea microkernel-ului L4 a ajuns în telefoanele mobile .

În august 2006, Heiser a Open Kernel Labs La acea vreme, Heiser a servit ca șef al programului ERTOS organizat de NICTA [21] și a fost profesor la UNSW. OK Labs a fost creat pentru

În aprilie 2008, a fost lansată versiunea 2.1 a microkernel-ului „OKL4”, prima implementare publică a L4 care are securitate bazată pe capacități . În octombrie 2008, a fost lansată versiunea 3.0 [22] - cea mai recentă versiune open source  a „OKL4” . Codul sursă pentru următoarele versiuni a fost închis. Stratul de microkernel care alimentează hipervizorul a fost rescris pentru a adăuga suport pentru un hipervizor nativ numit „microvizor OKL4” [23] .

OK Labs a distribuit un sistem de operare Linux  paravirtualizat numit OK :Linux [24] . OK : Linux a fost un descendent al Wombat OS . OK Labs a distribuit, de asemenea, versiuni paravirtualizate ale sistemelor de operare Symbian și Android .

OK Labs a achiziționat drepturile asupra microkernel-ului seL4 de la NICTA.

La începutul anului 2012, au fost vândute peste 1,5 miliarde de dispozitive , echipate cu o implementare a microkernel-ului L4 [25] . Cele mai multe dintre aceste dispozitive au conținut cipuri care implementează modemuri wireless și au fost lansate de Qualcomm .

O implementare a L4 a fost, de asemenea, utilizată în sistemele de divertisment în mașină [26] .

Sistemul de operare, construit pe baza implementării L4, a fost executat de procesorul secure enclave, care face parte din circuitul electronic Apple A7 situat pe cip [27] . Aceeași implementare L4 a fost folosită în proiectul Darbat al NICTA [28] . Dispozitivele care conțin Apple A7 sunt livrate cu iOS . În 2015, existau aproximativ 310 milioane de dispozitive iOS [29] .

Verificare

seL4

În 2006, a început dezvoltarea celei de -a treia generații de microkernel , numită „seL4” [30] . Dezvoltarea a început de la zero de către un grup de programatori de la NICTA. Scop: crearea unei baze pentru construirea de sisteme sigure și fiabile care să poată îndeplini cerințele moderne de securitate, așa cum este scris, de exemplu, în documentul „Criterii generale pentru evaluarea securității tehnologiei informației”. Încă de la început, codul microkernel-ului a fost scris în așa fel încât să se poată verifica (verificarea corectitudinii). Verificarea a fost efectuată folosind limbajul Haskell : cerințele pentru microkernel (specificația) au fost scrise în limbajul Haskell; obiectele microkernel au fost reprezentate ca obiecte Haskell; lucrul cu echipamentul a fost emulat [31] . Pentru a putea obține informații despre disponibilitatea unui obiect prin efectuarea unui raționament formal, seL4 a folosit controlul accesului bazat pe securitatea bazată pe capacități.

În 2009, a fost finalizată dovada corectitudinii codului de microkernel seL4 [32] . Existența unei dovezi a asigurat conformitatea între implementare și specificație, a confirmat absența unor bug-uri în implementare (de exemplu, absența deadlock -urilor, livelock-urilor, buffer overflows , excepții aritmetice și cazuri de utilizare a variabilelor neinițializate). Microkernel-ul seL4 a fost primul microkernel conceput pentru un sistem de operare general și verificat [32] .

Microkernel-ul seL4 a implementat managementul non-standard al resurselor kernelului [33] :

Ceva similar a fost implementat în sistemul experimental Barrelfish OS . Datorită acestei abordări de gestionare a resurselor nucleului, a devenit posibilă efectuarea raționamentului cu privire la izolarea proprietăților, iar ulterior s-a dovedit că microkernel-ul seL4 asigură integritatea și confidențialitatea proprietăților [34] . Dovada a fost făcută pentru codul original.

O echipă de cercetători de la firma NICTA a demonstrat corectitudinea traducerii textului din limbajul C în codul mașinii. Acest lucru a făcut posibilă excluderea compilatorului din lista de software de încredere și să se considere că dovada efectuată pentru codul sursă microkernel este valabilă și pentru fișierul executabil microkernel.

Microkernel-ul seL4 a devenit primul nucleu în mod protejat pentru care analiza timpului de execuție în cel mai rău caz a fost efectuată în întregime, iar rezultatele acestei analize au fost publicate. Rezultatele analizei sunt necesare pentru utilizarea microkernel-ului într-un sistem de operare hard în timp real [34] .

29 iulie 2014 NICTA și General Dynamics C4 Systemsa anunțat lansarea microkernel-ului seL4 (inclusiv toate dovezile corectitudinii lor) sub licențe deschise [35] . Codul sursă pentru microkernel și dovezile au fost lansate sub licența GPL v2. Majoritatea bibliotecilor și instrumentelor au fost distribuite sub licența BSD cu două clauze.

O afirmație interesantă a cercetătorilor [36] este că costul efectuării verificării software-ului este mai mic decât costul cercetării software tradiționale, în ciuda faptului că informații mult mai fiabile pot fi obținute în timpul verificării.

În august 2012, NICTA, Rockwell Collins, Galois Inc , Boeing și Universitatea din Minnesota , ca parte a unui program de dezvoltare a sistemelor cibernetice militare de înaltă încredere [37] organizat de agenția DARPA , au început dezvoltarea unui vehicul aerian fără pilot [38] . Principala cerință pentru dezvoltare este asigurarea fiabilității ridicate a dispozitivului. Fiecare dintre firmele enumerate a avut un rol de jucat în program. NICTA a fost responsabil pentru dezvoltarea sistemului de operare și l-a construit în jurul microkernel-ului seL4. Sarcinile responsabile au fost implementate ca componente microkernel, în timp ce cele neresponsabile au fost rulate sub un sistem de operare Linux paravirtualizat. Dezvoltarile programului au fost planificate pentru a fi utilizate în elicopterul NICTA Unmanned Little Bird, care a fost dezvoltat de Boeing. Elicopterul trebuia să suporte atât controlul pilotului, cât și modul fără pilot. În noiembrie 2015, a fost raportată o implementare cu succes [39] .

Alte cercetări și dezvoltare

Hurd/L4 . În noiembrie 2000, lista de corespondență „l4-hurd” a fost creată pentru a discuta ideea de a porta kernel-ul „ GNU Hurd ” la microkernel-ul L4. Portarea a fost efectuată în perioada 2002-2004, rezultatul a fost numit „Hurd / L4”. Implementarea „Hurd/L4” nu a fost finalizată. În 2005 proiectul a fost oprit [40] .

Osker  este un sistem de operare care implementează L4 și a fost scris în Haskell în 2005 . Scopul proiectului: testarea posibilității implementării OS într-un limbaj funcțional (și nu studierea microkernel-ului) [41] .

Codezero  este o implementare a microkernel-ului L4 pentru sisteme încorporate care a devenit disponibilă public în vara anului 2009 [42] . Creat de dezvoltatorii companiei britanice „B Labs” de la zero. Codul a fost scris în C. Implementarea acceptă procesoare cu arhitectură ARM , implementează un hypervisor de ordinul întâi și acceptă virtualizarea sistemului de operare Linux și Android [43] [44] . În ciuda declarației despre livrarea codului sub licența GPL v3, este imposibil să descărcați codul de pe site-ul oficial.

F9  este o implementare a microkernel-ului L4 care a devenit disponibil public în iulie 2013 [45] . Scris de la zero în C. Proiectat pentru sisteme încorporate. Suporta arhitectura ARM seria de procesoare Cortex-M . Codul este furnizat sub o licență BSD.

Fiasco.OC  este un microkernel de a treia generație bazat pe microkernel-ul „L4/Fiasco”. Implementează mecanismul de securitate bazat pe capacitate, suportă procesoare multi-core și virtualizare hardware [46] .

L4 Runtime Environment (L4Re pe scurt) este un cadru care rulează peste microkernel-ul „Fiasco.OC” și este conceput pentru a crea componente pentru spațiul utilizatorului. L4Re oferă funcționalități pentru construirea de aplicații client/server, implementarea sistemelor de fișiere, implementarea bibliotecilor populare, cum ar fi biblioteca standard C ("libc"), biblioteca standard C++ ("libstdc++") și biblioteca pthreads .

Cadrul L4Re și microkernel-ul „Fiasco.OC” au suportat arhitecturi x86 (IA-32 și AMD64), ARM și PowerPC (WiP).

L4Linux  este un subsistem pentru rularea sistemului de operare Linux peste microkernel-ul „Fiasco.OC” folosind paravirtualizarea [47] . Anterior, în locul perechii „Fiasco.OC” - L4Re, a fost folosită perechea „L4 / Fiasco” - L4Env.

NOVA ( the  N OVA O S v irtualization a rhitecture ) este un proiect de cercetare creat pentru a crea un mediu de virtualizare sigur și eficient [48] [49] [50] cu o mică listă de software de încredere ( bază de calcul de încredere ) .  NOVA include:

Proiectul NOVA a suportat procesoare x86 multi-core. Pentru a rula sub controlul unui micro-hypervisor (un hypervisor construit pe un microkernel) NOVA, sistemul de operare invitat trebuie să accepte Intel VT-x sau AMD-V . Codul sursă a fost furnizat sub licența GPL v2.

Xameleon  este un sistem de operare bazat pe microkernel-ul L4 [52] . Proiectul a fost fondat în 2001 de singurul dezvoltator Alexei Mandrykin (născut pe 19 ianuarie 1973 ). Sistemul de operare a fost construit inițial pe microkernel -ul „ L4/Fiasco ”. Mai târziu, autorul a migrat sistemul de operare la microkernel-ul „ L4Ka::Pistachio ”. Codul sursă al sistemului de operare este închis.

WrmOS este un sistem de operare în timp real (RTOS) cu sursă deschisă bazat pe microkernel-ul L4. WrmOS are propria sa implementare a nucleului, biblioteci standard și stiva de rețea. Arhitecturile de procesor acceptate sunt SPARC, ARM, x86, x86_64. Nucleul WrmOS se bazează pe documentul L4 Kernel Reference Manual Versiunea X.2 . Există un nucleu Linux paravirtualizat ( w4linux ) care rulează pe WrmOS.

Note

  1. ↑ 1 2 Liedtke, Jochen (decembrie 1993 ). „Îmbunătățirea IPC prin designul nucleului” (PDF) . Al 14-lea simpozion ACM privind principiile sistemului de operare . Asheville , NC , SUA . pp. 175-88. Verificați data la |date=( ajutor în engleză ) Arhivat pe 4 martie 2016 la Wayback Machine
  2. ↑ Familia L4 de micronuclee. Prezentare generală Arhivată 14 mai 2015 la Wayback Machine  (engleză) // Site -ul web al Universității Tehnice din Dresda ( Germania ).
  3. ↑ ELAN Language Arhivat 12 mai 2015 pe site- ul Wayback Machine  // Universitatea Tehnică din Dresda .
  4. ↑ 1 2 3 4 5 6 7 8 9 10 Liedtke, Jochen (decembrie 1993 ). „Un sistem persistent în uz real – experiențe din primii 13 ani” (PDF) . Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS) . Asheville , NC , SUA . pp. 2-11. Verificați data la |date=( ajutor în engleză ) Arhivat pe 10 iulie 2015 la Wayback Machine
  5. ↑ 1 2 In Memoriam Jochen Liedtke (1953-2001) Arhivat 5 martie 2012 la Wayback Machine .
  6. ↑ 1 2 Liedtke, Jochen (decembrie 1995 ). „Despre construcția µ-Kernel” . Proc. Al 15-lea simpozion ACM privind principiile sistemelor de operare (SOSP) . pp. 237-250. Verificați data la |date=( ajutor în engleză ) Arhivat pe 18 martie 2009 la Wayback Machine
  7. ↑ 1 2 3 Grup de arhitectură de sistem. despre noi. oameni. Liedtke . Copie arhivată .
  8. ↑ Jochen Liedtke. Structuri de tabel de pagini pentru memorie virtuală cu granulație fină Arhivat la 12 noiembrie 2007 la Wayback Machine . Raport tehnic 872. Centrul național german de cercetare pentru informatică (GMD). octombrie 1994 .
  9. ↑ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathan; Deller, Luke; Reuther, Lars ( 2000 ). „Abordarea multiserver Sawmill” . Atelierul European ACM SIGOPS . Kolding , Danemarca . pp. 109-114. Verificați data la |date=( ajutor în engleză )
  10. ↑ Fleisch, Brett D; Allan, Mark. Microkernel și OS la locul de muncă: un  studiu de caz . — John Wiley & Sons, Ltd. Arhivat din original pe 24 august 2007.
  11. ↑ Pagina de grup „L4Ka” // archive.org .
  12. ↑ Prezentare generală a picăturilor Arhivat la 7 august 2011 la Wayback Machine .
  13. ↑ Microkernel „L4Ka::Pistachio” Arhivat pe 9 ianuarie 2007 la Wayback Machine  .
  14. ↑ Echipa de dezvoltare „L4Ka” Arhivată la 22 ianuarie 2007 la Wayback Machine  .
  15. ↑ Microkernelul L4Ka::Pistachio . (Engleză) Carte albă . PDF . 1 mai 2003 // archive.org .
  16. ↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (aprilie 2005). Itanium - povestea implementatorului sistemului . Conferința tehnică anuală USENIX . Annaheim , CA , SUA . pp. 264-278. Parametru depreciat folosit |coauthors=( ajutor );Verificați data la |date=( ajutor în engleză ) Arhivat pe 17 februarie 2007 la Wayback Machine
  17. ↑ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Gotz, Stefan; Grey, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot . Drivere de dispozitiv la nivel de utilizator: performanță atinsă  (neopr.)  // Journal of Computer Science and Technology. - T. 20 , nr 5 . — S. 654-664 . - doi : 10.1007/s11390-005-0654-4 .
  18. ↑ van Schaik, Carl; Heiser, Gernot (ianuarie 2007). „Microkernel-uri de înaltă performanță și virtualizare pe ARM și arhitecturi segmentate” . Primul Atelier Internațional de Microkernel-uri pentru Sisteme Embedded . Sydney , Australia : NICTA . pp. 11-21 . Accesat 2007-04-01 . Verificați data la |date=( ajutor în engleză ) Arhivat pe 26 aprilie 2007 la Wayback Machine
  19. ↑ Ruocco, Sergio. Un tur de programator în timp real al microkernel-urilor L4 de uz general //  EURASIP  Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications : jurnal. - 2008. - octombrie ( vol. 2008 ). - P. 1-14 . - doi : 10.1155/2008/234710 .  (link indisponibil)
  20. ↑ [1] Arhivat la 25 august 2006 la Wayback Machine .
  21. ↑ Pagina programului ERTOS de pe site-ul NICTA // archive.org .
  22. ↑ OKL4 3.0 (link descendent) . Consultat la 21 mai 2011. Arhivat din original pe 16 mai 2011. 
  23. ↑ Microvizor OKL4 Arhivat la 13 martie 2014 la Wayback Machine .
  24. ↑ OK:Linux (link descendent) . Preluat la 8 iulie 2015. Arhivat din original la 10 aprilie 2015. 
  25. ↑ Open Kernel Labs (19 ianuarie 2012). Software-ul Open Kernel Labs depășește pragul de 1,5 miliarde de livrări de dispozitive mobile . Comunicat de presă . Accesat 2015-11-10 .
  26. ↑ Open Kernel Labs ( 27 martie 2012 ). Virtualizarea autovehiculelor Open Kernel Labs selectată de Bosch pentru sistemele de infotainment . Comunicat de presă . Arhivat din original pe 2 iulie 2012.
  27. ↑ Securitate iOS . Preluat la 28 septembrie 2017. Arhivat din original la 23 septembrie 2014.
  28. ↑ Proiectul Darbat Arhivat 19 decembrie 2013 la Wayback Machine .
  29. ↑ [2] Arhivat pe 15 iulie 2015 la Wayback Machine .
  30. ↑ [3] Arhivat 3 mai 2022 la Wayback Machine .
  31. ↑ Derrin, Filip; Elphinstone, Kevin; Klein, Gerwin; cocoş; David; Chakravarty, Manuel MT (septembrie 2006 ). „Rularea manualului: o abordare a dezvoltării de microkernel de înaltă asigurare” (PDF) . Atelierul ACM SIGPLAN Haskell . Portland , Oregon , SUA . pp. 60-71. Verificați data la |date=( ajutor în engleză ) Arhivat pe 3 martie 2016 la Wayback Machine
  32. ↑ 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronic, iunie; Cocoș, David; Derrin, Filip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Atinge, Harvey; Winwood, Simon (octombrie 2009 ). „seL4: Verificarea formală a unui nucleu OS” (PDF) . Al 22-lea simpozion ACM privind principiile sistemului de operare . Big Sky , MT , SUA . Verificați data la |date=( ajutor în engleză ) Arhivat pe 28 iulie 2011 la Wayback Machine
  33. ↑ Elkaduwe, Dhammika; Derrin, Filip; Elphinstone, Kevin (aprilie 2008 ). „Proiectarea nucleului pentru izolarea și asigurarea memoriei fizice” . Primul Atelier de Izolare și Integrare în Sisteme Embedded . Glasgow , Marea Britanie . DOI : 10.1145/1435458 . Accesat 2015-07-08 . Parametru depreciat folosit |coauthors=( ajutor );Verificați data la |date=( ajutor în engleză ) Arhivat pe 24 aprilie 2010 la Wayback Machine
  34. ↑ 1 2 Klein, Gerwin; Andronic, iunie; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Verificarea formală cuprinzătoare a unui microkernel OS  (engleză)  // ACM Transactions on Computer Systems: journal. — Vol. 32 , nr. 1 . — P. 2:1-2:70 . - doi : 10.1145/2560537 .
  35. ↑ NICTA ( 29 iulie 2014 ). Sistemul de operare securizat dezvoltat de NICTA devine open source . Comunicat de presă . Arhivat din original pe 10 august 2014. Preluat 2015-07-08 .
  36. ↑ Klein, Gerwin; Andronic, iunie; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Verificarea formală cuprinzătoare a unui microkernel OS  (engleză)  // ACM Transactions on Computer Systems: journal. - 2014. - Vol. 32 . — P. 64 . - doi : 10.1145/2560537 .
  37. ↑ Sisteme militare cibernetice de înaltă asigurare Arhivat 8 august 2014. (HACM-uri).
  38. ↑ Proiectul SMACCM Arhivat 10 iulie 2015 pe site-ul Wayback Machine // NICTA. SMACCM este o abreviere a englezei.  compoziția sigură, asigurată din punct de vedere matematic, a modelelor de control .
  39. ↑ Dronele de nouă generație nu pot fi piratate Arhivat 18 noiembrie 2015 la Wayback Machine // Popular Mechanics Magazine. 12 noiembrie 2015.
  40. ↑ Istoria GNU Hurd. Portare la un alt microkernel Arhivat 8 martie 2017 la Wayback Machine  .
  41. ↑ Hallgren, T.; Jones, deputat; Leslie, R.; Tolmach, A. O abordare principială a construcției sistemului de operare în Haskell  //  Actele celei de-a zecea conferințe internaționale ACM SIGPLAN privind programarea funcțională : jurnal. - 2005. - Vol. 40 , nr. 9 . - P. 116-128 . — ISSN 0362-1340 . - doi : 10.1145/1090189.1086380 .
  42. ↑ Codezero Arhivat 9 iulie 2015 la Wayback Machine pe genode.org.
  43. ↑ dev.b-labs.com // archive.org .
  44. ↑ Site-ul oficial al proiectului Codezero Arhivat 9 iulie 2015 la Wayback Machine .
  45. ↑ Depozitul de proiect F9 Arhivat 5 martie 2017 la Wayback Machine // github.com .
  46. ↑ Petru, Mihai; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (martie 2009 ). „Mașini virtuale închise - Virtualizare în sisteme cu baze de calcul mici de încredere” . VTDS'09: Workshop on Virtualization Technology for Fiable Systems . Nürnberg , Germania . Parametru depreciat folosit |coauthors=( ajutor );Verificați data la |date=( ajutor în engleză )
  47. ↑ L4Linux Arhivat pe 7 iulie 2015 la Wayback Machine .
  48. ↑ Steinberg, Udo; Bernhard, Kauer (aprilie 2010 ). „NOVA: O arhitectură de virtualizare sigură bazată pe microhypervisor”. EuroSys '10: Actele celei de-a 5-a Conferințe europene privind sistemele informatice . Paris , Franța . Verificați data la |date=( ajutor în engleză )
  49. ↑ Steinberg, Udo; Bernhard, Kauer (aprilie 2010 ). „Către un mediu scalabil la nivel de utilizator multiprocesor”. IIDS'10: Atelier de izolație și integrare pentru sisteme de încredere . Paris , Franța . Verificați data la |date=( ajutor în engleză )
  50. ↑ Project Nova Arhivat 24 iunie 2015 la Wayback Machine . Site-ul oficial.
  51. ↑ VMM Seoul Arhivat 11 iunie 2018 la Wayback Machine // github.com
  52. ↑ l4os.ru Arhivat 9 februarie 2011 la Wayback Machine . Site-ul oficial al proiectului Xameleon.

Literatură

Link -uri