基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难.在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证.对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性.交互式定理证明方法中常用程序逻辑对程序进行验证,分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用这些方法的程序验证工具和程序验证成果进行总结.

基于分离逻辑的云存储系统并发正确性验证

云存储系统的应用日益广泛,其可靠性尤为受研究者关注。现有的基于块分离逻辑的验证方法能很好地描述和验证具备“文件-块-数据”三层架构的云存储系统的各类性质,文章在此基础上提出一种验证云存储系统并发正确性的方法,工作包括:(1)扩展云存储系统的建模语言,增加对线程间通信等并发行为的描述;(2)扩展断言语言,用于描述云存储环境下与并发执行和存储控制相关的系统性质;(3)提出一组霍尔规则,用于推导系统的性质。文章给出的验证实例能说明该方法的有效性。文章的工作扩展了块分离逻辑的适用范围,为MapReduce等框架下的并发程序正确性验证工作提供了理论基础。

基于TL2软件事务内存的并发程序的精化验证

软件事务内存并发机制将对共享存储复杂的同步访问控制转嫁给底层系统开发者,从而大大减轻高层程序员开发并发程序的负担。TL2是一个经典的基于锁的高性能软件事务内存算法。本文以一个TL2读写事务的底层具体实现为验证目标,首先采用并发程序间的精化关系来刻画基于TL2的底层细粒度并发程序是某个具体的高层抽象原子事务代码块的正确实现,然后通过基于依赖保证的并发程序模拟技术证明两个程序间具有精化关系,完成读写事务的底层实现在代码级的验证并总结TL2算法满足的不变式,为完成TL2算法在代码级的完整验证奠定基础。