Explicit Stabilisation for Modular Rely-Guarantee Reasoning
Explicit Stabilisation for Modular Rely-Guarantee Reasoning
复制标题
模块化依赖保证推理的显式稳定性
DOI：
10.1007/978-3-642-11957-6_32
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Matthew J. Parkinson
中科院分区：
文献类型：
--
作者：
John Wickerson;Mike Dodds;Matthew J. Parkinson
我们提出了一个新的形式化的稳定性的可靠保证，其中一个断言的稳定性被编码到其语法形式。这使得模块化推理有两个进步。首先，它使Rely-Guarantee首次能够独立于客户端环境验证并发库。其次，在顺序设置中，它允许在验证其客户端时隐藏模块的内部干扰。我们证明了我们的方法，通过验证，使用RGSep，版本7 Unix内存管理器，发现一个二十年的老错误的过程中。
We propose a new formalisation of stability for Rely-Guarantee, in which an assertion's stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients' environments. Secondly, in a sequential setting, it allows a module's internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds