基于有色网的事务型并发编程模型及其验证技术

基于共享存储器的并发程序设计将成为片上多处理器(CMP)系统应用开发的主流程序设计范型。以新兴的事务型存储器技术取代锁机制实现对共享数据访问的互斥和同步，可以极大地降低此类并发程序设计的难度。然而，针对这种新型体系结构的并发编程模型及其验证技术的研究目前尚处于开始阶段。本项目将提出一种有色Petri网与事务型存储器理念相结合的新型并发编程模型，研究目标是使得这种基于共享存储器的事务型并发程序既易于编码和验证，又利于发挥CMP系统的效能。在该模型中，并发程序本身是一个有色 Petri 网系统，其变迁对应于事务型的顺序线程，网结构描述并发关系。并发行为的验证以网系统的模型检验为基础，顺序线程的规范和验证基于通常的程序逻辑方法。原型系统的设计将采用验证式编译器框架，以可信的低级并发程序验证系统为基础，同时包括可支持低级并发程序执行的虚拟机环境，虚拟机程序将被映射到带有事务型存储器CMP系统结构。