Ochiq seL4 mikroyadrosini ishlab chiqish loyihasi har yili kompyuter tizimlari sohasidagi eng nufuzli xalqaro tashkilot hisoblovchi mashinalar assotsiatsiyasi (ACM) tomonidan beriladigan ACM Software System mukofotiga sazovor bo'ldi. Mukofot rasmiy tilda ko'rsatilgan spetsifikatsiyalarga to'liq mos kelishini ko'rsatadigan va muhim vazifalarda foydalanishga tayyorligini e'tirof etuvchi operatsiya ishonchliligini matematik isbotlash sohasidagi yutuqlar uchun beriladi. seL4 loyihasi nafaqat sanoat operatsion tizimi darajasidagi dizaynlar uchun ishonchlilik va xavfsizlikni to'liq rasmiy ravishda tekshirish, balki unumdorlik va ko'p qirralilikni buzmasdan bunga erishish mumkinligini ko'rsatdi.
ACM dasturiy ta'minot tizimi mukofoti har yili sanoatga aniq ta'sir ko'rsatgan, yangi kontseptsiyalarni joriy etgan yoki tijorat qo'llanilishining yangi sohalarini ochgan dasturiy ta'minot tizimlarining rivojlanishini tan olish uchun taqdim etiladi. Mukofot miqdori 35 ming AQSh dollarini tashkil etadi. O'tgan yillarda ACM mukofotlari GCC va LLVM loyihalariga hamda ularning asoschilari Richard Stallman va Kris Latnerga berildi. Mukofot, shuningdek, UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB va Eclipse kabi loyihalar va texnologiyalarni taqdirladi. .
seL4 mikroyadrosi arxitekturasi yadro resurslarini foydalanuvchi maydoniga boshqarish uchun qismlarni ko'chirish va foydalanuvchi resurslari kabi resurslarga kirishni boshqarish vositalaridan foydalanish bilan ajralib turadi. Mikroyadro fayllarni, jarayonlarni, tarmoq ulanishlarini va shunga o'xshashlarni boshqarish uchun tayyor yuqori darajadagi abstraktsiyalarni ta'minlamaydi, aksincha, u jismoniy manzil maydoniga, uzilishlar va protsessor resurslariga kirishni boshqarishning minimal mexanizmlarini taqdim etadi. Yuqori darajadagi abstraktsiyalar va apparat bilan o'zaro ta'sir qilish uchun drayverlar foydalanuvchi darajasidagi vazifalar shaklida mikroyadroning tepasida alohida amalga oshiriladi. Bunday vazifalarning mikroyadroda mavjud bo'lgan resurslarga kirishi qoidalarni aniqlash orqali tashkil etiladi.
Manba: opennet.ru