Projekti qĂ« zhvillon mikrokernelin e hapur seL4 ka marrĂ« çmimin ACM Software System Award, i cili jepet çdo vit nga Association for Computing Machinery (ACM), organizata ndĂ«rkombĂ«tare mĂ« autoritare nĂ« fushĂ«n e sistemeve kompjuterike. Ămimi Ă«shtĂ« dhĂ«nĂ« pĂ«r arritjet nĂ« fushĂ«n e provĂ«s matematikore tĂ« besueshmĂ«risĂ« sĂ« funksionimit, e cila vĂ«rteton pĂ«rputhjen e plotĂ« me specifikimet e pĂ«rcaktuara nĂ« gjuhĂ« formale dhe konfirmon gatishmĂ«rinĂ« pĂ«r pĂ«rdorim nĂ« skenarĂ« kritikĂ«. Projekti seL4 tregoi se Ă«shtĂ« e mundur jo vetĂ«m tĂ« kryhet verifikim formal i plotĂ« i besueshmĂ«risĂ« dhe sigurisĂ« pĂ«r projekte tĂ« nivelit tĂ« sistemeve operative industriale, por edhe tĂ« arrihet kjo pa kompromentuar performancĂ«n dhe universalitetin.
Ămimi ACM Software System Award jepet çdo vit pĂ«r zhvillimin e sistemeve softuerike qĂ« kanĂ« pasur ndikim pĂ«rcaktues nĂ« industri, duke sjellĂ« koncepte tĂ« reja nĂ« pĂ«rdorim ose duke hapur fusha tĂ« reja tĂ« zbatimit komercial. Vlera e çmimit Ă«shtĂ« 35 mijĂ« dollarĂ« amerikanĂ«. NĂ« vitet e mĂ«parshme, çmimet ACM u janĂ« dhĂ«nĂ« projekteve GCC dhe LLVM, si edhe themeluesve tĂ« tyre Richard Stallman dhe Chris Lattner. Me kĂ«tĂ« çmim janĂ« vlerĂ«suar gjithashtu projekte dhe teknologji si UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB dhe Eclipse.
Arkitektura e mikrokernelit seL4 dallohet për zhvendosjen e pjesëve të menaxhimit të burimeve të kernelit në hapësirën e përdoruesit dhe për përdorimin e të njëjtave mekanizma të kontrollit të aksesit për këto burime si për burimet e përdoruesit. Mikrokerneli nuk ofron abstraksione të gatshme të nivelit të lartë për menaxhimin e skedarëve, proceseve, lidhjeve të rrjetit etj.; në vend të kësaj, ai ofron vetëm mekanizmat minimalë për menaxhimin e aksesit në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraksionet e nivelit të lartë dhe drajverët për ndërveprim me pajisjet implementohen veçmas mbi mikrokernelin në formën e detyrave që ekzekutohen në nivel përdoruesi. Aksesi i këtyre detyrave te burimet që mikrokerneli ka në dispozicion organizohet përmes përcaktimit të rregullave.
Burimi: opennet.ru
