Aikin bude microkernel na seL4 ya sami lambar yabo ta ACM Software System Award, lambar yabo ta shekara-shekara da Ƙungiyar Ƙwaƙwalwar Ƙwaƙwalwa (ACM) ke bayarwa, ƙungiyar kasa da kasa da aka fi girmamawa a fannin tsarin kwamfuta. An ba da lambar yabo don nasarori a fagen shaidar aikin lissafi, wanda ke nuna cikakken yarda da ƙayyadaddun bayanai da aka bayar a cikin yare na yau da kullun kuma ya gane shirye-shiryen amfani da aikace-aikacen manufa. Aikin seL4 ya nuna cewa ba zai yiwu ba ne kawai don tabbatar da cikakken tabbaci da aminci ga ayyuka a matakin tsarin aiki na masana'antu, amma har ma don cimma wannan ba tare da sadaukar da aiki da haɓaka ba.
Ana ba da lambar yabo ta ACM Software System Award kowace shekara don gane haɓakar tsarin software waɗanda ke da tasiri mai ma'ana akan masana'antu, gabatar da sabbin dabaru ko buɗe sabbin aikace-aikacen kasuwanci. Adadin kyautar dalar Amurka dubu 35 ne. A cikin shekarun da suka gabata, an ba da kyaututtukan ACM ga ayyukan GCC da LLVM, da waɗanda suka kafa su Richard Stallman da Chris Latner. Sauran ayyuka da fasahohin da aka ba da su sune UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB da eclipse .
Gine-gine na microkernel seL4 sananne ne don cire sassa don sarrafa albarkatun kwaya a cikin sararin mai amfani da kuma amfani da hanyoyin sarrafa dama don irin albarkatun kamar na albarkatun mai amfani. Microkernel baya samar da babban matakin abstractions na waje don sarrafa fayiloli, matakai, haɗin yanar gizo, da makamantansu, a maimakon haka yana samar da ƙananan hanyoyi don sarrafa damar shiga sararin adireshin jiki, katsewa, da albarkatun sarrafawa. Ana aiwatar da abstractions masu girma da direbobi don yin hulɗa tare da kayan aiki daban a saman microkernel a cikin nau'ikan ayyuka masu amfani. Samun damar irin waɗannan ayyuka zuwa albarkatun da ke samuwa ga microkernel an tsara su ta hanyar ma'anar dokoki.
source: budenet.ru