Isiseko seRISC-V sibhengeze ukuba singqinisisile isebenza njani i-microkernel seL4 kwiinkqubo ezine iseti yoyilo loyilo I-RISC-V. Apho inkqubo yokuqinisekiswa incitshisiwe kubungqina bemathematika bokuthembeka kwe-seL4, ebonisa ukuthotyelwa ngokupheleleyo kwemigaqo echazwe kulwimi olusesikweni.
Ukuvavanywa kokunyaniseka kwenza ukuba i-seL4 isetyenziswe kwiinkqubo eziphambili ze-RISC-V RV64, efuna inqanaba eliphezulu lokuthembeka kwaye akuqinisekisi ukusilela.
Abaphuhlisi besoftware abasebenza ngaphezulu kwe-seL4 kernel banokuqiniseka ngokupheleleyo ukuba kwimeko yokusilela kwinxalenye enye yenkqubo, ukusilela akuyi kusasazeka kuyo yonke le nkqubo kwaye, ngakumbi, kwiindawo zayo ezibalulekileyo. .
Malunga ne-seL4
Uyilo lwe-seL4 kuyaphawuleka ngokususa iindawo zokulawula izixhobo ze-kernel kwindawo yomsebenzisi kwaye usebenzise iindlela ezifanayo zolawulo lokufikelela kwezixhobo ezinje ngezixhobo zomsebenzisi.
Imakethi encinci ayiboneleli ngokukhutshwa kwinqanaba eliphezulu sele ilungiselelwe ukulawula iifayile, iinkqubo, uqhagamshelo lwenethiwekhi, njl., Kodwa endaweni yoko ibonelela kuphela ngeendlela ezincinci zokulawula ukufikelela kwindawo yendawo yedilesi, ukuphazamisa kunye nezixhobo zeprosesa.
Amanqanaba aphezulu okutsala kunye nabalawuli bokunxibelelana nekhompyuter baphunyezwa ngokwahlukeneyo ngaphezulu kwe-microkernel ngohlobo lwemisebenzi eyenziwa kwinqanaba lomsebenzisi.
Ukufikelela kwemisebenzi enjalo kwimithombo ekhoyo kwi-microkernel kulungelelaniswe ngokuchazwa kwemithetho.
I-RISC-V ibonelela ngenkqubo evulekileyo neguqukayo yemiyalelo yomatshini leyo ivumela ukwenza ii-microprocessors kwizicelo ezingahambelaniyo, ngaphandle kokufuna ukuncitshiswa kwaye ngaphandle kokubeka iimeko zokusetyenziswa.
I-RISC-V ikuvumela ukuba wenze iiprosesa ezivulekileyo ngokupheleleyo kunye nee-SoCs. Okwangoku, ngokusekwe kwinkcazo ye-RISC-V, iinkampani ezininzi kunye noluntu oluphantsi kwamaphepha-mvume asimahla (i-BSD, i-MIT, i-Apache 2.0) iphuhlisa uninzi lwezinto ezahlukeneyo esele zivelisiwe ze-microprocessor cores, ii-SoCs kunye neetshipsi.
Inkxaso ye-RISC-V ijikeleze okoko kwaphuma i-Glibc 2.27, i-binutils 2.30, gcc 7, kunye ne-Linux 4.15 kernel.
Malunga novavanyo lwe-seL4 microkernel
Ekuqaleni, i-microkernel I-seL4 yaqinisekiswa ngeeprosesa ezingama-32-bit ARM, kwaye kamva kwiiprosesa ezingama-x86 ezingama-64.
Kuyajongwa ukuba indibaniselwano ye-RISC-V evulekileyo yoyilo lwehardware kunye ne-microkernel evulekileyo I-seL4 iya kufezekisa inqanaba elitsha lokhuseleko, njengoko izixhobo zehardware zangomso zinokuqinisekiswa ngokupheleleyo, ezingenakho ukufezekiswa kulwakhiwo lwezixhobo zekhompyutha.
Xa sijonga i-seL4, kufuneka sicinge ukuba izixhobo zekhompyuter zisebenza ngokufanelekileyo (Oko kukuthi, njengoko kuchaziwe). Oko kucinga ukuba kukho inkcazo engacacanga kwindawo yokuqala, leyo ayisiyiyo imeko yazo zonke izixhobo zekhompyutha.
Kodwa nangona olo lwazi lukhona, kwaye lusesikweni (Oko kukuthi, kulungiswa kwimathematika esesikweni exhasa ukuqiqa ngemathematika malunga neepropathi zayo), sazi njani ukuba iyayibamba indlela yokuziphatha kwentsimbi?
Inyani yile yokuba sinokuqiniseka ukuba ayisiyiyo. I-Hardware yahlukile kwisoftware kuba zombini ziyi-buggy.
Kodwa ukuba ne-ISA evulekileyo kunezibonelelo ezingaphaya kokungahlawulelwa. Inye kukuba ivumela ukuphunyezwa komthombo ovulekileyo wehardware.
Xa ujonga i-seL4, kucingelwa ukuba izixhobo zisebenza njengoko kubonisiwe kwaye inkcazo ichaza ngokupheleleyo indlela yokuziphatha kwenkqubo, kodwa enyanisweni izixhobo azinampazamo, nto leyo ibonakaliswe kakuhle ziingxaki ezivela rhoqo kwinkqubo yokuqikelela Imiyalelo.
Amaqonga evulekileyo ezinto zokwenza lula ukuhlanganiswa kotshintsho ezinxulumene nokhuselo, umzekelo, ukuvimba onke amajelo avuzayo ngamajelo omntu wesithathu, apho kusebenza ngakumbi ngakumbi ekupheliseni ingxaki ngesixhobo sehardware kunokuzama ukufumana isisombululo ngesoftware.
Okokugqibela, ukuba ufuna ukwazi ngakumbi ngayo, ungajonga kwinqaku ukulandela ikhonkco.
Kum, le processor yinto endibiza kakhulu. Ihlala kuphela inja etyebileyo yekhompyuter ukwenza ikhompyuter esinokuyithenga.
Umcimbi we-ARM yinto endicothayo, sele sikubonile okwenzekileyo ngeHuawei ngezohlwayo. Ndicacile ukuba i-RISC-V yam isisombululo esingcono kakhulu kuwo onke amanqanaba. Okwangoku uHuawei sele ebeke iliso kuyo kwaye mhlawumbi kwixa elizayo baya kuba nezixhobo kunye nale mic. Ukuba kunjalo, ngokuqinisekileyo kuya kubakho iinkampani ezininzi eziza kuyamkela kwaye kum oko kuya kuba kokufanelekileyo kwaye ngaphezulu kwako konke oko ii-distros zinika inkxaso hayi i-ARM kuphela njengoko kusenzeka kuninzi.
+ 10