Projekt rozvíjajúci otvorené mikrojadro seL4 získal ocenenie ACM Software System Award, ktoré každoročne udeľuje Asociácia výpočtovej techniky (ACM), najuznávanejšia medzinárodná organizácia v oblasti počítačových systémov. Ocenenie bolo udelené za úspechy v oblasti matematického dôkazu spoľahlivosti, ktorý potvrdzuje plnú zhodu s predpísanými formálnymi špecifikáciami a uznáva pripravenosť na použitie v kritických aplikáciách. Projekt seL4 preukázal, že je možné nielen úplne vykonať formálnu verifikáciu spoľahlivosti a bezpečnosti pre projekty na úrovni priemyselných operačných systémov, ale aj dosiahnuť to bez straty výkonu a univerzálnosti.
Ocenenie ACM Software System Award sa každoročne udeľuje za vývoj softvérových systémov, ktoré mali rozhodujúci vplyv na odvetvie, zaviedli nové koncepcie alebo odhalili nové oblasti komerčného využitia. Výška ocenenia je 35 tisíc dolárov. V predchádzajúcich rokoch boli ocenenia ACM udelené projektom GCC a LLVM, ako aj ich zakladateľom Richardovi Stallmanovi a Chrisovi Lattnerovi. Ocenením boli tiež priznane projekty a technológie ako UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB a Eclipse.
Architektúra mikrojadra seL4 sa vyznačuje presunom častí na správu zdrojov jadra do priestoru používateľa a využívaním pre tieto zdroje rovnakých prístupových mechanizmov ako pre používateľské zdroje. Mikrojadro neposkytuje hotové vysokúrovňové abstrakcie pre správu súborov, procesov, sieťových pripojení a pod., namiesto toho poskytuje iba minimálne mechanizmy pre správu prístupu k fyzikálnemu adresnému priestoru, prerušenia a procecorových zdrojov. Vysokúrovňové abstrakcie a ovládače na interakciu s hardvérom sú implementované samostatne nad mikrojadrom vo forme úloh, ktoré sa vykonávajú na používateľskej úrovni. Prístup týchto úloh k zdrojom mikrojadra je organizovaný prostredníctvom definície pravidiel.
Zdroj: opennet.ru
