一种基于P/T网的低级并发程序验证模型  

作　　者：梁英毅 王生原[1] 董渊[1] 

机构地区：[1]清华大学计算机科学与技术系,北京100084

出　　处：《中国科学：信息科学》2010年第1期13-32,共20页Scientia Sinica(Informationis)

基　　金：国家自然科学基金(批准号:60573017;90818019);国家高技术研究发展计划(批准号:2008AA01Z102)资助项目

摘　　要：随着片上多处理器/多核技术的不断发展,采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景.然而,低级并发程序的验证问题也成为程序语言领域一种新的挑战.并发程序安全性验证领域现有的工作多数是针对高级语言、规范或者演算,而针对机器级语言的甚少。这种情况的主要原因之一是缺少低级抽象模型.文中描述一种可验证的低级并发编程模型P-PMCC.P-PMCC程序是一个扩展的P/T网系统,其网结构用来刻画低级并发线程(原子的顺序汇编级代码)之间的并发关系.P-PMCC程序的验证采取模型检查和定理证明相结合的方法,分开考虑并发行为与顺序线程的规范和验证:前者借助于Petri网领域已有的方法,后者则借助现有的顺序程序的正确性证明方法。P-PMCC程序也可以看作并发程序的一种可验证的低级中间表示.

关 键 词：低级并发程序 PETRI网 抽象机器 程序验证 分离逻辑 

分 类 号：TN407[电子电信—微电子学与固体电子学]