I-RISC-V Foundation imemezele ukuthi iqinisekisile ukusebenza kwe- seL4 microkernel ezinhlelweni ezinesakhiwo sesethi yemiyalelo ye -RISC-V . Inqubo yokuqinisekisa yehliswa yaba ubufakazi bezibalo bokuthembeka kwe-seL4, okubonisa ukuhambisana okugcwele nemininingwane echazwe olimini olusemthethweni.
Ukuhlolwa kokuthembeka kuvumela ukusetshenziswa kwe-seL4 ezinhlelweni ezibalulekile ezisekelwe kuma -processor e -RV64 RISC-V , adinga izinga eliphezulu lokuthembeka futhi akuqinisekisi 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
Ukwakheka kwe-seL4 kuyaphawuleka ngokususa izingxenye zokuphatha izinsiza ze-kernel esikhaleni somsebenzisi nokusebenzisa izindlela ezifanayo zokulawula ukufinyelela kwezinsiza ezifana nezezinsiza zomsebenzisi.
I-microkernel ayinikezi izifinyezo ezisezingeni eliphezulu ezenziwe ngomumo zokuphatha amafayela, izinqubo, ukuxhumana kwenethiwekhi, njll., kodwa inikeza izindlela ezincane zokulawula ukufinyelela esikhaleni sekheli elingokoqobo , ukuphazamiseka, kanye 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 lokufundisa lomshini oluvulekile noluguquguqukayo oluvumela ukudalwa kwama-microprocessors okusetshenziswa ngokungahleliwe, 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 -seL4 microkernel yaqinisekiswa kuma-processor e-ARM angu-32-bit , futhi kamuva kuma-processor angu-64-bit x86.
Kuyabonakala ukuthi ukuhlanganiswa kokwakheka kwehadiwe ye-RISC-V evulekile ne- microkernel ye-seL4 evulekile kuzofeza izinga elisha lokuphepha , njengoba izingxenye zehadiwe esikhathini esizayo nazo zingaqinisekiswa ngokugcwele, okuyinto engenakwenzeka ngezakhiwo zehadiwe ezizimele.
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 e-hardware avulekile enza kube lula ukuhlanganiswa kwezinguquko ezihlobene nokuphepha, isibonelo, ukuvimba zonke iziteshi ezivuzayo ezingaba khona ngeziteshi zenkampani yangaphandle, lapho kusebenza kahle kakhulu ukuqeda inkinga nge-hardware kunokuzama ukuthola izixazululo ngesofthiwe.
Okokugcina, uma ufuna ukwazi okwengeziwe ngakho, ungabheka lesi sihloko kusixhumanisi esilandelayo.