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

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