Poling: SMT Aided Linearizability Proofs

Abstract. Proofs of linearizability of concurrent data structures generally rely on identifying linearization points to establish a simulation argument between the implementation and the specification. However, for many linearizable data structure operations, the linearization points may not correspond to their internal static code locations; for example, they might reside in the code of another concurrent operation. To overcome this limitation, we identify important program patterns that expose such instances, and describe a tool (Poling) that automatically verifies the linearizability of implementations that conform to these patterns.

• Type: Journal
• Year: 2015
• Where: CAV
• Authors: He Zhu, Gustavo Petri, Suresh Jagannathan
• Keywords: CAV 2015, Hardware