Kutshanje iindaba zavakala ukuba isindululo senziwe ukuba sibandakanywe ikernel ye Linux 5.20 (okanye mhlawumbi isebe liya kubalwa 6.0, konke kuxhomekeke kwisigqibo sikaLinus Torvalds ngenxa yezimvo zakhe azenzileyo kwiKernel 5.19 ukukhululwa).
Isindululo esenziwe simalunga iseti yeepetshi ngokuphunyezwa kwendlela yeRV (Ukuqinisekiswa kwexesha Lokusebenza), okuyindlela yokuqinisekisa ukusebenza okuchanekileyo kwiinkqubo ezithembeke kakhulu eziqinisekisa ukungabikho kokusilela.
ukuqinisekiswa kwenziwa ngexesha lokuqhuba ngokuncamathisela izibambi kwiindawo zomkhondo ezijonga eyona nkqubela-phambili yokwenziwa ngokuchasene nemodeli yesalathiso echazwe kwangaphambili ye-automaton emisela ukuziphatha okulindelekileyo kwenkqubo.
uMphuhlisi weLinux, UDaniel Bristot de Oliveira ukhankanya:
Kule minyaka imbalwa idlulileyo, bendiphonononga ukuba nokwenzeka kokuqinisekisa ukuziphatha kwe-Linux kernel usebenzisa i-Runtime Verification.
I-Runtime Verification (RV) yindlela ekhaphukhaphu (kodwa ingqongqo) ehambelana neendlela zokuqinisekisa ezipheleleyo (ezifana nokujonga imodeli kunye nokuqinisekisa i-theorem) kunye nendlela yokujongana nezandla kwiinkqubo ezinzima. Endaweni yokuxhomekeka kwimodeli eneenkcukacha yenkqubo (umzekelo, ukuzalisekiswa kwakhona kwenqanaba lomyalelo), i-VR isebenza ngokuhlalutya umkhondo wokwenziwa kwenkqubo, ithelekisa nenkcazo esesikweni yokuziphatha kwenkqubo.
Ukusetyenziswa kwe-automata ye-deterministic ye-VR yindlela esekelwe kakuhle. Kwimeko ethile ye-Linux kernel, unokufunda indlela yokuziphatha entsonkothileyo ye-Linux kernel ngeli nqaku:
uDe Oliveira, uDaniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Ukuqinisekiswa okusesikweni okusebenzayo kwi-Linux kernel.* Ku: Inkomfa yaMazwe ngaMazwe kubuNjineli beSoftware kunye neendlela ezisesikweni. Springer, Cham, 2019. p. 315-332.
Kwaye isebenza njani le ndlela apha:
uDe Oliveira, uDaniel B.; uDe Oliveira, uRomulo S.; Cucinotta, uTommaso. *Imodeli yongqamaniso lwentambo ye-PREEMPT_RT Linux kernel.* Ijenali yeNkqubo yoYilo lweZakhiwo, 2020, 107: 101729.
I-TLDR: Ukuziphatha okuntsonkothileyo kunokuqulunqwa ngendlela eyimodyuli, kunye ne-overhead eyamkelekileyo (kwanakwiinkqubo zokuvelisa).
Kuyakhankanywa ukuba ulwazi ngenqaku lomkhondo luhambisa imodeli ukusuka kwelinye ilizwe ukuya kwelinye, kwaye ukuba i-state entsha ayihambelani neeparameters zemodeli, isilumkiso senziwa okanye i-kernel ingena kwi-"panic" state (icinga ukuba iinkqubo ezithembekileyo kakhulu ziya kubhaqa kwaye ziphendule kwiimeko ezinjalo).
Imodeli ye-automaton ichaza uguqulo ukusuka kwelinye ilizwe ukuya kwelinye ithunyelwa ngaphandle kwifomathi "yechaphaza". (graphviz), emva koko iguqulelwe kusetyenziswa into eluncedo ye-dot2c kumboniso we-C, olayishwe ngokohlobo lwemodyuli yekernel elandelela ukunxaxha. ufezekiso olusuka kwimodeli echazwe kwangaphambili.
Ukujonga iimodeli ngexesha lokuqhuba kubekwe njengendlela elula kwaye elula ukuphumeza ukuqinisekisa ukuchaneka kokuphunyezwa kwiinkqubo zobuthunywa-ezibalulekileyo, ezincedisa iindlela zakudala zokuqinisekisa ukuthembeka, ezifana nokuqinisekiswa kwemodeli kunye nobungqina bemathematika bokuthotyelwa kwekhowudi kunye neenkcukacha ezinikwe ngolwimi olusesikweni.
Umlondolozi wenkqubo engaphantsi komkhondo uSteven Rostedt wayishwankathela ngolu hlobo:
» Olu lolona tshintsho lukhulu kwesi sicelo sokutsalwa. Yazisa isiqinisekiso sexesha lokuqhuba esifunekayo ukuze kuqhutywe iLinux kwiinkqubo ezibaluleke kakhulu zokhuseleko. Ivumela imodeli ye-automata ye-deterministic ukuba ifakwe kwi-kernel ukuba ifakwe kwii-tracepoints, apho ulwazi malunga nala ma-tracepoints luya kuhambisa imodeli ukusuka kwelinye ilizwe ukuya kwelinye.
Phakathi kweenzuzo ezikhankanyiweyo ze-RV kukukwazi ukubonelela ngokuqinisekiswa okungqongqo ngaphandle kokuphunyezwa okwahlukileyo kwenkqubo yonke ngolwimi lomzekelo, kunye nokuphendula okuguquguqukayo kwiziganeko ezingalindelekanga, umzekelo, ukuthintela ukusasazwa kokungaphumeleli kweenkqubo ezibalulekileyo.
Okokugqibela, ukuba unomdla wokwazi ngakumbi ngayo, ungajongana neenkcukacha kwi ukulandela ikhonkco.
Umthombo: https://www.phoronix.com/