Projekti qĂ« zhvillon mikrothemelin e hapur seL4 fitoi çmimin ACM Software System Award, i cili jepet çdo vit nga Shoqata e KompjuterĂ«ve (ACM), organizata mĂ« autoritative ndĂ«rkombĂ«tare nĂ« fushĂ«n e sistemeve kompjuterike. Ămimi Ă«shtĂ« dhĂ«nĂ« pĂ«r arritjet nĂ« fushĂ«n e provimit matematikor tĂ« besueshmĂ«risĂ«, i cili dĂ«shmon pĂ«r pĂ«rputhshmĂ«rinĂ« e plotĂ« me specifikimet e caktuara nĂ« njĂ« gjuhĂ« formale dhe njihet pĂ«r gatishmĂ«rinĂ« e pĂ«rdorimit nĂ« aplikime kritike. Projekti seL4 ka treguar se Ă«shtĂ« e mundur jo vetĂ«m tĂ« kryhet njĂ« verifikim formal i plotĂ« i besueshmĂ«risĂ« dhe sigurisĂ« pĂ«r projekte tĂ« nivelit tĂ« sistemeve operative industriale, por gjithashtu tĂ« arrihet kjo pa kompromis nĂ« rendiment dhe shumĂ«anshmĂ«ri.
Ămimi ACM Software System Award jepet çdo vit pĂ«r zhvillimin e sistemeve software qĂ« kanĂ« njĂ« ndikim tĂ« rĂ«ndĂ«sishĂ«m nĂ« industri, duke sjellĂ« koncepte tĂ« reja ose duke zbuluar fusha tĂ« reja tĂ« aplikimit komercial. Vlera e çmimit Ă«shtĂ« 35 mijĂ« dollarĂ« amerikanĂ«. NĂ« vitet e kaluara, çmimi ACM Ă«shtĂ« dhĂ«nĂ« pĂ«r projekte si GCC dhe LLVM, si dhe pĂ«r themeluesit e tyre Richard Stallman dhe Chris Lattner. Ămimi gjithashtu ka nderuar 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 mikrogrimcës seL4 shquhet për ndarjen e pjesëve për menaxhimin e burimeve të kernels në hapësirën përdoruese dhe përdorimin e të njëjtave mjete ndarjeje për këto burime si për burimet përdoruese. Mikrogrimca nuk ofron abstraksione të gatshme me nivele të larta për menaxhimin e skedarëve, procedurave, lidhjeve rrjetore etj., por ofron vetëm mekanizma minimalë për menaxhimin e qasjes në hapësirën fizike adresuese, interruptet dhe burimet e procesorit. Abstraksionet e nivelit të lartë dhe drejtuesit për ndërveprimin me pajisjet realizohen veçmas mbi mikrogrimcë në formën e detyrave që ekzekutohen në nivelin përdorues. Qasja e këtyre detyrave në burimet ekzistuese të mikrogrimcës organizohet përmes përcaktimit të rregullave.
Burimi: opennet.ru
