Weqfa RISC-V di derbarê verastkirina xebata mîkrokernelê de li ser pergalên bi mîmariya set talîmatên RISC-V. Verification tê xwarê pêbaweriya operasyona seL4, ku lihevhatina tevahî bi taybetmendiyên ku di zimanê fermî de hatine destnîşan kirin destnîşan dike. Delîlên pêbaweriyê seL4 di pergalên mîsyonê-krîtîk ên li ser pêvajoyên RISC-V RV64-ê de ku hewceyê astek zêde pêbaweriyê hewce dike û nebûna têkçûn garantî dike. Pêşdebirên nermalava ku li ser kernel seL4 dixebitin dikarin bi tevahî pê ewle bin ku heke di perçeyek pergalê de têkçûnek hebe, ev têkçûn dê li pergalên mayî û, bi taybetî, beşên wê yên krîtîk belav nebe.
Mîkrokernelê seL4 di destpêkê de ji bo pêvajoyên ARM-ê yên 32-bit, û paşê ji bo pêvajoyên 64-bit x86 hate verast kirin. Tê destnîşan kirin ku berhevoka mîmariya hişk a vekirî RISC-V bi mîkrokernelê vekirî ya seL4 re dê astek nû ya ewlehiyê bi dest bixe, ji ber ku hêmanên hardware di pêşerojê de jî bi tevahî têne verast kirin, ku ne gengaz e ku meriv ji bo mîmariyên hardware yên xwedan bigihîje.
Dema ku seL4 verast dike, tê texmîn kirin ku alav wekî ku hatî destnîşan kirin dixebite û taybetmendî bi tevahî tevgera pergalê vedibêje, lê di rastiyê de amûr ji xeletiyan ne bêpar e, ku ev yek ji hêla pirsgirêkên bi rêkûpêk ve di mekanîzmaya darvekirina spekulatîf de bi zelalî tê destnîşan kirin. talîmatên. Platformên hardware yên vekirî entegrekirina guheztinên têkildar ên ewlehiyê hêsantir dike - mînakî, astengkirina hemî lehiyên kanalên alîgir ên gengaz, li cihê ku jêbirina pirsgirêkê di hardware de ji hewildana dîtina rêgezên nermalavê pir bikêrtir e.
Bînin bîra xwe ku mîmariya seL4 parçeyên diherikin ji bo birêvebirina çavkaniyên kernelê li cîhê bikarhêner û sepandina heman wateyên kontrolkirina gihîştinê ji bo çavkaniyên weha yên wekî çavkaniyên bikarhêner. Mîkrokernel ji bo birêvebirina pelan, pêvajoyan, girêdanên torê, û yên wekî wan, ji bo birêvebirina pelan, pêvajoyan, girêdanên torê û yên wekî wan, abstraksyonên amade-asta bilind peyda nake; di şûna wê de, ew tenê mekanîzmayên hindiktirîn ji bo kontrolkirina gihîştina cîhê navnîşana laşî, navber û çavkaniyên pêvajoyê peyda dike. Abstractions-asta bilind û ajokarên ji bo danûstendina bi hardware-ê re di forma karên asta bikarhêner de li ser mîkrokernelê veqetandî têne bicîh kirin. Gihîştina peywirên weha ji çavkaniyên ku ji mîkrokernelê re peyda dibin bi pênasekirina qaîdeyan têne organîze kirin.
RISC-V pergalek rêwerziya makîneya vekirî û maqûl peyda dike ku destûrê dide mîkroprosesoran ku ji bo serîlêdanên kêfî werin çêkirin bêyî ku pêdivî bi xêzan an rêzikên pêvekirî bi kar bîne. RISC-V dihêle hûn SoC û pêvajoyên bi tevahî vekirî biafirînin. Naha li ser bingeha taybetmendiya RISC-V ji hêla pargîdan û civakên cûda ve di bin lîsansên cûda yên belaş de (BSD, MIT, Apache 2.0) bi dehan guhertoyên korên mîkroprosesor, SoC û çîpên berê hatine hilberandin. Piştgiriya RISC-V ji ber berdana Glibc 2.27, binutils 2.30, gcc 7, û kernel Linux 4.15 ve heye.
Source: opennet.ru