Sciweavers

Share
VMCAI
2009
Springer

Shape-Value Abstraction for Verifying Linearizability

10 years 14 days ago
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.
Viktor Vafeiadis
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where VMCAI
Authors Viktor Vafeiadis
Comments (0)
books