TY - GEN
T1 - Poling
T2 - 27th International Conference on Computer Aided Verification, CAV 2015
AU - Zhu, He
AU - Petri, Gustavo
AU - Jagannathan, Suresh
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84951063389&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84951063389&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-21668-3_1
DO - 10.1007/978-3-319-21668-3_1
M3 - Conference contribution
AN - SCOPUS:84951063389
SN - 9783319216676
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 19
BT - Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings
A2 - Păsăreanu, Corina S.
A2 - Kroening, Daniel
PB - Springer Verlag
Y2 - 18 July 2015 through 24 July 2015
ER -