并发程序精化验证及其应用

《并发程序精化验证及其应用》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中国科学技术大学博士学位论文并发程序精化验证及其应用作者姓名：学科专业：导师姓名：完成时间：梁红瑾计算机软件与理论冯新宇教授邵中教授二零一四年五月：，白鳜＼，Author，sName：HongjinLiangspeciality：Conaputerso脚areandThe。Ivsuperv迅or：Pr。￡XinyuFengPr。￡zh。ngs二a。Fillishedtime：May,2014，CnI，．叶e-rl，甜怜f●、．’7吖治”焐鲫dO、，、I■■●●-k眦弋Kr惭Dd埒氏∞●lI●甜丌∞幻eOb．ba廿Saf工LO玎”治吣$ed怡川mAOS-KS；●l僧S钏m岭Ca

2、洲¨嗽陷钟糊蚴舱叫m童中国科学技术大学学位论文原创性声明本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均已在论文中作了明确的说明。作者签名：三避中国科学技术大学学位论文授权使用声明作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入《中国学位论文全文数据库》等有关数据库进行检索，可以采用影印、缩

3、印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论文的内容相一致。保密的学位论文在解密后也遵守此规定。／＼乒公开口保密(——年)作者签名：盗至!鳢导师签名：i刍隧签字日期：垫!生』：§!签字日期：丝!生：』!：主垒摘要许多程序验证问题都可以被归结为精化验证，即证明一个较具体的程序不会比一个较抽象的程序产生更多的行为。本文发掘了在并发环境下精化验证的应用场景，并提出若干种可以支持这些精化应用实例的验证技术。具体来说，本文在理解和验证并发程序精化方面做出了如下贡献。首先，本文提出了一种基于依赖／保证的模拟关系RGSim，作为并发程序精化的通用验证手段。这一新颖

4、的模拟关系将线程和并发环境之间的交互作为参数，从而获得可组合性，支持模块化验证。同时，它将精化应用中对并发环境的特定前提参数化，因而具有较好的灵活性和实用性。我们应用RGSim验证了并发环境下的几种程序优化。此外，我们还将并发垃圾收集器的验证归结为精化验证，并提出一种基于RGSim的通用验证框架。使用这一框架，我们验证了Boehm等人提出的并发的标记．清扫垃圾收集算法。其次，本文提出了一种霍尔风格的程序逻辑，用于高效地、模块化地验证并发对象的线性一致性。这是并发程序精化验证的一种重要应用。作为该程序逻辑的一部分，我们提出了一种轻量的辅助代码插桩机制。我们的程序逻辑支持可线性化

5、点不固定的并发算法，这些算法的验证难度很大。具体包括：使用帮助机制的无锁算法(如HSY栈)，可线性化点依赖未来不确定执行的算法(如懒惰集合算法)，以及同时有这两种特性的算法(如RDCSS算法)。我们还扩展了模拟关系RGSim以支持可线性化点不固定的程序，新的模拟关系保证了我们的程序逻辑的可靠性，它可以蕴涵一种上下文精化关系，该精化关系与线性一致性等价。我们应用这一程序逻辑验证了12个著名的并发算法，其中两个算法已经在Java并发包_java．util．concurrent中使用。最后，本文展示了一个用精化关系刻画并发对象完整正确性(包括线性一致性以及各种进展性性质)的统一框架

6、。我们证明了对于满足线性一致性的并发对象，每种进展性性质等价于一种特定的对终止性敏感的上下文精化关系。我们用上下文精化关系统一了并发对象的线性一致性和所有常见的进展性性质，包括无等待性、无锁性、无阻碍性、无饥饿性和无死锁性。根据这一结果，对于任何使用并发对象操作的客户端程序，我们可以模块化地验证该客户端程序的安全性和终止性。另一方面，它也告诉我们，有希望借鉴己有的验证上下文精化的技术来同时验证线性一致性和进展性性质。T摘要关键词：并发程序验证精化模拟关系程序逻辑程序正确性IIABSTRACTManyverificationproblemscanbereducedtorefin

7、ementverification，i．e·，provingthataconcreteprogramhasnomorebehaviorsthanamoreabstractprogram·Thisdis。sertationexplorestheapplicationsofrefinementverificationofconcurrentprograms，andproposescompositionalverificationtechniquesthatsupporttheseapplications·I