Proving correctness of highly-concurrent linearisable objects

We study a family of implementations for linked lists using finegrain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical, coarse-grain synchronisation. Our examples are demonstrative of common design patterns such as lock coupling, optimistic, and lazy synchronisation. Although they are are highly concurrent, we prove that they are linearisable, safe, and they correctly implement a highstraction. Our proofs illustrate the power and applicability of rely-guarantee reasoning, as well of some of its limitations. The examples of the paper establish a benchmark challenge for other reasoning techniques. Categories and Subject Descriptors D.2.3 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Algorithms, verification Keywords Concurrent programming, shared-memory concurrency, formal verification, linearisabil...

• Type: Conference
• Year: 2006
• Where: PPOPP
• Authors: Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro
• Keywords: Coarse-grain Synchronisation, Distributed And Parallel Computing, PPOPP 2006, Rely-guarantee Reasoning, finegrain Synchronisation