Projekt, mis arendab avatud mikro tuuma seL4, pälvis ACM Software System Award'i, mille iga-aastaselt annab välja ACM (Association for Computing Machinery), rahvusvaheline autoriteet arvutisüsteemide valdkonnas. Auhind anti matemaatilisi tõendeid usaldusväärsuse kohta, mis näitab täielikku vastavust formaalkeeles esitatud spetsifikatsioonidele ja tunnustab valmidust kasutamiseks kriitilistes rakendustes. Projekt seL4 näitas, et on võimalik täielikult läbi viia formaalne kinnitamine usaldusväärsuse ja ohutuse osas tööstuslike operatsioonisüsteemide tasemel, saavutades seda ilma jõudluse ja mitmekesisuse kahjustamiseta.
ACM Software System Award'i antakse igal aastal välja tarkvarasüsteemide arendamise eest, mis on olulisel määral mõjutanud tööstust, tutvustades uusi kontseptsioone või avades uusi kaubanduslikke rakendusi. Auhinna suurus on 35 tuhat USA dollarit. Varasematel aastatel on ACM auhindu antud projektidele GCC ja LLVM ning nende asutajatele Richard Stallmanile ja Chris Latnerile. Au on saanud ka sellised projektid ja tehnoloogiad nagu UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ja Eclipse.
Mikrokiibi seL4 arhitektuur on tähelepanuväärne, kuna osade kernelite ressursside haldamine on viidud kasutajaruumi, rakendades neid samu juurdepääsukontrolli meetodeid, mis on ette nähtud kasutajaressursside haldamiseks. Mikrokiip ei paku valmis kõrgema taseme abstraktsioone failide, protsesside, võrguühenduste jms haldamiseks, vaid pakub ainult minimaalset mehhanismi füüsiliste aadressiruumide, katkestuste ja protsessori ressursside juurdepääsu haldamiseks. Kõrgema taseme abstraktsioonid ja draiverid riistvaraga suhtlemiseks rakendatakse eraldi mikrokiibi pinnal kasutatavate ülesannete kujul, mis toimuvad kasutaja tasemel. Aksesne nendel ülesannetel olevate mikrokiibi ressursside valitsemiseks korraldatakse reeglite määratlemise kaudu.
Allikas: opennet.ru
