Proving Correctness of Concurrent Objects by Validating Linearization Points

In the recent years, several concurrent data-structures/objects have been proposed. These data-structures allow multiple threads/process to operate on them concurrently while maintaining consistency. By allowing multiple threads to operate on them simultaneously, these structures strive to increase parallelism. These structures typically involve the operating threads applying different fine-grained synchronization mechanisms. While these concurrent structures with fine-grained synchronization mechanisms certainly improve parallelism, proving their correctness has turned out to be a challenging task. The well accepted criterion for proving correctness of these concurrent objects is Linearizability. Showing that these concurrent structures are linearizable is non-trivial in many cases. The standard technique to show correctness adopted by several researchers and practitioners in this case is to use Linearization Points (LPs) - an atomic event within each method between the invocation and response events where the effect of the entire method seems to have taken place. In many of these cases, the LPs intuitively prove the correctness of the object. Without a formal proof, it is not clear if these LPs and hence the concurrent structure are indeed correct. In this paper, we present a hand-written technique for verifying the correctness of Linearization Points of a class of commonly used concurrent data-structures. Although the technique is hand-written, we believe that it is applicable to wide variety of concurrent data-structures. We demonstrate the efficacy of this technique by showing the correctness of two commonly used variants of set data-structure based on linked-lists: Hand-over-Hand locking and Lazy List. Further, we hope to extend this technique for automatic verification in future.