RISC-V បានផ្ទៀងផ្ទាត់មីខឺរហ្សែល seL4 នៅលើឧបករណ៍កែច្នៃ RV64 របស់ពួកគេ

មូលនិធិ RISC-V បានប្រកាសថាបានផ្ទៀងផ្ទាត់ របៀបដែលមីក្រូជីនដំណើរការ seL4 នៅក្នុងប្រព័ន្ធជាមួយ ស្ថាបត្យកម្មសំណុំការណែនាំ RISC-V ។ ក្នុងនោះដំណើរការនៃការផ្ទៀងផ្ទាត់ត្រូវបានកាត់បន្ថយទៅជាភ័ស្តុតាងគណិតវិទ្យានៃភាពអាចជឿជាក់បាននៃអេសអិល ៤ ដែលបង្ហាញពីការអនុលោមតាមច្បាប់ពេញលេញជាមួយនឹងលក្ខណៈជាក់លាក់ដែលបានបញ្ជាក់ជាភាសាផ្លូវការ

ការធ្វើតេស្តភាពជឿជាក់អាចជួយឱ្យ seL4 ត្រូវបានប្រើនៅក្នុងប្រព័ន្ធសំខាន់នៃបេសកកម្មដោយផ្អែកលើប្រព័ន្ធដំណើរការ RISC-V RV64ដែលត្រូវការកម្រិតខ្ពស់នៃភាពអាចជឿជាក់បាននិងមិនធានាការបរាជ័យ។

អ្នកអភិវឌ្ឍន៍សូហ្វវែរដែលដំណើរការលើខឺណែល seL4 អាចមានទំនុកចិត្តទាំងស្រុងថាក្នុងករណីមានការខកខានផ្នែកមួយនៃប្រព័ន្ធការបរាជ័យនេះនឹងមិនរាលដាលដល់ផ្នែកផ្សេងទៀតនៃប្រព័ន្ធនិងជាពិសេសដល់ផ្នែកសំខាន់ៗរបស់វា។

អំពី seL4

ស្ថាបត្យកម្ម seL4 មិនគួរឱ្យកត់សម្គាល់សម្រាប់ការយកផ្នែកចេញដើម្បីគ្រប់គ្រងធនធានខឺណែលក្នុងចន្លោះអ្នកប្រើ និងប្រើវិធីសាស្ត្រត្រួតពិនិត្យការចូលប្រើដូចគ្នាសម្រាប់ធនធានដូចជាធនធានអ្នកប្រើ។

មីក្រូវ៉េវ មិនផ្តល់នូវការអរូបីកំរិតខ្ពស់ទេ រៀបចំរួចហើយដើម្បីគ្រប់គ្រងឯកសារដំណើរការការភ្ជាប់បណ្តាញ។ ល។ ប៉ុន្តែជំនួសវិញ ផ្តល់តែយន្តការតិចតួចប៉ុណ្ណោះដើម្បីគ្រប់គ្រងការចូលប្រើអាសយដ្ឋានអាស័យដ្ឋាន, រំខាននិងធនធានដំណើរការ។

អរូបីកម្រិតខ្ពស់និងកម្មវិធីបញ្ជាសម្រាប់ការប្រាស្រ័យទាក់ទងជាមួយកុំព្យួទ័រត្រូវបានអនុវត្តដាច់ដោយឡែកពីគ្នានៅលើកំពូលមីក្រូវ៉េវក្នុងទម្រង់នៃភារកិច្ចដែលបានអនុវត្តនៅកម្រិតអ្នកប្រើប្រាស់។

ការទទួលបានភារកិច្ចបែបនេះទៅនឹងធនធានដែលមាននៅក្នុងមីក្រូខនត្រូវបានរៀបចំឡើងតាមរយៈនិយមន័យនៃច្បាប់។

RISC-V ផ្តល់នូវប្រព័ន្ធបើកចំហនិងបត់បែន នៃសេចក្តីណែនាំម៉ាស៊ីនដែល អនុញ្ញាតឱ្យបង្កើតមីក្រូវ៉េវសម្រាប់កម្មវិធីតាមអំពើចិត្តដោយមិនតម្រូវឱ្យមានការកាត់បន្ថយ និងដោយមិនកំណត់លក្ខខណ្ឌនៃការប្រើប្រាស់។

RISC-V អនុញ្ញាតឱ្យអ្នកបង្កើត SoCs និងខួរក្បាលដែលបានបើកទាំងស្រុង។ បច្ចុប្បន្ននេះផ្អែកលើការបញ្ជាក់របស់ RISC-V ក្រុមហ៊ុននិងសហគមន៍មួយចំនួនដែលស្ថិតនៅក្រោមអាជ្ញាប័ណ្ណឥតគិតថ្លៃផ្សេងៗគ្នា (BSD, MIT, Apache 2.0) កំពុងអភិវឌ្ឍជាច្រើននៃស្នូលមីក្រូវ៉េវសូកូសនិងបន្ទះសៀគ្វី។

