分区操作系统内核中隔离性质的研究

为了达到经过形式化验证分区操作系统内核隔离性质的目标,采取形式化方法描述系统的顶层规范设计中描述隔离性质需求,通过将航空电子应用软件标准接口ARINC653与GWV定理相结合,实现了对分区操作系统需要满足的隔离性质的抽象描述,并通过使用类Z/Z++作为形式化描述语言。     

并发事务的一种操作模型

本文定义了一种描述分布式数据系统并发事务行为的操作模型，以此为基础讨论了并发事务的调度，并享模式的Ｌｏｃｋｉｎｇ机制，死锁等问题。     

基于ORC的OpenMP编译器设计与实现

该文提出了一种OpenMP翻译技术,旨在提高OpenMP编译系统的性能,并在这种技术基础上构造了一个完整的基于ORC的OpenMP编译系统。系统采用了下面的主要技术来提高性能:1)系统集成在后端的优化编译器中,具有更多的优化机会,并可以采用更为精细的开销模型;2)提出了一种基于指导语句全局嵌套类型的OpenMP翻译技术,可以有效地减少翻译代码的长度,并减少运行时开销。这个OpenMP系统从设计开始,就是为了提供一个合适的编译技术研究平台,具有更好的可控制性、可调试性和丰富的工具支持。     

BSP用于分布式系统的协议规范

ＢＳＰ是一种带有广播原语的分布式语言，能很好地支持分布式系统的消息传递。本文强调了ＢＳＰ在分布式系统协议规范方面的应用，并完成了对ＯＳＩ参考模型的网络协议以及数据库并控制的ｔｉｍｅｓｔａｍｐ协议的规范说明。     

嵌入式CPU软硬件协同开发中的操作系统设计

为了满足高性能嵌入式CPU软硬件协同开发的需要,提出一个嵌入式Linux操作系统设计方案,在真正的硬件完成之前利用虚拟原型系统进行软硬件集成测试。该方案基于开放源代码软件,采用精简配置的Linux Kernel,以u-Clibc和Busybox为主构成根文件系统,特别选择加入必要的基准测试程序。该系统成功应用于清华大学THUMP系列CPU开发,保证了验证的完备性,提高了验证效率,为CPU的性能优化提供了有力的支持。实验结果表明:该方案满足了验证目的和虚拟环境对操作系统设计提出的严格要求,同时为目标CPU未来运行系统提供了基础。     

Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy

Concurrent programs written in a machine level language are being used in many areas but verifi- cation of such programs brings new challenges to the programming language community. Most of the stud- ies in the literature on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi. Therefore, more studies are needed on concurrency verification for machine level language programs. This paper describes a framework of a Petri net based safety policy for the verification of concurrent assembly programs, to exploit the capability of Petri nets in concurrency modeling. The con- currency safety properties can be considered separately using the net structure and by mixing Hoare logic and computational tree logic. Therefore, more useful higher-level safety properties can be specified and verified.