research-article

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement

Authors:

Yannick Zakowski,

Delphine Demange,

David PichardieAuthors Info & Claims

SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

Pages 1881 - 1890

https://doi.org/10.1145/3167132.3167333

Published: 09 April 2018 Publication History

Abstract

Compiling concurrent and managed languages involves implementing sophisticated interactions between client code and the runtime system. An emblematic runtime service, whose implementation is particularly error-prone, is concurrent garbage collection. In a recent work [31], we implement an on-the-fly concurrent garbage collector, and formally prove its functional correctness in the Coq proof assistant. The garbage collector is implemented in a compiler intermediate representation featuring abstract concurrent data structures.

The present paper extends this work by considering the concrete implementation of some of these abstract concurrent data structures. We formalize, in the Coq proof assistant, a theorem establishing the semantic correctness of a compiling pass which translates abstract, atomic data structures into their concrete, fine-grained concurrent implementations.

At the crux of the proof lies a generic result establishing once and for all a simulation relation, starting from a carefully crafted rely-guarantee specification. Inspired by the work of Vafeiadis [28], implementations are annotated with linearization points. Semantically, this instrumentation reflects the behavior of abstract data structures.

References

[1]

J. Baker, A. Cunei, T. Kalibern, F. Pizlo, and J. Vitek. 2009. Accurate Garbage Collection in Uncooperative Environments Revisited. Concurrency and Computation: Practice and Experience 21, 12 (2009).

Digital Library

[2]

J. Derrick, G. Schellhorn, and H. Wehrheim. 2011. Mechanically Verified Proof Obligations for Linearizability. TOPLAS, Article 4 (2011).

Digital Library

[3]

T. Domani, E. K. Kolodner, E. Lewis, E. E. Salant, K. Barabash, I. Lahan, Y. Levanoni, E. Petrank, and I. Yanover. 2000. Implementing an On-the-Fly Garbage Collector for Java. In Proc. of ISMM'00.

Digital Library

[4]

B. Dongol and J. Derrick. 2015. Verifying Linearisability: A Comparative Survey. ACM Comput. Surv., Article 19 (Sept. 2015), 43 pages.

Digital Library

[5]

X. Feng, R. Ferreira, and Z. Shao. 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In Proc. of ESOP.

Digital Library

[6]

I. Filipović, P. O'Hearn, N. Rinetzky, and H. Yang. 2009. Abstraction for Concurrent Objects. In Proc. of ESOP.

Digital Library

[7]

P. Gammie, A. L. Hosking, and K. Engelhardt. 2015. Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In Proc. of PLDI 2015.

Digital Library

[8]

G. Gonthier. 1996. Verifying the Safety of a Practical Concurrent Garbage Collector. In Proc. of CAV.

Digital Library

[9]

Klaus Havelund. 1999. Mechanical verification of a garbage collector. Springer Berlin Heidelberg, Berlin, Heidelberg.

[10]

Klaus Havelund and Natarajan Shankar. 1997. A Mechanized Refinement Proof for a Garbage Collector. (1997). Unpublished report, available at http://havelund.com/Publications/gc-paper.ps.

[11]

C. Hawblitzel and E. Petrank. 2009. Automated verification of practical garbage collectors. In Proc of POPL.

Digital Library

[12]

C Hawblitzel, E. Petrank, S. Qadeer, and S Tasiran. 2015. Automated and Modular Refinement Reasoning for Concurrent Programs. In Proc. of CAV.

[13]

F. Henderson. 2002. Accurate Garbage Collection in an Uncooperative Environment. In Proc. of ISMM.

Digital Library

[14]

D. Hendler, N. Shavit, and L. Yerushalmi. 2004. A Scalable Lock-free Stack Algorithm. In Proc. of SPAA.

Digital Library

[15]

M. Herlihy and N. Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.

Digital Library

[16]

M. P. Herlihy and J. M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. TOPLAS (1990).

Digital Library

[17]

