计算机科学 ›› 2018, Vol. 45 ›› Issue (9): 70-74.doi: 10.11896/j.issn.1002-137X.2018.09.010

• 第十六届全国软件与应用学术会议 • 上一篇    下一篇

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

丁贵强1, 王雷1, 王鹿鸣1, 康乔2   

  1. 北京航空航天大学计算机学院 北京1001911
    北京航空航天大学软件学院 北京1001912
  • 收稿日期:2017-10-15 出版日期:2018-09-20 发布日期:2018-10-10
  • 通讯作者: 王 雷 男,博士,副教授,主要研究方向为操作系统,E-mail:wanglei@buaa.edu.cn
  • 作者简介:丁贵强 男,硕士生,主要研究方向为微内核操作系统;王鹿鸣 男,主要研究方向为操作系统;康 乔 男,硕士生,主要研究方向为虚拟化。
  • 基金资助:
    本文受国家自然科学基金(61672073,61272167)资助。

Study of Partition Mechanism for seL4 on Multi-core Platform

DING Gui-qiang1, WANG Lei1, WANG Lu-ming1, KANG Qiao2   

  1. School of Computer Science & Engineering,Beihang University,Beijing 100191,China1
    School of Software,Beihang University,Beijing 100191,China2
  • Received:2017-10-15 Online:2018-09-20 Published:2018-10-10

摘要: 在航空电子等嵌入式领域中,多核时代已经来临,如何充分利用多核成为了现在系统领域的研究热点。同时由于系统集成度越来越高,一个硬件平台可能需要同时运行不同安全级别的任务,这就需要操作系统为应用提供隔离与保护。为了解决这两个问题,文中在目前只支持单核的seL4的基础上分别加入多核和分区隔离的支持,之后又提出多核和分区机制相结合的方案,实现了带分区机制的多核seL4。最终将其运行在qemu模拟器上,分区机制的实现符合ARINC653标准的语义。

关键词: seL4, 多核, 分区, 嵌入式

Abstract: 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.

Key words: Embedded, Multi-core, Partition, Sel4

中图分类号: 

  • TP316
