| 摘要: |
| 并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度, 在现实中有着非常广泛的应用. 但是并发程序与并发系统往往难以保证其实现的正确性, 实际应用程序运行中的错误会带来严重的后果. 同时, 并发程序执行时的不确定性会给其正确性验证带来巨大的困难. 在形式化验证方法中, 人们可以通过交互式定理证明器严格地对并发程序进行验证. 对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结, 它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性. 交互式定理证明方法中常用程序逻辑对程序进行验证, 分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案, 并对使用这些方法的程序验证工具和程序验证成果进行总结. |
| 关键词: 并发程序验证 可线性化 上下文精化 程序逻辑 关系霍尔逻辑 |
| DOI：10.13328/j.cnki.jos.007138 |
| 分类号: |
| 基金项目: |
|
| Survey on Interactive Theorem Proving Based Concurrent Program Verification |
|
WANG Zhong-Ye, WU Shu-Shu, CAO Qin-Xiang
|
|
School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai 200240, China
|
| Abstract: |
| Concurrent programs and systems are usually highly efficient and respond faster than serial systems, making them widely used in practice. However, concurrent programs and systems are often prone to error, which could bring fatal consequences in real world applications. Moreover, the non-determinism brought by concurrency is a major difficulty in the verification of concurrent programs. With formal verification, people could use interactive theorem provers to rigorously prove the correctness of a concurrent program. This study presents several correctness criteria for concurrent programs, which can be verified by interactive theorem proof techniques. The criteria include Hoare triple, linearizability, contextual refinement, and logical atomicity. Researchers usually use program logic to verify programs in an interactive theorem prover. This study summarizes the usage of concurrent separation logic, rely-guarantee-based logic, and relational Hoare logic in concurrent program verifications. It also surveys existing foundational verification tools and verification results by these techniques. |
| Key words: concurrent program verification linearizability contextual refinement program logic relational Hoare logic |
