微内核架构多线程机制的形式化设计研究  

Research on Formal Design of Multi-thread Mechanism Based on Microkernel Architecture

作　　者：钱振江[1,2,3] 卢亮[1,2] 黄皓[1,2] 

机构地区：[1]南京大学软件新技术国家重点实验室,南京210046 [2]南京大学计算机科学与技术系,南京210046 [3]常熟理工学院计算机科学与工程学院,常熟215500

出　　处：《计算机科学》2013年第4期136-141,163,共7页Computer Science

基　　金：国家高技术研究发展计划(863)(2011AA01A202);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)资助

摘　　要：微内核架构因其有效的模块隔离性而成为操作系统方面研究的热点,多线程机制是微内核架构需要解决的关键性能问题。有不少的工作对微内核架构多线程机制进行了研究,但存在频繁的系统地址空间切换和实现复杂度高的问题。采用形式化的方式对微内核架构多线程和安全机制进行描述和设计,提出一个微内核线程分层对象语义模型,用以设计多线程机制的线程间通信、调度和互斥同步方案。在已实现和验证的微内核操作系统VTOS中对多线程功能和性能进行了测试,结果表明VTOS有效地实现了多线程机制,并具有很好的系统性能。Microkernel architecture has become a hot topic in the research area of operating systems because of its effective isolation for modules.The multi-thread mechanism is a critical issue for the performance of the microkernel architecture.Many works research into the multi-thread of microkernel operating systems,but there are some problems such as frequent switching of system address space and high degree of implementation complexity.We used formal methods to describe and design the multi-thread and security mechanism,and proposed a hierarchical object semantics model.With the object semantics model,we formally designed the mechanism of inter-thread communication,thread scheduling,mutual exclusion and synchronization.Meanwhile,we used our self-implemented and verified microkernel operating system-VTOS as an example to test,and the results show that VTOS achieves multi-thread effectively and has a good system performance.

关 键 词：微内核 多线程 操作系统 形式化描述 形式化设计 

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