[1]KLEIN G,ANDRONICK J,ELPHINSTONE K,et al.seL4:formalverification of an operating system kernel[J].Communications of the Acm,2010,53(6):107-115.
[2]PETERS S,DANIS A,ELPHINSTONE K,et al.For a Microkernel,a Big Lock Is Fine[C]∥Proceedings of the 6th Asia-Pacific Workshop on Systems.Newyork.NY,USA:ACM,APSys’15,2015.
[3]ALVES-FOSS J,OMAN P W,TAYLOR C,et al.The MILS architecture for high-assurance embedded systems[J].Internationl Journal of Embedded Systems,2006,2(3/4):239-247.
[4]PRISAZNUK P J.ARINC 653 role in integrated modular avio-nics(IMA)[C]∥2008 IEEE/AIAA 27th Digital Avionics Systems Conference.2008.
[5]COMMITTEE A E E,et al.Avionics application software stan-dard interface part 1required services[EB/OL].https://stan-dards.globalspec.com/std/280829/arinc-653p1.
[6]HAN S,JIN H W.Kernel-level ARINC653 partitioning for
Linux[C]∥Proceedings of the 27th Annual ACM Symposium on Applied Computing.2012:1632-1637.
[7]DELANGE J,POK L L.An ARINC653-compliant operating
system released under the BSD license[C]∥13th Real-Time Linux Workshop.2011.
[8]ASBERG M,NOLTE T.Towardsauser-mode approach to partitioned scheduling in the seL4 microkernel[J].ACM SIGBED Review,2013,10(3):15-22.
[9]FORD B,SUSARLA S.CPU inheritance scheduling[C]∥Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation(OSDI’96).1996:91-105.
[10]LACKORZYN′SKI A,WARG A,VÖLP M,et al.Flattening hie-rarchical scheduling[C]∥Proceedings of the Tenth ACM International Conference on Embedded Software.2012:93-102.
[11]HEISER A L G,LYONS A,VANGE M,et al.FlaRe:Efficient Capability Semantics for Timely Processor Access[EB/OL].https://people.mpi-sws.org/~bbb/papers/pdf/preprint-FlaRe.pdf.
[12]SERGEY B,ALEXANDRA F.User-level schedulingon NUMA multicore systems under Linux[EB/OL].http://citeseerx.ist.psu.edu /viewdoc/download?doi=10.1.1.369.9422&rep=rep1&type=pdf.
[13]MERCER C W,SAVAGE S,TOKUDA H.Processor capacity
reserves:An abstraction for managing processor usage[C]∥Fourth Workshop on Workstation Operating Systems.1993:129-134.
[14]UHLIG R,NEIGER G,RODGERS D,et al.Intel virtualization technology[J].Computer,2005,38(5):48-56.
[15]MERKEL D.Docker:lightweight linux containers for consistent development and deployment[J].Linux Journal,2014,2014(239):2.
[16]NICTA.The seL4 microkernel[EB/OL].https://github.com/seL4/seL4.
[17]KLEIN G,ANDRONICK J,ELPHINSTONE K,et al.Comprehensive formal verification of an OS micro-kernel[J].ACM Transactions on Computer Systems(TOCS),2014,32(1):32-102.
[1] 李浩东, 胡洁, 范勤勤.
基于并行分区搜索的多模态多目标优化及其应用
Multimodal Multi-objective Optimization Based on Parallel Zoning Search and Its Application
计算机科学, 2022, 49(5): 212-220. https://doi.org/10.11896/jsjkx.210300019
[2] 王如斌, 李瑞远, 何华均, 刘通, 李天瑞.
面向海量空间数据的分布式距离连接算法
Distributed Distance Join Algorithm for Massive Spatial Data
计算机科学, 2022, 49(1): 95-100. https://doi.org/10.11896/jsjkx.210100060
[3] 杜亮, 任鑫, 张海莹, 周芃.
基于局部回归融合的多核聚类方法
Multiple Kernel Clustering via Local Regression Integration
计算机科学, 2021, 48(8): 47-52. https://doi.org/10.11896/jsjkx.201000106
[4] 何权奇, 余飞鸿.
面向无线网络相机的低功耗架构研究综述
Review of Low Power Architecture for Wireless Network Cameras
计算机科学, 2021, 48(6A): 369-373. https://doi.org/10.11896/jsjkx.201100099
[5] 瞿伟, 余飞鸿.
基于多核处理器的非对称嵌入式系统研究综述
Survey of Research on Asymmetric Embedded System Based on Multi-core Processor
计算机科学, 2021, 48(6A): 538-542. https://doi.org/10.11896/jsjkx.200900204
[6] 卢永超, 王斌翊, 胡江峰, 穆阳, 任俊龙.
综合电子时间同步技术研究
Research on Integrated Electronic Time Synchronization Technology
计算机科学, 2021, 48(6A): 629-632. https://doi.org/10.11896/jsjkx.201100114
[7] 邵兴辉, 黄建华, 王梦楠, 武海霞, 麦勇.
基于信任的双层可拓展共识协议
Trust-based Dual-layer Scalable Consensus Protocol
计算机科学, 2021, 48(11): 142-150. https://doi.org/10.11896/jsjkx.210100126
[8] 庄园, 郭强, 张洁, 曾云辉.
大规模申威众核环境下二维数据计算的可扩展方法
Large Scalability Method of 2D Computation on Shenwei Many-core
计算机科学, 2020, 47(8): 87-92. https://doi.org/10.11896/jsjkx.191000011
[9] 黄锦灏, 丁钰真, 肖亮, 沈志荣, 朱珍民.
一种基于强化学习的嵌入式系统抗拒绝服务攻击的缓存调度方案
Reinforcement Learning Based Cache Scheduling Against Denial-of-Service Attacks in Embedded Systems
计算机科学, 2020, 47(7): 282-286. https://doi.org/10.11896/jsjkx.200100135
[10] 蔡玉鑫, 汤志伟, 赵博, 杨明, 吴禹非.
基于嵌入式多核DSP的加速软件系统
Accelerated Software System Based on Embedded Multicore DSP
计算机科学, 2020, 47(6A): 622-625. https://doi.org/10.11896/JsJkx.190400079
[11] 陈云.
嵌入式设备的邮递式升级方案
Embedded Device’s IAP Solution Based on Mail-update
计算机科学, 2020, 47(6A): 648-651. https://doi.org/10.11896/JsJkx.191000052
[12] 朱晓玲, 李琨, 张长胜, 杜付鑫.
基于Gabor小波变换和多核支持向量机的电梯导靴故障诊断方法
Elevator Boot Fault Diagnosis Method Based on Gabor Wavelet Transform and Multi-coreSupport Vector Machine
计算机科学, 2020, 47(12): 258-261. https://doi.org/10.11896/jsjkx.200700039
[13] 张长贵, 张岩峰, 李晓华, 聂铁铮, 于戈.
区块链新技术综述:图型区块链和分区型区块链
Survey of New Blockchain Techniques:DAG Based Blockchain and Sharding Based Blockchain
计算机科学, 2020, 47(10): 282-289. https://doi.org/10.11896/jsjkx.191000057
[14] 袁良,张云泉,白雪瑞,张广婷.
并行程序设计语言中局部性机制的研究
Research on Locality-aware Design Mechanism of State-of-the-art Parallel Programming Languages
计算机科学, 2020, 47(1): 7-16. https://doi.org/10.11896/jsjkx.181202409
[15] 李蜜, 庄毅, 胡镡文.
一种结合AADL与Z的嵌入式软件可靠性建模与评估方法
Embedded Software Reliability Model and Evaluation Method Combining AADL and Z
计算机科学, 2019, 46(8): 217-223. https://doi.org/10.11896/j.issn.1002-137X.2019.08.036
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!