La projekto evoluiganta la malferman seL4-mikrokernon ricevis la ACM Software System Award, aljuĝitan ĉiujare fare de la Association for Computing Machinery (ACM), la plej aŭtoritata internacia organizo en la kampo de komputilsistemoj. La premio estas aljuĝita por atingoj en la kampo de matematika pruvo de fidindeco de operacio, kiu pruvas plenan konformecon kun specifoj specifitaj en formala lingvo kaj rekonas pretecon por uzo en misi-kritikaj aplikoj. La projekto seL4 montris, ke estas ne nur eble plene formale kontroli fidindecon kaj sekurecon por industriaj operaciumaj nivelaj dezajnoj, sed ankaŭ atingi ĉi tion sen kompromiti rendimenton kaj ĉiuflankecon.
La ACM Software System Award estas prezentita ĉiujare por rekoni la evoluon de softvarsistemoj kiuj havis difinan efikon al la industrio, lanĉante novajn konceptojn aŭ malfermante novajn areojn de komerca apliko. La kvanto de la premio estas 35 mil usonaj dolaroj. En pasintaj jaroj, ACM-premioj estis aljuĝitaj al la projektoj GCC kaj LLVM, kaj iliaj fondintoj Richard Stallman kaj Chris Latner. La premio ankaŭ rekonis tiajn projektojn kaj teknologiojn kiel UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB kaj Eclipse .
La mikrokerna arkitekturo seL4 estas rimarkinda pro movi partojn por administrado de kernresursoj en uzantspacon kaj uzado de la samaj alirkontroliloj por tiaj resursoj kiel por uzantresursoj. La mikrokerno ne disponigas pretajn altnivelajn abstraktaĵojn por administrado de dosieroj, procezoj, retkonektoj, kaj similaĵo; anstataŭe, ĝi disponigas nur minimumajn mekanismojn por kontrolado de aliro al fizika adresspaco, interrompoj, kaj procesorresursoj. Altnivelaj abstraktaĵoj kaj ŝoforoj por interagado kun aparataro estas efektivigitaj aparte aldone al la mikrokerno en la formo de uzant-nivelaj taskoj. Aliro de tiaj taskoj al la rimedoj disponeblaj al la mikrokerno estas organizita per la difino de reguloj.
fonto: opennet.ru