research-article

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects

Authors:

Aleksandar Nanevski,

Anindya Banerjee,

Germán Andrés DelbiancoAuthors Info & Claims

OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

Pages 92 - 110

https://doi.org/10.1145/2983990.2983999

Published: 19 October 2016 Publication History

Abstract

Designing efficient concurrent objects often requires abandoning the standard specification technique of linearizability in favor of more relaxed correctness conditions. However, the variety of alternatives makes it difficult to choose which condition to employ, and how to compose them when using objects specified by different conditions.

In this work, we propose a uniform alternative in the form of Hoare logic, which can explicitly capture--in the auxiliary state--the interference of environment threads. We demonstrate the expressiveness of our method by verifying a number of concurrent objects and their clients, which have so far been specified only by non-standard conditions of concurrency-aware linearizability, quiescent, and quantitative quiescent consistency. We report on the implementation of the ideas in an existing Coq-based tool, providing the first mechanized proofs for all the examples in the paper.

References

[1]

FCSL: Fine-grained Concurrent Separation Logic. Coq Development and Code Commentary. Available on the project website at http://software.imdea.org/fcsl.

[2]

Y. Afek, G. Korland, and E. Yanovsky. Quasi-Linearizability: Relaxed Consistency for Improved Concurrency. In OPODIS, pages 395–410. Springer, 2010.

Digital Library

[3]

M. Ajtai, J. Koml´os, and E. Szemerédi. An O(n log n) sorting network. In STOC, pages 1–9. ACM, 1983.

Digital Library

[4]

J. Aspnes, M. Herlihy, and N. Shavit. Counting networks. J. ACM, 41(5):1020–1048, 1994.

Digital Library

[5]

C. J. Bell, A. W. Appel, and D. Walker. Concurrent separation logic for pipelined parallelization. In SAS, pages 151–166. Springer, 2010.

Digital Library

[6]

A. Bouajjani, M. Emmi, C. Enea, and J. Hamza. Tractable refinement checking for concurrent objects. In POPL, pages 651–662. ACM, 2015.

Digital Library

[7]

Coq Development Team. The Coq Proof Assistant Reference Manual - Version 8.5pl2, 2016. https://coq.inria.fr.

[8]

P. da Rocha Pinto, T. Dinsdale-Young, M. Dodds, P. Gardner, and M. J. Wheelhouse. A simple abstraction for complex concurrent indexes. In OOPSLA, pages 845–864. ACM, 2011.

Digital Library

[9]

P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. TaDA: A Logic for Time and Data Abstraction. In ECOOP, pages 207–231. Springer, 2014.

Digital Library

[10]

J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, and H. Wehrheim. Quiescent Consistency: Defining and Verifying Relaxed Linearizability. In FM, pages 200–214. Springer, 2014.

Digital Library

[11]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent Abstract Predicates. In ECOOP, pages 504–528. Springer, 2010.

Digital Library

[12]

M. Dodds, S. Jagannathan, and M. J. Parkinson. Modular reasoning for deterministic parallelism. In POPL, pages 259– 270. ACM, 2011.

Digital Library

[13]

C. Dragoi, A. Gupta, and T. A. Henzinger. Automatic linearizability proofs of concurrent objects with cooperating updates. In CAV, pages 174–190. Springer, 2013.

[14]

Class Exchanger<V>, Java Platform SE 8 Documentation. Available from http://docs.oracle.com/javase/8/ docs/api/java/util/concurrent/Exchanger.html. Accessed June 24, 2015.

[15]

I. Filipovic, P. W. O’Hearn, N. Rinetzky, and H. Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51- 52):4379–4398, 2010.

Digital Library

[16]

M. Fu, Y. Li, X. Feng, Z. Shao, and Y. Zhang. Reasoning about optimistic concurrency using a program logic for history. In CONCUR, pages 388–402. Springer, 2010.

Digital Library

[17]

G. Gonthier, A. Mahboubi, and E. Tassi. A Small Scale Reflection Extension for the Coq system. Technical Report 6455, Microsoft Research – Inria Joint Centre, 2009.

[18]

A. Gotsman, N. Rinetzky, and H. Yang. Verifying concurrent memory reclamation algorithms with grace. In ESOP, pages 249–269. Springer, 2013.

