More Web Proxy on the site http://driver.im/

article

CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors

Authors:

Martin T. Vechev,

David F. Bacon,

Noam RinetzkyAuthors Info & Claims

ACM SIGPLAN Notices, Volume 42, Issue 6

Pages 456 - 467

https://doi.org/10.1145/1273442.1250787

Published: 10 June 2007 Publication History

Abstract

Concurrent garbage collectors are notoriously hard to design, implement, and verify. We present a framework for the automatic exploration of a space of concurrent mark-and-sweep collectors. In our framework, the designer specifies a set of "building blocks" from which algorithms can be constructed. These blocks reflect the designer's insights about the coordination between the collector and the mutator. Given a set of building blocks, our framework automatically explores a space of algorithms, using model checking with abstraction to verify algorithms in the space.

We capture the intuition behind some common mark-and-sweep algorithms using a set of building blocks. We utilize our framework to automatically explore a space of more than 1,600,000 algorithms built from these blocks, and derive over 100 correct fine-grained algorithms with various space, synchronization, and precision tradeoffs.

References

[1]

Bar-David, Y., and Taubenfeld, G. Automatic discovery of mutual exclusion algorithms. In Proceedings of the 22nd Annual Symposium on Principles of Distributed Computing (2003).

Digital Library

[2]

Barabash, K., Ossia, Y., and Petrank, E. Mostly concurrent garbage collection revisited. In Proceedings of the 18th ACM conference on Object-oriented programing, systems, languages, and applications (2003).

Digital Library

[3]

Ben-Ari, M. Algorithms for on-the-fly garbage collection. ACM Trans. Program. Lang. Syst. 6, 3 (1984).

Digital Library

[4]

Birkedal, L., Torp-Smith, N., and Reynolds, JC. Local reasoning about a copying garbage collector. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (2004).

Digital Library

[5]

Bowman, H., Derrick, J., and Jones, RE. Modelling garbage collection algorithms. In Proceedings of International Computing Symposium (1994).

[6]

Burdy, L. B vs. Coq to prove a garbage collector. In the 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings (2001).

[7]

Das, M., Lerner, S., and Seigle, M. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (2002).

Digital Library

[8]

Demmers, A., Weiser, M., Hayes, B., Boehm, H., Bobrow, D., and Shenker, S. Combining generational and conservative garbage collection: framework and implementations. In Proceedings of the 17th ACM symposium on Principles of programming languages (1990).

Digital Library

[9]

Dewar, R. BK., Shirar, M., and Weixelbaum, E. Transformational derivation of a garbage collection algorithm. ACM Trans. Program. Lang. Syst. 4, 4 (1982).

Digital Library

[10]

Dijkstra, EW., Lamport, L., Martin, AJ., Scholten, CS., and Steffens, E. FM. On-the-fly garbage collection: an exercise in cooperation. Commun. ACM 21, 11 (1978).

Digital Library

[11]

Gries, D. An exercise in proving parallel programs correct. Commun. ACM 20, 12 (1977).

Digital Library

[12]

Gries, D. Corrigendum. Commun. ACM 21, 12 (December 1978), 1048.

Digital Library

[13]

Hackett, B., and Rugina, R. Region-based shape analysis with tracked locations. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (2005), ACM.

Digital Library

[14]

Havelund, K. Mechanical verification of a garbage collector. In Fourth International Workshop on Formal Methods for Parallel Programming: Theory and Applications (1999).

Digital Library

[15]

Jackson, PB. Verifying a garbage collection algorithm. In Theorem Proving in Higher Order Logics, 11th International Conference (1998).

Digital Library

[16]

Massalin, H. Superoptimizer: a look at the smallest program. In the 2nd International Conference on Architectural Support for Programming Languages and Operating Systems (1987).

Digital Library

[17]

Paulson, L. Isabelle: A Generic Theorem Prover, vol828 of Lecture Notes in Computer Science. 1994.

[18]

Prensa Nieto, L., and Esparza, J. Verifying single and multi-mutator garbage collectors with Owicki/Gries in Isabelle/HOL. In Mathematical Foundations of Computer Science (2000).

Digital Library

[19]

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

[20]

Sagiv, M., Reps, T., and Wilhelm, R. Parametric shape analysis via 3-valued logic. ACM Trans. on Prog. Lang. and Systems 24, 3 (2002).

Digital Library

[21]

