RISC-V ya tabbatar da seL4 microkernel akan masu sarrafa RV64 ɗin su

Gidauniyar RISC-V ta sanar da cewa ta tabbatar yadda microkernel yake aiki seL4 a cikin tsarin tare da wa'azin kafa gine RISC-V. A cikin abin da tsarin tabbatarwa ya ragu zuwa tabbacin lissafi na amincin seL4, wanda ke nuna cikakkiyar bin takamaiman abubuwan da aka ƙayyade a cikin harshe na yau da kullun.

Gwajin dogaro yana ba da damar yin amfani da seL4 a cikin tsarin mahimmanci na manufa bisa ga masu sarrafa RISC-V RV64, wanda ke buƙatar matakin mafi girma na aminci kuma baya bada garantin gazawa.

Masu haɓaka software waɗanda ke gudana a saman kifin na seL4 na iya tabbata gaba ɗaya cewa idan har aka samu matsala a wani ɓangare na tsarin, wannan gazawar ba za ta yaɗu zuwa sauran tsarin ba kuma, musamman, zuwa ga mahimman sassanta.

Game da seL4

Tsarin seL4 sananne ne don cire sassa don sarrafa albarkatun kernel a sararin mai amfani kuma yi amfani da hanyoyin sarrafa hanyoyin shiga iri ɗaya don irin albarkatun kamar don albarkatun mai amfani.

Da microkernel ba ya samar da manyan abubuwa na zamani an riga an shirya don sarrafa fayiloli, aiwatarwa, haɗin hanyar sadarwa, da dai sauransu, amma a maimakon haka kawai yana samar da ƙananan ƙira don sarrafa damar zuwa sararin adireshin zahiri, katsewa, da sarrafa kayan aiki.

Ana aiwatar da manyan zane-zane da masu sarrafawa don hulɗa da kwamfutar daban a saman microkernel a cikin ayyukan ayyukan da aka yi a matakin mai amfani.

Samun damar irin waɗannan ayyukan ga albarkatun da ke cikin microkernel an tsara su ta hanyar ma'anar dokoki.

RISC-V yana ba da buɗaɗɗen tsari da sassauƙa na umarnin inji cewa yana ba da damar ƙirƙirar microprocessors don aikace-aikacen son zuciya, ba tare da buƙatar ragi ba kuma ba tare da sanya sharuɗɗan amfani ba.

RISC-V yana baka damar ƙirƙirar buɗe SoCs da masu sarrafawa. A halin yanzu, bisa ga takamaiman bayanin RISC-V, kamfanoni da al'ummomi da yawa a ƙarƙashin lasisi daban-daban na kyauta (BSD, MIT, Apache 2.0) suna haɓaka nau'ikan bambance-bambancen dozin da dama waɗanda aka riga aka samar da ƙwayoyin microprocessor, SoCs da kwakwalwan kwamfuta.

Tallafin RISC-V ya kasance tun fitowar Glibc 2.27, binutils 2.30, gcc 7, da Linux 4.15 kernel.

Game da gwajin microkernel na seL4

Da farko, microkernel seL4 an tabbatar dashi don masu sarrafa ARM 32-bitda kuma daga baya don x86 64-bit sarrafawa.

An lura cewa haɗuwa da RISC-V buɗe kayan haɗin gine tare da buɗe microkernel seL4 zai cimma sabon matakin tsaro, kamar yadda kayan aikin kayan gaba na gaba za a iya tabbatar da su sosai, wanda ba zai yuwu a cimma ba don tsarin mallakar kayan masarufi.

Lokacin da muka bincika seL4, dole ne mu ɗauka cewa kayan aikin suna aiki daidai (wato, kamar yadda aka ƙayyade). Wannan yana ɗauka akwai ƙayyadaddun bayanai a farkon, wanda ba haka bane ga duk kayan aikin. 

Amma koda lokacin da irin wannan takamaiman bayani ya kasance, kuma yana da tsari (ma'ana, tsafi ne a tsarin lissafi wanda yake tallafawa tunanin lissafi game da kaddarorin sa), ta yaya zamu san cewa a zahiri yana ɗaukar halayen kayan aikin? 

Gaskiyar ita ce, zamu iya tabbatar da cewa ba haka bane. Kayan aiki ba shi da banbanci da software ta yadda dukkansu suna da matsala.

Amma samun buɗe ISA yana da fa'idodi waɗanda suka wuce kasancewar ba ta da sarauta. Isaya shine cewa yana ba da izinin aiwatar da kayan aikin kayan buɗewa.

Lokacin bincika seL4, ana ɗauka cewa kayan aikin suna aiki kamar yadda aka nuna kuma ƙayyadadden bayanin cikakken tsarin halayyar tsarin, amma a zahiri kayan aikin ba ɓataccen kuskure bane, wanda aka nuna shi da kyau ta hanyar matsalolin da ke faruwa akai-akai a cikin tsarin aiwatar da hasashe Umarni.

Bude dandamali na kayan aiki yana sauƙaƙa haɗin canje-canje mai alaƙa da tsaro, alal misali, toshe duk hanyoyin da za su iya zubowa ta hanyar tashoshi na ɓangare na uku, inda ya fi dacewa don kawar da matsala ta kayan aiki fiye da ƙoƙarin nemo mafita ta hanyar software.

A ƙarshe, idan kuna son ƙarin sani game da shi, kuna iya tuntuɓar bayanin kula a cikin bin hanyar haɗi.