seL4 avatud mikrotuuma projekti omanikud pälvisid ACM Software System Award'i, mis antakse igal aastal välja ACM-i (Association for Computing Machinery) poolt, mis on kõige tuntum rahvusvaheline organisatsioon arvutisüsteemide valdkonnas. Auhind anti matemaatilise tõestamise saavutuste eest, mis kinnitab, et süsteem vastab formaalses keeles esitatud spetsifikatsioonidele ja tunnustab selle kasutamiseks sobivust kriitilise tähtsusega rakendustes. seL4 projekt tõestab, et mitte ainult et on võimalik täielikult läbi viia formaalne verifitseerimine tööstuslike operatsioonisüsteemide tasemel, vaid seda on võimalik saavutada ka ilma jõudluse ja universaalsuse kahjuks toomata.
ACM Software System Award antakse igal aastal välja tarkvarasüsteemide arenduse eest, mis on avaldanud olulist mõju tööstusele, tuues kasutusele uusi kontseptsioone või avardades uusi kaubanduslikke rakendusi. Auhinna suurus on 35 000 USA dollarit. Eelmistel aastatel on ACM auhindadega tunnustatud projekte GCC ja LLVM ning nende loojaid Richard Stallmanit ja Chris Latnerit. Auhind on antud ka sellistele projektidele ja tehnoloogiatele nagu UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ja Eclipse.
seL4 mikrokernel'i arhitektuur paistab silma selle poolest, et osad tuumast, mis haldavad ressursside haldamist, on viidud kasutajaruumis ja nende ressursside jaoks kasutatakse samu juurdepääsukontrolli vahendeid nagu kasutajaressursside jaoks. Mikrokernel ei paku valmis kõrgtasemel abstraktsioone failide, protsesside, võrguühenduste jne haldamiseks, vaid ainult minimaalset mehhanismide kogumit füüsilise aadressiruumi, katkestuste ja CPU ressursside haldamiseks. Kõrgtasemel abstraktsioonid ja seadme draiverid, mis suhtlevad riistvaraga, rakendatakse eraldi mikrokernel'i peal ülesannete kujul, mis töötavad kasutajaruumis. Selliste ülesannete juurdepääs mikrokernel'il olevatele ressurssidele organiseeritakse reeglite määratlemise kaudu.
Allikas: opennet.ru