Digital Library

[19]

A. Gotsman and H. Yang. Linearizability with ownership transfer. In CONCUR, pages 256–271. Springer, 2012.

Digital Library

[20]

A. Haas, T. A. Henzinger, A. Holzer, C. M. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, and H. Veith. Local Linearizability for Concurrent Container-Type Data Structures. In CONCUR, 2016. To appear.

[21]

N. Hemed and N. Rinetzky. Brief announcement : Concurrency-Aware Linearizability. In PODC, pages 209– 211. ACM, 2014.

Digital Library

[22]

N. Hemed, N. Rinetzky, and V. Vafeiadis. Modular verification of concurrency-aware linearizability. In DISC, pages 371–387. Springer, 2015.

[23]

T. A. Henzinger, C. M. Kirsch, H. Payer, A. Sezgin, and A. Sokolova. Quantitative relaxation of concurrent data structures. In POPL, pages 317–328. ACM, 2013.

Digital Library

[24]

M. Herlihy and N. Shavit. The art of multiprocessor programming. M. Kaufmann, 2008.

Digital Library

[25]

M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst., 12(3):463–492, 1990.

Digital Library

[26]

A. Hobor and C. Gherghina. Barriers in concurrent separation logic. In ESOP, pages 276–296. Springer, 2011.

Digital Library

[27]

B. Jacobs and F. Piessens. Expressive modular fine-grained concurrency specification. In POPL, pages 271–282. ACM, 2011.

Digital Library

[28]

R. Jagadeesan and J. Riely. Between Linearizability and Quiescent Consistency - Quantitative Quiescent Consistency. In ICALP (2), pages 220–231. Springer, 2014.

[29]

R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer. Higherorder ghost state. In ICFP. ACM, 2016.

Digital Library

[30]

R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL, pages 637–650. ACM, 2015.

Digital Library

[31]

L. Lamport. Composition: A way to make proofs harder. In COMPOS, pages 402–423. Springer, 1998.

Digital Library

[32]

R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarse-grained concurrency. In POPL, pages 561–574. ACM, 2013.

Digital Library

[33]

H. Liang and X. Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, pages 459–470. ACM, 2013.

Digital Library

[34]

A. McCreight. Practical Tactics for Separation Logic. In TPHOLs, pages 343–358. Springer, 2009.

Digital Library

[35]

A. Nanevski, R. Ley-Wild, I. Sergey, and G. A. Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP, pages 290–310. Springer, 2014.

Digital Library

[36]

S. S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM, 19(5):279– 285, 1976.

Digital Library

[37]

A. Raad, J. Villard, and P. Gardner. CoLoSL: Concurrent Local Subjective Logic. In ESOP, pages 710–735. Springer, 2015.

[38]

M. C. Rinard. Unsynchronized techniques for approximate parallel computing. In RACES - SPLASH Workshop, 2012.

[39]

W. N. Scherer III, D. Lea, and M. L. Scott. A scalable elimination-based exchange channel. In SCOOL, 2005.

[40]

I. Sergey, A. Nanevski, and A. Banerjee. Mechanized verification of fine-grained concurrent programs. In PLDI, pages 77–87. ACM, 2015.

Digital Library

[41]

I. Sergey, A. Nanevski, and A. Banerjee. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP, pages 333–358. Springer, 2015.

Digital Library

[42]

N. Shavit. Data structures in the multicore age. Commun. ACM, 54(3):76–84, 2011.

Digital Library

[43]

N. Shavit and A. Zemach. Diffracting trees. ACM Trans. Comput. Syst., 14(4):385–428, 1996.

Digital Library

[44]

K. Svendsen and L. Birkedal. Impredicative Concurrent Abstract Predicates. In ESOP, pages 149–168. Springer, 2014.

Digital Library

[45]

K. Svendsen, L. Birkedal, and M. J. Parkinson. Modular reasoning about separation of concurrent data structures. In ESOP, pages 169–188. Springer, 2013.

Digital Library

[46]

R. K. Treiber. Systems programming: coping with parallelism. Technical Report RJ 5118, IBM Almaden, 1986.

[47]

A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP, pages 377–390. ACM, 2013.

Digital Library

[48]