ការគាំទ្រ RISC-V គឺមានតាំងពីការចេញផ្សាយ Glibc 2.27, binutils 2.30, gcc 7 និងខឺណែលលីនុច 4.15 ។

អំពីការធ្វើតេស្តមីក្រូជីល seL4

ដំបូងមីក្រូវ៉េវ seL4 ត្រូវបានផ្ទៀងផ្ទាត់សម្រាប់ឧបករណ៍ដំណើរការអេមអេសអេមប៊ីត 32 ប៊ីតនិង ក្រោយមកទៀតសម្រាប់ x86 ៦៤ ប៊ីត.

វាត្រូវបានគេសង្កេតឃើញថាការរួមបញ្ចូលគ្នានៃស្ថាបត្យកម្មផ្នែករឹងចំហររបស់ RISC-V ជាមួយនឹងមីក្រូបើក seL4 នឹងទទួលបានកំរិតសន្តិសុខថ្មីមួយដូចជាសមាសធាតុផ្នែករឹងនាពេលអនាគតក៏អាចត្រូវបានផ្ទៀងផ្ទាត់យ៉ាងពេញលេញផងដែរដែលមិនអាចសម្រេចបានសម្រាប់ស្ថាបត្យកម្មផ្នែករឹងដែលមានកម្មសិទ្ធិ។

នៅពេលយើងពិនិត្យមើល seL4 យើងត្រូវសន្មតថាផ្នែករឹងកំពុងដំណើរការបានត្រឹមត្រូវ (នោះគឺដូចដែលបានបញ្ជាក់) ។ នោះសន្មតថាមានការបញ្ជាក់ដែលមិនមានភាពប្រាកដប្រជានៅក្នុងកន្លែងដំបូងដែលមិនមែនជាករណីសម្រាប់ផ្នែករឹងទាំងអស់ទេ។ 

ប៉ុន្តែសូម្បីតែនៅពេលមានការបញ្ជាក់បែបនេះមានហើយវាជាផ្លូវការ (នោះគឺត្រូវបានគេដាក់បញ្ចូលទៅក្នុងទម្រង់គណិតវិទ្យាដែលគាំទ្រដល់ហេតុផលគណិតវិទ្យាអំពីលក្ខណៈសម្បត្តិរបស់វា) តើយើងដឹងយ៉ាងដូចម្តេចថាវាពិតជាចាប់យកឥរិយាបទរបស់ផ្នែករឹង? 

ការពិតគឺថាយើងអាចប្រាកដថាវាមិនមែនទេ។ ផ្នែករឹងមិនខុសពីកម្មវិធីដែលក្នុងនោះទាំងពីរមានកំហុសទេ។

ប៉ុន្តែការមាន ISA បើកចំហមានគុណសម្បត្តិដែលលើសពីការមិនមានសិទ្ធិជាប់ពន្ធនាគារ។ មួយគឺថាវាអនុញ្ញាតឱ្យមានការអនុវត្តផ្នែករឹងប្រភពបើកចំហ។

នៅពេលពិនិត្យមើល SeL4 វាត្រូវបានសន្មតថាឧបករណ៍ដំណើរការដូចបានចង្អុលបង្ហាញហើយការបញ្ជាក់នេះពិពណ៌នាយ៉ាងពេញលេញអំពីឥរិយាបថរបស់ប្រព័ន្ធប៉ុន្តែការពិតឧបករណ៍មិនមានកំហុសទេដែលត្រូវបានបង្ហាញយ៉ាងល្អដោយបញ្ហាដែលកើតឡើងជាប្រចាំនៅក្នុងយន្តការប្រតិបត្តិដែលប៉ាន់ស្មាន។ ។

បើកវេទិកាផ្នែករឹងធ្វើសមាហរណកម្មការផ្លាស់ប្តូរ ទាក់ទងនឹងសន្តិសុខឧទាហរណ៍ដើម្បីទប់ស្កាត់បណ្តាញលេចធ្លាយដែលអាចកើតមានទាំងអស់តាមរយៈបណ្តាញភាគីទីបីដែលវាមានប្រសិទ្ធភាពក្នុងការកម្ចាត់បញ្ហាដោយផ្នែករឹងជាជាងព្យាយាមរកដំណោះស្រាយដោយសូហ្វវែរ។

នៅចុងបញ្ចប់ប្រសិនបើអ្នកចង់ដឹងបន្ថែមអំពីវាអ្នកអាចពិគ្រោះជាមួយកំណត់សំគាល់នៅក្នុងឯកសារ តំណខាងក្រោម។