Poling: SMT aided linearizability proofs

He Zhu; Gustavo Petri; Suresh Jagannathan

doi:10.1007/978-3-319-21668-3_1

Poling: SMT aided linearizability proofs

He Zhu, Gustavo Petri, Suresh Jagannathan

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

14 Scopus citations

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.

Original language	English (US)
Title of host publication	Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings
Editors	Corina S. Păsăreanu, Daniel Kroening
Publisher	Springer Verlag
Pages	3-19
Number of pages	17
ISBN (Print)	9783319216676
DOIs	https://doi.org/10.1007/978-3-319-21668-3_1
State	Published - 2015
Externally published	Yes
Event	27th International Conference on Computer Aided Verification, CAV 2015 - San Francisco, United States Duration: Jul 18 2015 → Jul 24 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9207
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	27th International Conference on Computer Aided Verification, CAV 2015
Country/Territory	United States
City	San Francisco
Period	7/18/15 → 7/24/15

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-21668-3_1

Cite this

Zhu, H., Petri, G., & Jagannathan, S. (2015). Poling: SMT aided linearizability proofs. In C. S. Păsăreanu, & D. Kroening (Eds.), Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings (pp. 3-19). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9207). Springer Verlag. https://doi.org/10.1007/978-3-319-21668-3_1

Zhu, He ; Petri, Gustavo ; Jagannathan, Suresh. / Poling : SMT aided linearizability proofs. Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. editor / Corina S. Păsăreanu ; Daniel Kroening. Springer Verlag, 2015. pp. 3-19 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fd37cc08a5b045a79f6a0315c9643ea0,

title = "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.",

author = "He Zhu and Gustavo Petri and Suresh Jagannathan",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 27th International Conference on Computer Aided Verification, CAV 2015 ; Conference date: 18-07-2015 Through 24-07-2015",

year = "2015",

doi = "10.1007/978-3-319-21668-3_1",

language = "English (US)",

isbn = "9783319216676",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--19",

editor = "P{\u a}s{\u a}reanu, {Corina S.} and Daniel Kroening",

booktitle = "Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings",

address = "Germany",

}

Zhu, H, Petri, G & Jagannathan, S 2015, Poling: SMT aided linearizability proofs. in CS Păsăreanu & D Kroening (eds), Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9207, Springer Verlag, pp. 3-19, 27th International Conference on Computer Aided Verification, CAV 2015, San Francisco, United States, 7/18/15. https://doi.org/10.1007/978-3-319-21668-3_1

Poling : SMT aided linearizability proofs. / Zhu, He; Petri, Gustavo; Jagannathan, Suresh.

Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. ed. / Corina S. Păsăreanu; Daniel Kroening. Springer Verlag, 2015. p. 3-19 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9207).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Poling

T2 - 27th International Conference on Computer Aided Verification, CAV 2015

AU - Zhu, He

AU - Petri, Gustavo

AU - Jagannathan, Suresh

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 -

Zhu H, Petri G, Jagannathan S. Poling: SMT aided linearizability proofs. In Păsăreanu CS, Kroening D, editors, Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Springer Verlag. 2015. p. 3-19. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-21668-3_1

Poling: SMT aided linearizability proofs

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this