This paper presents a novel abstraction for heap-allocateddata structures that keeps track of both their shape and their con-tents. By combining this abstraction with thread-local analysis and rely-guarantee reasoning, we can verify a collection of fine-grained blockingand 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.
展开▼