A. Turon, V. Vafeiadis, and D. Dreyer. GPS: navigating weak memory with ghosts, protocols, and separation. In OOPSLA, pages 691–707. ACM, 2014.

Digital Library

[49]

A. J. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer. Logical relations for fine-grained concurrency. In POPL, pages 343–356. ACM, 2013.

Digital Library

[50]

V. Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, 2007.

[51]

V. Vafeiadis. Automatically proving linearizability. In CAV, pages 450–464. Springer, 2010.

Digital Library

[52]

K. Zee, V. Kuncak, and M. C. Rinard. Full functional verification of linked data structures. In PLDI, pages 349–361. ACM, 2008.

Digital Library

Cited By

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Dang HJung JChoi JNguyen DMansky WKang JDreyer DJhala RDillig I(2022)Compass: strong and compositional library specifications in relaxed memory separation logicProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523451(792-808)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523451
Feldman YKhyzha AEnea CMorrison ANanevski ARinetzky NShoham S(2020)Proving highly-concurrent traversals correctProceedings of the ACM on Programming Languages10.1145/34281964:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428196
Show More Cited By

Index Terms

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

Mechanized verification of fine-grained concurrent programs
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated ...
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects
OOPSLA '16

Designing efficient concurrent objects often requires abandoning the standard specification technique of linearizability in favor of more relaxed correctness conditions. However, the variety of alternatives makes it difficult to choose which condition ...
Linearizable counting networks
Summary
The counting problem requires n asynchronous processes to assign themselves successive values. A solution is linearizable if the order of the values assigned reflects the real-time order in which they were requested. Linearizable counting lies at ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

October 2016

915 pages

ISBN:9781450344449

DOI:10.1145/2983990

General Chair:
Eelco Visser
Delft University of Technology, Netherlands
,
Program Chair:
Yannis Smaragdakis
University of Athens, Greece

ACM SIGPLAN Notices Volume 51, Issue 10
OOPSLA '16
October 2016
915 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3022671
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2016 ACM.

© 2016 Association for Computing Machinery. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the United States Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGAda: ACM Special Interest Group on Ada Programming Language

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 October 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '16

Sponsor:

SIGPLAN

SPLASH '16: Conference on Systems, Programming, Languages, and Applications: Software for Humanity

November 2 - 4, 2016

Amsterdam, Netherlands

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
224
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Dang HJung JChoi JNguyen DMansky WKang JDreyer DJhala RDillig I(2022)Compass: strong and compositional library specifications in relaxed memory separation logicProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523451(792-808)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523451
Feldman YKhyzha AEnea CMorrison ANanevski ARinetzky NShoham S(2020)Proving highly-concurrent traversals correctProceedings of the ACM on Programming Languages10.1145/34281964:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428196
Krishna SPatel NShasha DWies TDonaldson ATorlak E(2020)Verifying concurrent search structure templatesProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386029(181-196)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3386029
Tassarotti JHarper R(2019)A separation logic for concurrent randomized programsProceedings of the ACM on Programming Languages10.1145/32903773:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290377
Emmi MEnea C(2019)Weak-consistency specification via visibility relaxationProceedings of the ACM on Programming Languages10.1145/32903733:POPL(1-28)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290373
Peterson CLaBorde PDechev DGuéhéneuc YKhomh FSarro F(2019)CCSpecProceedings of the 27th International Conference on Program Comprehension10.1109/ICPC.2019.00041(220-230)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICPC.2019.00041
Bozga MIosif RSifakis J(2023)Verification of component-based systems with recursive architecturesTheoretical Computer Science10.1016/j.tcs.2022.10.022940(146-175)Online publication date: Jan-2023
https://doi.org/10.1016/j.tcs.2022.10.022
Ahrens EBozga MIosif RKatoen J(2022)Reasoning about distributed reconfigurable systemsProceedings of the ACM on Programming Languages10.1145/35632936:OOPSLA2(145-174)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563293
Cook VPeterson CPainter ZDechev D(2022)Quantifiability: a concurrent correctness condition modeled in vector spaceComputing10.1007/s00607-022-01092-3105:5(955-978)Online publication date: 7-Jun-2022
https://doi.org/10.1007/s00607-022-01092-3
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents