Shape-Value Abstraction for Verifying Linearizability

lue Abstraction for Verifying Linearizability Viktor Vafeiadis Microsoft Research, Cambridge, UK This paper presents a novel abstraction for heap-allocated data structures that keeps track of both their shape and their contents. By combining this abstraction with thread-local analysis and relyguarantee reasoning, we can verify a collection of fine-grained blocking and non-blocking concurrent algorithms for an arbitrary (unbounded) number of threads. We prove that these algorithms are linearizable, namely equivalent (modulo termination) to their sequential counterparts.

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Viktor Vafeiadis
• Keywords: Abstraction, Lue Abstraction, Non-blocking Concurrent Algorithms, Software Engineering, VMCAI 2009