Բաց seL4 միկրոմիջուկը մշակող նախագիծը ստացել է ACM Software System Award մրցանակը, որը ամեն տարի շնորհվում է Համակարգչային համակարգերի ոլորտում ամենահեղինակավոր միջազգային կազմակերպության կողմից՝ ACM-ի կողմից: Մրցանակը շնորհվում է շահագործման հուսալիության մաթեմատիկական ապացուցման ոլորտում ձեռքբերումների համար, որը ցույց է տալիս պաշտոնական լեզվով սահմանված տեխնիկական պայմանների ամբողջական համապատասխանությունը և ճանաչում է առաքելության կարևորագույն ծրագրերում օգտագործման պատրաստակամությունը: SeL4 նախագիծը ցույց է տվել, որ ոչ միայն հնարավոր է լիովին պաշտոնապես ստուգել հուսալիությունը և անվտանգությունը արդյունաբերական օպերացիոն համակարգի մակարդակի նախագծման համար, այլ նաև հասնել դրան՝ առանց կատարողականության և բազմակողմանի խախտման:
ACM Software System Award մրցանակը շնորհվում է ամեն տարի՝ ճանաչելու ծրագրային համակարգերի զարգացումը, որոնք որոշիչ ազդեցություն են ունեցել արդյունաբերության վրա՝ ներդնելով նոր հայեցակարգեր կամ բացելով առևտրային կիրառման նոր ոլորտներ: Մրցանակի գումարը կազմում է 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 միկրոմիջուկի ճարտարապետությունը հատկանշական է շարժվող մասերի համար՝ միջուկի ռեսուրսները օգտագործողի տարածք կառավարելու և այնպիսի ռեսուրսների համար մուտքի վերահսկման նույն գործիքների օգտագործման համար, ինչ օգտագործողի ռեսուրսների համար: Միկրոմիջուկը չի տրամադրում պատրաստի բարձր մակարդակի աբստրակցիաներ ֆայլերի, պրոցեսների, ցանցային կապերի և այլնի կառավարման համար, փոխարենը տրամադրում է միայն նվազագույն մեխանիզմներ ֆիզիկական հասցեների տարածության, ընդհատումների և պրոցեսորի ռեսուրսների հասանելիությունը վերահսկելու համար: Բարձր մակարդակի աբստրակցիաները և սարքավորումների հետ փոխազդեցության դրայվերներն իրականացվում են առանձին միկրոմիջուկի վերևում՝ օգտագործողի մակարդակի առաջադրանքների տեսքով: Նման առաջադրանքների հասանելիությունը միկրոմիջուկին հասանելի ռեսուրսներին կազմակերպվում է կանոնների սահմանման միջոցով:
Source: opennet.ru