SeL4 microkernel jẹ ijẹrisi mathematiki fun faaji RISC-V

RISC-V Foundation royin nipa a mọ daju awọn isẹ ti awọn microkernel seL4 lori awọn ọna šiše pẹlu RISC-V ilana ṣeto faaji. Ijerisi wa si isalẹ lati ẹri mathematiki Igbẹkẹle ti iṣẹ seL4, eyiti o tọka ibamu ni kikun pẹlu awọn pato ti a sọ pato ninu ede deede. Ẹri ti igbẹkẹle faye gba o lati lo seL4 ni awọn ọna ṣiṣe pataki-pataki ti o da lori awọn ilana RISC-V RV64 ti o nilo ipele ti igbẹkẹle ti o pọ si ati iṣeduro isansa ti awọn ikuna. Awọn olupilẹṣẹ ti sọfitiwia nṣiṣẹ lori oke ekuro seL4 le ni igboya patapata pe ti ikuna ba wa ni apakan kan ti eto naa, ikuna yii kii yoo tan si iyoku eto naa ati, ni pataki, awọn ẹya pataki rẹ.

SeL4 microkernel jẹ iṣeduro lakoko fun awọn ilana ARM 32-bit, ati nigbamii fun awọn ilana 64-bit x86. O ṣe akiyesi pe apapọ ti faaji ohun elo RISC-V ṣiṣi pẹlu microkernel seL4 ṣii yoo ṣaṣeyọri ipele aabo tuntun, nitori awọn paati ohun elo tun le rii daju ni kikun ni ọjọ iwaju, eyiti ko ṣee ṣe lati ṣaṣeyọri fun awọn ayaworan ohun elo ohun-ini.

Nigbati o ba rii daju seL4, o ro pe ohun elo naa ṣiṣẹ bi a ti sọ ati pe sipesifikesonu ṣe apejuwe ihuwasi ti eto naa ni kikun, ṣugbọn ni otitọ ohun elo naa ko ni ominira lati awọn aṣiṣe, eyiti o jẹ afihan ni gbangba nipasẹ awọn iṣoro ti o nwaye nigbagbogbo ni siseto ti ipaniyan akiyesi ti ilana. Ṣii awọn iru ẹrọ ohun elo jẹ ki o rọrun lati ṣepọ awọn ayipada ti o ni ibatan si aabo - fun apẹẹrẹ, lati dènà gbogbo awọn n jo ikanni-ẹgbẹ ti o ṣeeṣe, nibiti o ti munadoko diẹ sii lati yọ iṣoro naa kuro ninu ohun elo ju lati gbiyanju lati wa awọn agbegbe iṣẹ ni sọfitiwia.

Ranti wipe seL4 faaji lokiki gbigbe awọn ẹya fun iṣakoso awọn orisun kernel sinu aaye olumulo ati lilo awọn ọna iṣakoso iwọle kanna fun iru awọn orisun bi fun awọn orisun olumulo. Microkernel ko pese awọn abstractions ipele ti o ti ṣetan fun ṣiṣakoso awọn faili, awọn ilana, awọn asopọ nẹtiwọọki, ati bii; dipo, o pese awọn ọna ṣiṣe to kere nikan fun iṣakoso iraye si aaye adirẹsi ti ara, awọn idilọwọ, ati awọn orisun ero isise. Awọn abstractions ipele giga ati awọn awakọ fun ibaraenisepo pẹlu ohun elo jẹ imuse lọtọ lori oke microkernel ni irisi awọn iṣẹ-ṣiṣe ipele olumulo. Wiwọle ti iru awọn iṣẹ-ṣiṣe si awọn orisun ti o wa si microkernel ti ṣeto nipasẹ itumọ awọn ofin.

RISC-V n pese eto itọnisọna ẹrọ ṣiṣi ati rọ ti o fun laaye microprocessors lati kọ fun awọn ohun elo lainidii laisi nilo awọn ẹtọ ọba tabi awọn okun ti a so lati lo. RISC-V gba ọ laaye lati ṣẹda awọn SoCs ti o ṣii patapata ati awọn ilana. Lọwọlọwọ da lori sipesifikesonu RISC-V nipasẹ awọn ile-iṣẹ oriṣiriṣi ati agbegbe labẹ ọpọlọpọ awọn iwe-aṣẹ ọfẹ (BSD, MIT, Apache 2.0) ndagba orisirisi awọn mejila aba ti microprocessor ohun kohun, SoCs ati tẹlẹ produced awọn eerun. Atilẹyin RISC-V ti wa lati awọn idasilẹ ti Glibc 2.27, binutils 2.30, gcc 7, ati ekuro Linux 4.15.

orisun: opennet.ru

Fi ọrọìwòye kun