Solar-Lezama, A., Rabbah, RM., Bodík, R., and Ebcioglu, K. Programming by sketching for bit-streaming programs. In Proceedings of the ACM Conference on Programming Language Design and Implementation (2005).

Digital Library

[22]

Takahashi, K. Abstraction and Search in Verification by State Exploration. PhD thesis, University of Tokyo, Jan. 2002.

[23]

Vechev, M. Derivation And Evaluation Of Concurrent Collectors. PhD thesis, University of Cambridge, 2007.

[24]

Vechev, MT., Yahav, E., and Bacon, DF. Correctness-preserving derivation of concurrent garbage collection algorithms. In Proceedings of the ACM Conference on Programming Language Design and Implementation/ (2006).

Digital Library

[25]

Yahav, E., and Ramalingam, G. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the ACM conference on Programming language design and implementation/ (2004).

Digital Library

Cited By

Peleg HShoham SYahav EChaudron MCrnkovic IChechik MHarman M(2018)Programming not only by exampleProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180189(1114-1124)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180189
Vechev MYahav EYorsh G(2013)Abstraction-guided synthesis of synchronizationInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0232-315:5-6(413-431)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-012-0232-3
Kuncak VMayer MPiskac RSuter P(2013)Functional synthesis for linear arithmetic and setsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-011-0217-715:5-6(455-474)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-011-0217-7
Show More Cited By

Index Terms

Recommendations

CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

Concurrent garbage collectors are notoriously hard to design, implement, and verify. We present a framework for the automatic exploration of a space of concurrent mark-and-sweep collectors. In our framework, the designer specifies a set of "building ...
Simple concurrent garbage collection almost without synchronization

We present two simple mark and sweep algorithms, A and B, for concurrent garbage collection by a single collector running concurrently with a number of mutators that concurrently modify shared data. Both algorithms are based on the ideas of Ben-Ari's ...
Correctness-preserving derivation of concurrent garbage collection algorithms
Proceedings of the 2006 PLDI Conference

Constructing correct concurrent garbage collection algorithms is notoriously hard. Numerous such algorithms have been proposed, implemented, and deployed - and yet the relationship among them in terms of speed and precision is poorly understood, and the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 42, Issue 6

Proceedings of the 2007 PLDI conference

June 2007

491 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1273442

Issue’s Table of Contents

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2007
508 pages
ISBN:9781595936332
DOI:10.1145/1250734
General Chair:
Jeanne Ferrante
University of California, San Diego, USA
,
Program Chair:
Kathryn S. McKinley
University of Texas at Austin, USA

Copyright © 2007 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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 June 2007

Published in SIGPLAN Volume 42, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
373
Total Downloads

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

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Peleg HShoham SYahav EChaudron MCrnkovic IChechik MHarman M(2018)Programming not only by exampleProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180189(1114-1124)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180189
Vechev MYahav EYorsh G(2013)Abstraction-guided synthesis of synchronizationInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0232-315:5-6(413-431)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-012-0232-3
Kuncak VMayer MPiskac RSuter P(2013)Functional synthesis for linear arithmetic and setsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-011-0217-715:5-6(455-474)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-011-0217-7
Xu BMoss EBlackburn S(2022)Towards a Model Checking Framework for a New Collector FrameworkProceedings of the 19th International Conference on Managed Programming Languages and Runtimes10.1145/3546918.3546923(128-139)Online publication date: 14-Sep-2022
https://dl.acm.org/doi/10.1145/3546918.3546923
Qiu XSolar-Lezama A(2017)Natural synthesis of provably-correct data-structure manipulationsProceedings of the ACM on Programming Languages10.1145/31338891:OOPSLA(1-28)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133889
Ugawa TAbe TMaeda T(2017)Model checking copy phases of concurrent copying garbage collection with various memory modelsProceedings of the ACM on Programming Languages10.1145/31338771:OOPSLA(1-26)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133877
Bodik RJobstmann B(2013)Algorithmic program synthesisInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0287-915:5-6(397-411)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-013-0287-9
Vechev MYahav EYorsh G(2013)Abstraction-guided synthesis of synchronizationInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0232-315:5-6(413-431)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-012-0232-3
Kuncak VMayer MPiskac RSuter P(2013)Functional synthesis for linear arithmetic and setsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-011-0217-715:5-6(455-474)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-011-0217-7
Kuperstein MVechev MYahav E(2012)Automatic inference of memory fencesACM SIGACT News10.1145/2261417.226143843:2(108-123)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2261417.2261438
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 Issue’s Table of Contents