A projekt, amely az open source seL4 mikrokernel fejlesztésén dolgozik, elnyerte az ACM Software System Award díjat, amelyet évente adományoz az ACM, a számítógépes rendszerek területén legtekintélyesebb nemzetközi szervezet. A díjat a megbízhatóság matematikai bizonyítására tett eredményekért ítélték oda, amelyek a formális nyelven megfogalmazott specifikációknak való teljes megfelelést igazolják, és elismerik a kritikus alkalmazásokban való használatra való készenlétet. A seL4 projekt bemutatta, hogy nemcsak teljes körű formális verifikációt lehet végezni ipari operációs rendszerek szintjén, hanem ezt teljesítmény és univerzalitás rovására is lehet tenni.
Az ACM Software System Award díjat évente a szoftverrendszerek fejlesztéséért adják át, amelyek meghatározó hatást gyakoroltak az iparágra, új koncepciókat hoztak be a gyakorlatba, vagy új kereskedelmi alkalmazási területeket tárták fel. A díj összege 35 ezer amerikai dollár. Az elmúlt években az ACM díjat kaptak a GCC és LLVM projekteket, valamint azok alapítói, Richard Stallman és Chris Lattner. Emellett olyan projekteket és technológiákat is díjaztak, mint az UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB és Eclipse.
A seL4 mikrokernel architektúrája figyelemre méltó, mivel a kernel erőforrás-kezelő részeit a felhasználói térbe helyezi, és ugyanazokat a hozzáférés-vezérlési eszközöket alkalmazza e forrásokhoz, mint a felhasználói erőforrásokhoz. A mikrokernel nem nyújt készen álló, magas szintű absztrakciókat a fájlok, folyamatok, hálózati kapcsolatok stb. kezelésére, hanem csupán minimális mechanizmusokat biztosít a fizikai címzési térhez, megszakításokhoz és a CPU erőforrásokhoz való hozzáférés kezelésére. A magas szintű absztrakciók és az eszközökkel való interakcióra szolgáló driverek külön feladatok formájában valósulnak meg a mikrokernel felett, amelyek felhasználói szinten futnak. Az ilyen feladatok hozzáférését a mikrokernel erőforrásaihoz a szabályok meghatározása révén szervezik.
Forrás: opennet.ru
