Ang seL4 open microkernel project ay nakatanggap ng ACM Software System Award, isang taunang parangal na ibinibigay ng Association for Computing Machinery (ACM), ang pinakarespetadong internasyonal na organisasyon sa larangan ng mga computer system. Ang parangal ay ibinibigay para sa mga tagumpay sa larangan ng mathematical proof of operation, na nagpapahiwatig ng ganap na pagsunod sa mga pagtutukoy na ibinigay sa isang pormal na wika at kinikilala ang kahandaan para sa paggamit sa mga aplikasyong kritikal sa misyon. Ipinakita ng proyekto ng seL4 na hindi lamang posible na ganap na pormal na i-verify ang pagiging maaasahan at seguridad para sa mga proyekto sa antas ng mga pang-industriyang operating system, ngunit upang makamit din ito nang hindi isinasakripisyo ang pagganap at kakayahang magamit.
Ang ACM Software System Award ay itinatanghal taun-taon upang kilalanin ang pagbuo ng mga software system na nagkaroon ng tiyak na epekto sa industriya, pagpapakilala ng mga bagong konsepto o pagbubukas ng mga bagong komersyal na aplikasyon. Ang halaga ng award ay 35 thousand US dollars. Sa mga nakaraang taon, ang mga parangal ng ACM ay ibinigay sa mga proyekto ng GCC at LLVM, at ang kanilang mga tagapagtatag na sina Richard Stallman at Chris Latner. Ang iba pang mga proyekto at teknolohiya na ginawaran din ay ang UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB at eclipse .
Ang arkitektura ng microkernel seL4 ay kapansin-pansin para sa pag-alis ng mga bahagi para sa pamamahala ng mga mapagkukunan ng kernel sa espasyo ng gumagamit at para sa paglalapat ng parehong paraan ng kontrol sa pag-access para sa mga mapagkukunan tulad ng para sa mga mapagkukunan ng gumagamit. Ang microkernel ay hindi nagbibigay ng mga out-of-the-box na mataas na antas na abstraction para sa pamamahala ng mga file, proseso, koneksyon sa network, at mga katulad nito, sa halip ay nagbibigay lamang ito ng mga minimal na mekanismo para sa pagkontrol ng access sa pisikal na espasyo ng address, mga interrupt, at mga mapagkukunan ng processor. Ang mga high-level abstraction at driver para sa pakikipag-ugnayan sa hardware ay hiwalay na ipinapatupad sa ibabaw ng microkernel sa anyo ng mga gawain sa antas ng user. Ang pag-access ng naturang mga gawain sa mga mapagkukunang magagamit sa microkernel ay isinaayos sa pamamagitan ng kahulugan ng mga panuntunan.
Pinagmulan: opennet.ru