|
扩展功能
|
|
| 本文信息 | |
 |
补充材料 |
|
PDF(1004KB) |
|
[HTML全文] |
|
参考文献 |
| 服务与反馈 | |
|
加入引用管理器 |
|
引用本文 |
|
Email Alert |
|
文章反馈 |
|
浏览反馈信息 |
| 本文关键词相关文章 | |
|
低级并发程序 |
|
Petri网 |
|
抽象机器 |
|
程序验证 |
|
分离逻辑 |
| 本文作者相关文章 | |
| PubMed | |
一种基于P/T网的低级并发程序验证模型
梁英毅*, 王生原*, 董渊*
清华大学计算机科学与技术系, 北京 100084
随着片上多处理器/多核技术的不断发展, 采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景. 然而, 低级并发程序的验证问题也成为程序语言领域一种新的挑战. 并发程序安全性验证领域现有的工作多数是 针对高级语言、规范或者演算, 而针对机器级语言的甚少. 这种情况的主要原因之一是缺少低级抽象模型. 文中描述一种可验证的低级并发编程模型P-PMCC. P-PMCC程序是一个扩展的~P/T~网系统, 其网结构用来刻画低级并发线程 (原子的顺序汇编级代码)之间的并发关系. P-PMCC程序的验证采取模型检查和定理证明相结合的方法, 分开考虑并发行为与顺序线程的规范和验证: 前者借助于~Petri~ 网领域已有的方法, 后者则借助现有的顺序程序的正确性证明方法. P-PMCC程序也可以看作并发程序的一种可验证的低级中间表示.
国家自然科学基金(批准号: 60573017, 90818019)和国家高技术研究发展计划(批准号: 2008AA01Z102)资助项目