seL4 ашық микроядро жобасы компьютерлік жүйелер саласындағы ең беделді халықаралық ұйым - Есептеу машиналары қауымдастығы (ACM) беретін жыл сайынғы марапат - ACM Software System Award сыйлығын алды. Сыйлық жұмыстың математикалық дәлелі саласындағы жетістіктері үшін беріледі, бұл ресми тілде берілген спецификацияларға толық сәйкестігін көрсетеді және миссиясы маңызды қосымшаларда пайдалануға дайындығын мойындайды. seL4 жобасы өнеркәсіптік операциялық жүйелер деңгейінде жобалардың сенімділігі мен қауіпсіздігін толық ресми түрде тексеруге ғана емес, сонымен қатар өнімділік пен әмбебаптылықты жоғалтпай оған қол жеткізуге болатындығын көрсетті.
ACM бағдарламалық қамтамасыз ету жүйесі сыйлығы салаға айқын әсер еткен, жаңа концепцияларды енгізген немесе жаңа коммерциялық қосымшаларды ашқан бағдарламалық жүйелердің дамуын мойындау үшін жыл сайын беріледі. Сыйлықтың көлемі 35 мың АҚШ долларын құрайды. Өткен жылдары ACM марапаттары GCC және LLVM жобаларына және олардың негізін қалаушылар Ричард Сталлман мен Крис Латнерге берілді. Сыйлық сонымен қатар UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB және Eclipse сияқты жобалар мен технологияларға берілді.
seL4 микроядросының архитектурасы пайдаланушы кеңістігіндегі ядро ресурстарын басқаруға арналған бөліктерді жоюмен және пайдаланушы ресурстары сияқты ресурстарға бірдей қатынасты басқару құралдарын қолдануымен ерекшеленеді. Микроядро файлдарды, процестерді, желілік қосылымдарды және т.б. басқару үшін қордан тыс жоғары деңгейлі абстракцияларды қамтамасыз етпейді, оның орнына ол физикалық мекенжай кеңістігіне, үзілістерге және процессор ресурстарына қол жеткізуді басқарудың ең аз механизмдерін ғана қамтамасыз етеді. Аппараттық құралдармен әрекеттесу үшін жоғары деңгейлі абстракциялар мен драйверлер пайдаланушы деңгейіндегі тапсырмалар түрінде микроядроның жоғарғы жағында бөлек жүзеге асырылады. Мұндай тапсырмалардың микроядроға қолжетімді ресурстарға қол жеткізуі ережелерді анықтау арқылы ұйымдастырылады.
Ақпарат көзі: opennet.ru