SeL4 atvērtā mikrokodolu projekts ir saņēmis ACM Software System Award, kas ir ikgadējā balva, ko piešķir skaitļošanas tehnikas asociācija (ACM), cienījamākā starptautiskā organizācija datorsistēmu jomā. Apbalvojums tiek piešķirts par sasniegumiem darbības matemātiskā pierādīšanas jomā, kas norāda uz pilnīgu atbilstību oficiālajā valodā sniegtajām specifikācijām un atzīst gatavību izmantošanai misijai kritiskos lietojumos. SeL4 projekts ir parādījis, ka ir iespējams ne tikai pilnībā formāli pārbaudīt projektu uzticamību un drošību industriālo operētājsistēmu līmenī, bet arī to panākt, nezaudējot veiktspēju un daudzpusību.
ACM Software System Award tiek pasniegta katru gadu, lai novērtētu programmatūras sistēmu izstrādi, kurām ir bijusi izšķiroša ietekme uz nozari, ieviešot jaunas koncepcijas vai atverot jaunas komerciālas lietojumprogrammas. Balvas apmērs ir 35 tūkstoši ASV dolāru. Iepriekšējos gados ACM balvas ir piešķirtas GCC un LLVM projektiem, kā arī to dibinātājiem Ričardam Stallmanam un Krisam Latneram. Citi projekti un tehnoloģijas, kas arī tika apbalvotas, bija UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB un eclipse .
SeL4 mikrokodola arhitektūra ir ievērojama ar daļu noņemšanu kodola resursu pārvaldībai lietotāja telpā un tādu pašu piekļuves kontroles līdzekļu piemērošanu šādiem resursiem kā lietotāju resursiem. Mikrokodolis nenodrošina gatavu augsta līmeņa abstrakcijas failu, procesu, tīkla savienojumu un tamlīdzīgu pārvaldīšanai, tā vietā tas nodrošina tikai minimālus mehānismus, lai kontrolētu piekļuvi fiziskajai adrešu telpai, pārtraukumiem un procesora resursiem. Augsta līmeņa abstrakcijas un draiveri mijiedarbībai ar aparatūru tiek ieviesti atsevišķi virs mikrokodola lietotāja līmeņa uzdevumu veidā. Šādu uzdevumu piekļuve mikrokodola rīcībā esošajiem resursiem tiek organizēta, definējot noteikumus.
Avots: opennet.ru