Sciweavers

Share
CAV
2015
Springer

Poling: SMT Aided Linearizability Proofs

4 years 1 months ago
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.
He Zhu, Gustavo Petri, Suresh Jagannathan
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CAV
Authors He Zhu, Gustavo Petri, Suresh Jagannathan
Comments (0)
books