摘要: 微内核架构因其有效的模块隔离性而成为操作系统方面研究的热点,多线程机制是微内核架构需要解决的关键性能问题。有不少的工作对微内核架构多线程机制进行了研究,但存在频繁的系统地址空间切换和实现复杂度高的问题。采用形式化的方式对微内核架构多线程和安全机制进行描述和设计,提出一个微内核线程分层对象语义模型,用以 设计多线程机制的线程间通信、调度和互斥同步方案。在已实现和验证的微内核操作系统VTOS中对多线程功能和性能进行了测试,结果表明 VTOS有效地实现了多线程机制,并具有很好的系统性能。
[1] Zhou D.Towards the Formal Modeling of a Secure Operating System [C]∥ Proc.23rd National Information System Security Conference.2000 [2] Liedtke J.On μ-Kernel Construction[C]∥ Proc.15th ACMsymposium on Operating Systems Principles (SOSP’95).1995:237-250 [3] Heiser G,Elphinstone K,Kuz I,et al.Towards trustworthycomputing systems:taking microkernels to the next level [J].ACM SIGOPS Operating Systems Review,2007,41(4):3-11 [4] CMU CS.Mach Project [EB/OL].http://www-2.cs.cmu.edu/afs/cs/project/mach/public/www/mach.html,2011-06-05 [5] Accetta M,Baron R,Bolosky W,et al.Mach:A New KernelFoundation for UNIX Development [J].Computer,1986,39(4864):1-16 [6] L4Group.The L4μ-Kernel Family [EB/OL].http://os.inf.tu-dresden.de/L4/ [7] Elkaduwe D,Klein G,Elphinstone K.Verified Protection Model of the seL4Microkernel [C]∥LNCS 5295.2008:99-114 [8] Klein G,Andronick J,Elphinstone K,et al.seL4:Formal Verification of an Operating-System Kernel [J].Communications of the ACM,2010,53(6):107-115 [9] Smullyan R M.First-Order Logic (Dover Books on Mathema-tics) [M].Mineola:Dover Publications,1995 [10] Stallings W.Operating Systems:Internals and Design Principles [M].New Jersey:Prentice Hall,2004 [11] Bovet D P,Cesati M.Understanding the Linux Kernel (3rd)[M].Sebastopol:O’Reilly,2005 [12] Franke H,Russell R,Kirkwood M.Fuss,futexes and furwocks:Fast Userlevel Locking in Linux [C]∥Proc.Ottawa Linux symposium.2002 |
No related articles found! |
|