Mashruuca microkernel-ka furan ee seL4 waxa uu helay Abaalmarinta Nidaamka Software-ka ee ACM, abaal-marin sannadle ah oo ay bixiso Ururka Mashiinnada Xisaabinta (ACM), oo ah hay'adda caalamiga ah ee aadka loo ixtiraamo ee dhinaca nidaamyada kombiyuutarada. Abaalmarinta waxaa la siiyaa guulaha laga gaaray goobta caddaynta xisaabeed ee hawlgalka, taas oo muujinaysa u hoggaansanaanta buuxda ee qeexitaannada lagu bixiyo luqadda rasmiga ah oo aqoonsa u diyaargarowga isticmaalka codsiyada muhimka ah. Mashruuca seL4 waxa uu muujiyay in aanay suurtogal ahayn oo keliya in si buuxda loo xaqiijiyo isku halaynta iyo ammaanka mashaariicda heerka nidaamyada hawlgalka warshadaha, laakiin sidoo kale si loo gaaro tan iyada oo aan la hurin waxqabadka iyo wax-qabadka.
Abaalmarinta Nidaamka Software-ka ee ACM waxaa la soo bandhigaa sanad walba si loo aqoonsado horumarinta nidaamyada software ee saameyn qeexan ku yeeshay warshadaha, soo bandhigida fikrado cusub ama furitaanka codsiyo ganacsi oo cusub. Qadarka abaal-marintu waa 35 kun oo dollarka Maraykanka ah. Sanadihii la soo dhaafay, abaal-marinaha ACM waxaa la siiyay mashaariicda GCC iyo LLVM, iyo aasaasayaashooda Richard Stallman iyo Chris Latner. Mashaariicda kale iyo teknoolojiyadda sidoo kale la bixiyay ayaa kala ahaa UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB iyo madoobaad. .
Nashqadaynta microkernel-ka seL4 waxa ay caan ku tahay ka-saarista qaybaha lagu maamulayo ilaha kernel-ka ee goobta isticmaalaha iyo in la adeegsado hab la mid ah oo lagu xakameynayo agabka sida ilaha isticmaalaha. Microkernel-ku ma bixiyo ka-baxsan-sanduuqa-soo-saarka heer-sare ee maaraynta faylalka, hababka, isku xirka shabakadaha, iyo wixii la mid ah, taa beddelkeeda waxay bixisaa kaliya hababka ugu yar ee lagu xakameynayo gelitaanka goobta ciwaanka jireed, carqaladaynta, iyo ilaha processor-ka. Aabstractions heer sare ah iyo darawalada la falgalka qalabka waxaa si gooni gooni ah loo hirgeliyaa korka microkernel-ka qaab hawlo heerka user. Helitaanka hawlahan oo kale ee kheyraadka ay heli karaan microkernel-ka waxaa lagu habeeyaa qeexida xeerarka.
Source: opennet.ru