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

• 作者: 赵立飞
• 来源期刊: 电子技术
• 关键词: 软件事务内存 并发程序验证 TL2 基于依赖保证的模拟技术 精化验证
• 年，卷（期）: 2014,（9）
• 所属期刊栏目: 电子技术研发
• 页码范围: 43-49
• 页数: 7页
• 字数: 6325字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵立飞	中国科学技术大学计算机科学与技术学院	1	0	0.0	0.0