计算机科学 ›› 2018, Vol. 45 ›› Issue (9): 70-74.doi: 10.11896/j.issn.1002-137X.2018.09.010
丁贵强1, 王雷1, 王鹿鸣1, 康乔2
DING Gui-qiang1, WANG Lei1, WANG Lu-ming1, KANG Qiao2
摘要: 在航空电子等嵌入式领域中,多核时代已经来临,如何充分利用多核成为了现在系统领域的研究热点。同时由于系统集成度越来越高,一个硬件平台可能需要同时运行不同安全级别的任务,这就需要操作系统为应用提供隔离与保护。为了解决这两个问题,文中在目前只支持单核的seL4的基础上分别加入多核和分区隔离的支持,之后又提出多核和分区机制相结合的方案,实现了带分区机制的多核seL4。最终将其运行在qemu模拟器上,分区机制的实现符合ARINC653标准的语义。
中图分类号:
[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 |
|