De seL4 oppene Mikrokernelprojet huet den ACM Software System Award kritt, en alljährlechen Auszeechnung vun der Association for Computing Machinery (ACM), déi respektéiert international Organisatioun am Beräich vun de Computersystemer. De Präis gëtt fir Leeschtungen am Beräich vun der mathematescher Beweis vun der Operatioun ausgezeechent, wat d'voll Konformitéit mat de Spezifikatioune an enger formeller Sprooch uginn an d'Bereetschaft fir d'Benotzung a missionskritesch Uwendungen unerkennt. De seL4-Projet huet gewisen datt et net nëmme méiglech ass, d'Zouverlässegkeet an d'Sécherheet fir Projeten um Niveau vun den industriellen Betribssystemer voll formell z'iwwerpréiwen, awer och dëst z'erreechen ouni d'Leeschtung an d'Vielfalt ze Affer.
Den ACM Software System Award gëtt all Joer iwwerreecht fir d'Entwécklung vu Software Systemer z'erkennen, déi e definéierende Impakt op d'Industrie haten, nei Konzepter aféieren oder nei kommerziell Uwendungen opmaachen. De Betrag vum Präis ass 35 dausend US Dollar. An de leschte Joeren sinn ACM Auszeechnunge fir d'GCC an LLVM Projete ginn, an hir Grënner Richard Stallman a Chris Latner. Aner Projeten an Technologien déi och ausgezeechent goufen waren UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB an Eclipse .
D'Architektur vum seL4 Mikrokernel ass bemierkenswäert fir d'Entfernung vun Deeler fir d'Gestioun vun de Kernelressourcen am Benotzerraum a fir d'selwescht Mëttele fir Zougangskontrolle fir sou Ressourcen ze benotzen wéi fir Benotzerressourcen. De Mikrokernel bitt keng out-of-the-box High-level Abstraktioune fir d'Gestioun vun Dateien, Prozesser, Netzwierkverbindungen an dergläiche, amplaz bitt et nëmme minimal Mechanismen fir den Zougang zum kierperlechen Adressraum, Ënnerbriechungen a Prozessorressourcen ze kontrolléieren. Héichniveau Abstraktiounen a Chauffeuren fir mat Hardware interagéieren ginn separat uewen um Mikrokernel a Form vun User-Niveau Aufgaben ëmgesat. Den Zougang vun esou Aufgaben op d'Ressourcen, déi dem Mikrokernel verfügbar sinn, gëtt duerch d'Definitioun vu Regelen organiséiert.
Source: opennet.ru