I-RISC-V iqinisekise i-seL4 microkernel kuzinqubo zabo ze-RV64

I-RISC-V Foundation imemezele ukuthi isiqinisekisile isebenza kanjani i-microkernel seL4 ezinhlelweni ezine- ukufundwa kusethwe ukwakhiwa I-RISC-V. Lapho inqubo yokuqinisekisa incishiselwa esivivinyweni sezibalo sokwethembeka kwe-seL4, okukhombisa ukuhambisana okuphelele nemininingwane ebalulwe ngolimi olusemthethweni.

Ukuhlolwa kokuthembeka kunika amandla i-seL4 ukuthi isetshenziswe ezinhlelweni ezibucayi zemishini ngokususelwa kuma-RISC-V processor RV64, edinga izinga eliphakeme lokuthembeka futhi engakuqinisekisi ukwehluleka.

Abathuthukisi beSoftware abasebenza ngaphezulu kwe-seL4 kernel bangaqiniseka ngokuphelele ukuthi uma kwenzeka kwehluleka engxenyeni eyodwa yohlelo, lokhu kwehluleka ngeke kusabalale kulo lonke uhlelo futhi, ikakhulukazi ezingxenyeni zalo ezibucayi.

Mayelana ne-seL4

Ukwakhiwa kwe-seL4 kuyaphawuleka ngokususa izingxenye ukuphatha izinsiza ze-kernel esikhaleni somsebenzisi futhi usebenzise izindlela ezifanayo zokulawula ukufinyelela kuzinsizakusebenza ezinjengezinsiza zomsebenzisi.

I-microkernel ayihlinzeki ngokukhishwa okuphezulu sekulungiselelwe ukuphatha amafayela, izinqubo, ukuxhumana kwenethiwekhi, njll inikeza kuphela izindlela ezincane zokulawula ukufinyelela esikhaleni sekheli lendawo, iyaphazamisa, nezinsizakusebenza zeprosesa.

Ukukhishwa kwezinga eliphakeme kanye nabalawuli bokuxhumana nekhompyutha kufakwa ngokuhlukile ngaphezulu kwe-microkernel ngendlela yemisebenzi eyenziwa ezingeni lomsebenzisi.

Ukutholakala kwemisebenzi enjalo ezinsizakalweni ezitholakala ku-microkernel kuhlelwe ngokuchazwa kwemithetho.

I-RISC-V inikeza uhlelo oluvulekile futhi oluguquguqukayo yemiyalo yomshini ukuthi ivumela ukudala ama-microprocessors ezinhlelo zokusebenza ezingqubuzanayo, ngaphandle kokudinga ukuncishiswa futhi ngaphandle kokubeka imibandela yokusetshenziswa.

I-RISC-V ikuvumela ukuthi udale amaprosesa avuleke ngokuphelele nama-SoCs. Njengamanje, ngesisekelo sokucaciswa kwe-RISC-V, izinkampani eziningana nemiphakathi engaphansi kwamalayisense ahlukahlukene amahhala (i-BSD, i-MIT, i-Apache 2.0) ithuthukisa izinhlobonhlobo eziyishumi nambili zama-microprocessor cores asevele akhiqiziwe, ama-SoC nama-chips.

Ukuxhaswa kwe-RISC-V bekukhona selokhu kwakhululwa i-Glibc 2.27, i-binutils 2.30, i-gcc 7, ne-Linux 4.15 kernel.

Mayelana nokuhlolwa kwe-seL4 microkernel

Ekuqaleni, i-microkernel I-seL4 iqinisekiswe ngama-processor angama-32-bit ARM, futhi ngokuhamba kwesikhathi kuma-processor we-x86 64-bit.

Kuyabonakala ukuthi inhlanganisela yokwakhiwa kwehadiwe evulekile ye-RISC-V ne-microkernel evulekile I-seL4 izofinyelela ezingeni elisha lokuphephanjengoba izingxenye zehadiwe esikhathini esizayo nazo zingaqinisekiswa ngokuphelele, okungenakwenzeka ukufeza ukwakheka kwezingxenyekazi zekhompiyutha.

Lapho sihlola i-seL4, kufanele sicabange ukuthi i-hardware isebenza kahle (okungukuthi, njengoba kuchaziwe). Lokho kucabanga ukuthi kunencazelo engaqondakali kwasekuqaleni, okungeyona eyayo yonke i-hardware. 

Kepha noma ngabe ukucaciswa okunjalo kukhona, futhi kusemthethweni (okusho ukuthi, kulungiswa kuhlelo lwezibalo olusekela ukucabanga ngezibalo mayelana nezakhiwo zalo), sazi kanjani ukuthi empeleni kuthola ukusebenza kwehadiwe? 

Iqiniso ukuthi singaqiniseka impela ukuthi akunjalo. Izingxenyekazi zekhompuyutha azihlukile kusoftware ngoba zombili ziyi-buggy.

Kepha ukuba ne-ISA evulekile kunezinzuzo ezingaphezulu kokungabi namali yasebukhosini. Enye ukuthi ivumela ukusetshenziswa komthombo ovulekile wehadiwe.

Lapho ubheka i-seL4, kucatshangwa ukuthi okokusebenza kusebenza njengoba kukhonjisiwe futhi imininingwane ichaza ngokuphelele ukusebenza kohlelo, kepha empeleni okokusebenza akulona iphutha, okukhonjiswa kahle ngezinkinga eziqubuka njalo emshinini wokuqagela Imiyalelo .

Amapulatifomu evulekile e-Hardware enza lula ukuhlanganiswa kwezinguquko okuhlobene nezokuphepha, ngokwesibonelo, ukuvimba zonke iziteshi ezivuzayo ngeziteshi ezivela eceleni, lapho kusebenza khona kangcono ukuqeda inkinga ngehadiwe kunokuzama ukuthola izixazululo nge-software.

Ekugcineni, uma ufuna ukwazi kabanzi ngayo, ungaxhumana nenothi ku- isixhumanisi esilandelayo.