论文标题
验证繁忙的验证协议（使用锥和焦点框架的扩展）
Verification of the busy-forbidden protocol (using an extension of the cones and foci framework)
论文作者
论文摘要
繁忙的验证协议是一个新的读者撰写的锁定，读者之间没有资源争议，这使其可以胜过其他锁。为了进行验证，原始作者提供了其实施及其较不复杂的外部行为的规格，但仅证明是最多7个线程的等效物。我们使用锥体和焦点证明框架提供了一般证明，该框架在实现和规范中发生的数据对象之间的关系方面是否有两个规格为分支的分支。我们提供了该框架的扩展，该框架由数据对象上的三个附加属性组成，当这三个其他属性还具有时，这两个系统是差异呈差异的分支，这是上述关系的更强版本，也区分了牲畜。我们证明了此扩展名声并使用它来为繁忙的验证协议提供一般的等价证明。
The busy-forbidden protocol is a new readers-writer lock with no resource contention between readers, which allows it to outperform other locks. For its verification, specifications of its implementation and its less complex external behavior are provided by the original authors but are only proven equivalent for up to 7 threads. We provide a general proof using the cones and foci proof framework, which rephrases whether two specifications are branching bisimilar in terms of proof obligations on relations between the data objects occurring in the implementation and specification. We provide an extension of this framework consisting of three additional properties on data objects, When these three additional properties also hold, the two systems are divergence-preserving branching bisimilar, a stronger version of the aforementioned relation that also distinguishes livelock. We prove this extension to be sound and use it to give a general equivalence proof for the busy-forbidden protocol.
