Pwojè a devlope microkernel seL4 louvri a te resevwa ACM Software System Award, akòde chak ane pa Asosyasyon an pou machin enfòmatik (ACM), òganizasyon entènasyonal ki pi autorité nan domèn sistèm òdinatè. Yo bay pri a pou reyalizasyon nan domèn matematik prèv fyab nan operasyon, ki demontre konfòmite konplè ak espesifikasyon ki espesifye nan yon langaj fòmèl epi rekonèt preparasyon pou itilize nan aplikasyon misyon kritik. Pwojè seL4 la te montre ke li pa sèlman posib pou verifye konplètman fòmèlman fyab ak sekirite pou konsepsyon sistèm opere endistriyèl nan nivo, men tou, reyalize sa san sakrifye pèfòmans oswa adaptabilite.
ACM Software System Award yo prezante chak ane pou rekonèt devlopman nan sistèm lojisyèl ki te gen yon enpak defini sou endistri a, entwodwi nouvo konsèp oswa louvri nouvo zòn nan aplikasyon komèsyal yo. Kantite prim lan se 35 mil dola ameriken. Nan ane ki sot pase yo, yo te bay prim ACM pou pwojè GCC ak LLVM, ak fondatè yo Richard Stallman ak Chris Latner. Prim lan te rekonèt pwojè ak teknoloji tankou UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ak Eclipse. .
Achitekti microkernel seL4 remakab pou deplase pati pou jere resous nwayo nan espas itilizatè yo epi sèvi ak menm zouti kontwòl aksè pou resous sa yo tankou pou resous itilizatè yo. Mikrokernel la pa bay abstraksyon wo nivo pare pou jere fichye, pwosesis, koneksyon rezo, ak lòt bagay konsa, li bay sèlman mekanis minim pou kontwole aksè nan espas adrès fizik, entèwonp, ak resous processeur. Abstraksyon wo nivo ak chofè pou kominike avèk pyès ki nan konpitè yo aplike separeman sou tèt mikrokernel la nan fòm travay nan nivo itilizatè. Aksè travay sa yo nan resous ki disponib nan mikrokernel la òganize atravè definisyon règ yo.
Sous: opennet.ru
