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

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

微内核架构因其有效的模块隔离性而成为操作系统方面研究的热点,多线程机制是微内核架构需要解决的关键性能问题。有不少的工作对微内核架构多线程机制进行了研究,但存在频繁的系统地址空间切换和实现复杂度高的问题。采用形式化的方式对微内核架构多线程和安全机制进行描述和设计,提出一个微内核线程分层对象语义模型,用以设计多线程机制的线程间通信、调度和互斥同步方案。在已实现和验证的微内核操作系统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.