S. Jagannathan, V. Laporte, G. Petri, D. Pichardie, and J. Vitek. 2014. Atomicity Refinement for Verified Compilation. TOPLAS (2014).

Digital Library

[18]

C. B.Jones. 1983. Specification and design of (parallel) programs. In IFIP.

[19]

R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proc. of POPL.

Digital Library

[20]

D. Kästner, X. Leroy, S. Blazy, B. Schommer, M. Schmidt, and C. Ferdinand. 2017. Closing the gap - The formally verified optimizing compiler CompCert. In Proc. of SSS'17.

[21]

X. Leroy. 2009. A formally verified compiler back-end. JAR (2009), 363--446.

Digital Library

[22]

H. Liang and X. Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In Proc. of PLDI.

Digital Library

[23]

H. Liang, X. Feng, and M. Fu. 2014. Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations. TOPLAS (2014).

Digital Library

[24]

P. W. O'Hearn. 2007. Resources, concurrency, and local reasoning. TCS (2007).

Digital Library

[25]

David M. Russinoff. 1994. A mechanically verified incremental garbage collector. Formal Aspects of Computing 6, 4 (1994).

[26]

I. Sergey, A. Nanevski, and A. Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In Proc. of PLDI.

Digital Library

[27]

R. K. Treiber. 1986. Systems Programming: Coping with Parallelism. (1986). Technical Report RJ 5118. IBM Almaden Research Center.

[28]

V. Vafeiadis. 2007. Modular Fine-Grained Concurrency Verification. Ph.D. Dissertation. University of Cambridge.

[29]

V. Vafeiadis and M. J. Parkinson. 2007. A Marriage of Rely/Guarantee and Separation Logic. In Proc. of CONCUR.

Digital Library

[30]

Yannick Zakowski and David Cachera and Delphine Demange and David Pichardie. 2017. Verified Compilation of Linearizable Data Structures - Formal Development. (2017). http://www.irisa.fr/celtique/ext/simulin/.

[31]

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, and Jan Vitek. 2017. Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. In Proc. of ITP.

Cited By

Mével GJourdan J(2021)Formal verification of a concurrent bounded queue in a weak memory modelProceedings of the ACM on Programming Languages10.1145/34735715:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473571
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2019)Verifying a Concurrent Garbage Collector with a Rely-Guarantee MethodologyJournal of Automated Reasoning10.1007/s10817-018-9489-x63:2(489-515)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9489-x
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2017)Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyInteractive Theorem Proving10.1007/978-3-319-66107-0_31(496-513)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_31

Index Terms

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement
1. Theory of computation

Recommendations

Strongly linearizable implementations: possibilities and impossibilities
PODC '12: Proceedings of the 2012 ACM symposium on Principles of distributed computing

Herlihy and Wing [11] established that the set of possible outcomes of a shared memory distributed algorithm remains unchanged when atomic objects are replaced by their linearizable implementations. Since then, linearizability has been the correctness ...
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures

Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts ...
Mechanically verified proof obligations for linearizability

Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

April 2018

2327 pages

ISBN:9781450351911

DOI:10.1145/3167132

Conference Chairs:
Hisham M. Haddad
Kennesaw State University
,
Roger L. Wainwright
University of Tulsa
,
Richard Chbeir
University of Pau & Pays Adour, France

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC 2018

Sponsor:

SIGAPP

SAC 2018: Symposium on Applied Computing

April 9 - 13, 2018

Pau, France

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
58
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mével GJourdan J(2021)Formal verification of a concurrent bounded queue in a weak memory modelProceedings of the ACM on Programming Languages10.1145/34735715:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473571
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2019)Verifying a Concurrent Garbage Collector with a Rely-Guarantee MethodologyJournal of Automated Reasoning10.1007/s10817-018-9489-x63:2(489-515)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9489-x
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2017)Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyInteractive Theorem Proving10.1007/978-3-319-66107-0_31(496-513)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_31

View Options

Get Access

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