Aron maapil sa Linux 5.20 kernel (tingali ang sanga maihap nga 6.0), usa ka hugpong sa mga patch ang gisugyot sa pagpatuman sa RV (Runtime Verification) nga mekanismo, nga usa ka paagi sa pagsusi sa husto nga operasyon sa kasaligan kaayo nga mga sistema. nga naggarantiya sa pagkawala sa mga kapakyasan. Ang validation gihimo sa runtime pinaagi sa pag-attach sa mga handler sa mga tracepoints nga nagsusi sa aktuwal nga pag-uswag sa pagpatuman batok sa usa ka gitino nang daan nga reference deterministic nga modelo sa automat nga nagtino sa gipaabot nga kinaiya sa sistema.
Ang impormasyon gikan sa mga tracepoint nagpalihok sa modelo gikan sa usa ka estado ngadto sa lain, ug kung ang bag-ong estado dili motakdo sa mga parameter sa modelo, usa ka pasidaan ang mamugna o ang kernel ibutang ngadto sa usa ka "panic" nga estado (nasabtan nga ang labing kasaligan nga mga sistema makit-an ang ingon nga mga sitwasyon ug tubaga kini). Ang modelo sa automat nga naghubit sa mga transisyon gikan sa usa ka estado ngadto sa lain gi-eksport sa "tuldok" (graphviz) nga format, pagkahuman gihubad kini gamit ang dot2c utility ngadto sa representasyon sa C, nga gikarga sa porma sa kernel module nga nagsubay sa mga deviation. sa pag-uswag sa pagpatuman gikan sa usa ka predefined nga modelo.
Ang pagsusi sa modelo sa run-time gipahimutang ingon usa ka labi ka gaan ug dali nga ipatuman nga pamaagi sa pag-verify sa pagkahusto sa pagpatuman sa mga sistema nga kritikal sa misyon, nga nagpuno sa mga klasikal nga pamaagi sa pag-verify nga kasaligan, sama sa pagsusi sa modelo ug mga pruweba sa matematika sa pagsunod sa code sa gihatag nga mga detalye. sa usa ka pormal nga pinulongan. Lakip sa mga bentaha sa RV mao ang abilidad sa paghatag og hugot nga pag-verify nga walay bulag nga pagpatuman sa tibuok nga sistema sa usa ka modelo nga pinulongan, ingon man usab sa usa ka flexible nga tubag sa wala damhang mga panghitabo, pananglitan, aron babagan ang dugang nga pagpadaghan sa usa ka kapakyasan sa kritikal nga mga sistema.
Source: opennet.ru