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.
翻译:繁忙的禁止协议是一个读者之间没有资源争议的新读写锁,使得它能够超过其他锁。 为了核查它,原始作者提供了其实施规格及其不那么复杂的外部行为,但仅被证明相当于7条线。我们用锥形和foci验证框架提供了一个一般性证明,该框架用锥形和foci验证框架重新描述两种规格是否在对执行和规格中发生的数据对象之间的关系的证明义务方面有着两个不同的分支。我们提供了这个框架的延伸,包括数据对象的另外三个属性。当这三个特性同时保持时,这两个系统是差异-保留分支,两样不同,上述关系的一个更强有力的版本也区分了活锁。我们证明这一扩展是合理的,并用它来为繁忙的禁止协议提供一般等同证据。