Automatically Proving Linearizability

Abstract. This paper presents a practical automatic verification procedure for proving linearizability (i.e., atomicity and functional correctness) of concurrent data structure implementations. The procedure employs a novel instrumentation to verify logically pure executions, and is evaluated on a number of standard concurrent stack, queue and set algorithms.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Viktor Vafeiadis
• Keywords: Automatic Verification Procedure, CAV 2010, Concurrent Data Structure, Hardware, Standard Concurrent Stack