多核平台上针对seL4的分区机制研究  

Study of Partition Mechanism for seL4 on Multi-core Platform

作　　者：丁贵强 王雷[1] 王鹿鸣 康乔 DING Gui-qiang;WANG Lei;WANG Lu-ming;KANG Qiao(School of Computer Science&Engineering,Beihang University,Beijing 100191,China;School of Software,Beihang University,Beijing 100191,China)

机构地区：[1]北京航空航天大学计算机学院,北京100191 [2]北京航空航天大学软件学院,北京100191

出　　处：《计算机科学》2018年第9期70-74,共5页Computer Science

基　　金：国家自然科学基金(61672073;61272167)资助

摘　　要：在航空电子等嵌入式领域中,多核时代已经来临,如何充分利用多核成为了现在系统领域的研究热点。同时由于系统集成度越来越高,一个硬件平台可能需要同时运行不同安全级别的任务,这就需要操作系统为应用提供隔离与保护。为了解决这两个问题,文中在目前只支持单核的seL4的基础上分别加入多核和分区隔离的支持,之后又提出多核和分区机制相结合的方案,实现了带分区机制的多核seL4。最终将其运行在qemu模拟器上,分区机制的实现符合ARINC653标准的语义。In avionics and other embedded fields,the multi-core era has come.How to make full use of multiple cores has become the research hotspot in field of the system.At the same time,as the system integration is getting higher and higher,a hardware platform may need to run tasks with different security levels,which requires the operating system to provide isolation and protection for the application.In order to solve the two problems mentioned above,this paper added multi-core and partition isolation support on the basis of seL4 with a single core,and then put forward multi-core seL4 and partition mechanism to achieve a partition mechanism with multi-core seL4 running on the qemu simulator.The implementation of the partition mechanism is in accordance with the semantics of the ARINC653 standard.

关 键 词：seL4 多核 分区 嵌入式 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]