article

Correctness-preserving derivation of concurrent garbage collection algorithms

Authors:

Martin T. Vechev,

David F. BaconAuthors Info & Claims

ACM SIGPLAN Notices, Volume 41, Issue 6

Pages 341 - 353

https://doi.org/10.1145/1133255.1134022

Published: 11 June 2006 Publication History

Abstract

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 validation of one algorithm does not carry over to others.As programs with low latency requirements written in garbagecollected languages become part of society's mission-critical infrastructure, it is imperative that we raise the level of confidence in the correctness of the underlying system, and that we understand the trade-offs inherent in our algorithmic choice.In this paper we present correctness-preserving transformations that can be applied to an initial abstract concurrent garbage collection algorithm which is simpler, more precise, and easier to prove correct than algorithms used in practice--but also more expensive and with less concurrency. We then show how both pre-existing and new algorithms can be synthesized from the abstract algorithm by a series of our transformations. We relate the algorithms formally using a new definition of precision, and informally with respect to overhead and concurrency.This provides many insights about the nature of concurrent collection, allows the direct synthesis of new and useful algorithms, reduces the burden of proof to a single simple algorithm, and lays the groundwork for the automated synthesis of correct concurrent collectors.

References

[1]

APPEL, A.W., ELLIS, J. R., AND LI, K. Real-time concurrent collection on stock multiprocessors. In Proceedings of the SIGPLAN'88 Conference on Programming Language Design and Implementation (Atlanta, Georgia, June 1988). SIGPLAN Notices, 23, 7 (July), 11--20.]]

Digital Library

[2]

AZATCHI, H., LEVANONI, Y., PAZ, H., AND PETRANK, E. An on the-fly mark and sweep garbage collector based on sliding views. In Proceedings of the 18th ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications (Oct 2003), ACM Press, pp. 269--281.]]

Digital Library

[3]

BACON, D. F., ATTANASIO, C. R., LEE, H. B., RAJAN, V. T., AND SMITH, S. Java without the coffee breaks: A nonintrusive multiprocessor garbage collector. In Proc. of the SIGPLAN Conference on Programming Language Design and Implementation (Snowbird, Utah, June 2001). SIGPLAN Notices, 36, 5 (May), 92--103.]]

Digital Library

[4]

BACON, D. F., CHENG, P., AND RAJAN, V. T. A real-time garbage collector with low overhead and consistent utilization. In Proceedings of the 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New Orleans, Louisiana, Jan. 2003). SIGPLAN Notices, 38, 1, 285--298.]]

Digital Library

[5]

BAKER, H. G. List processing in real-time on a serial computer. Commun. ACM 21, 4 (Apr. 1978), 280--294.]]

Digital Library

[6]

BAKER, H. G. The Treadmill, real-time garbage collection without motion sickness. SIGPLAN Notices 27, 3 (Mar. 1992), 66--70.]]

Digital Library

[7]

BARABASH, K., OSSIA, Y., AND PETRANK, E. Mostly concurrent garbage collection revisited. In Proceedings of the 18th ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications (Oct 2003), ACM Press, pp. 255--268.]]

Digital Library

[8]

BARTH, J. M. Shifting garbage collection overhead to compile time. Commun. ACM 20, 7 (July 1977), 513--518.]]

Digital Library

[9]

BEN-ARI, M. Algorithms for on-the-fly garbage collection. ACM Trans. Program. Lang. Syst. 6, 3 (1984), 333--344.]]

Digital Library

[10]

BIRKEDAL, L., TORP-SMITH, N., AND REYNOLDS, J. C. Local reasoning about a copying garbage collector. In Proc. of the Thirty-first ACM Symposium on Principles of Programming Languages (Venice, Italy, 2004). SIGPLAN Notices, 39, 1, 220--231.]]

Digital Library

[11]

BOEHM, H.-J., DEMERS, A. J., AND SHENKER, S. Mostly parallel garbage collection. In Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (Toronto, Ontario, 1991). SIGPLAN Notices, 26, 6, 157--164.]]

Digital Library

[12]

BOWMAN, H., DERRICK, J., AND JONES, R. E. Modelling garbage collection algorithms. In Proceedings of International Computing Symposium (January 1994).]]

[13]

BROOKS, R. A. Trading data space for reduced time and code space in real-time garbage collection on stock hardware. In Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming (Austin, Texas, Aug. 1984), G. L. Steele, Ed., pp. 256--262.]]

Digital Library

[14]

BROOKS, S., AND O'HEARN, P. Resources, concurrency and local reasoning. Fifteenth International Conference on Concurrency Theory 3170 (2004).]]

[15]

BURDY, L. B vs. Coq to prove a garbage collector. In Fourteenth International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings (Sept. 2001), R. J. Boulton and P. B. Jackson, Eds., Report EDI-INF-RR-0046, Division of Informatics, University of Edinburgh, pp. 85--97.]]

[16]

CHEADLE, A. M., FIELD, A. J., MARLOW, S., PEYTON JONES, S. L., AND WHILE, R. L. Non-stop Haskell. In Proc. of the Fifth International Conference on Functional Programming (Montreal, Quebec, Sept. 2000). SIGPLAN Notices, 35, 9, 257--267.]]

Digital Library

[17]

CHENG, P., AND BLELLOCH, G. E. A parallel, real-time garbage collector. In Proceedings of the ACM Conference on Programming language design and implementation, ACM Press, pp. 125--136.]]

Digital Library

[18]

CLICK, C., TENE, G., AND WOLF, M. The pauseless GC algorithm. In Proc. of the First ACM/Usenix Conference on Virtual ExecutionEnvironments (Chicago, Illinois, June 2005).]]

Digital Library

[19]

DEMMERS, A., WEISER, M., HAYES, B., BOEHM, H., BOBROW, D., AND SHENKER, S. Combining generational and conservative garbage collection: framework and implementations. 261--269.]]

[20]

DEWAR, R. B. K., SHIRAR, M., AND WEIXELBAUM, E. Transformational derivation of a garbage collection algorithm. ACM Trans. Program. Lang. Syst. 4, 4 (1982), 650--667.]]

Digital Library

[21]

DIJKSTRA, E. W., LAMPORT, L., MARTIN, A. J., SCHOLTEN, C. S., AND STEFFENS, E. F. M. On-the-fly garbage collection: an exercise in cooperation. Commun. ACM 21, 11 (1978), 966--975.]]

Digital Library

[22]

DOLIGEZ, D., AND GONTHIER, G. Portable, unobtrusive garbage collection for multiprocessor systems. In Conf. Record of the Twenty-First ACM Symposium on Principles of Programming Languages (Jan. 1994), pp. 70--83.]]

Digital Library

[23]

DOLIGEZ, D., AND LEROY, X. A concurrent generational garbage collector for a multi-threaded implementation of ML. In Conf. Record of the Twentieth ACM Symposium on Principles of Programming Languages (Jan. 1993), pp. 113--123.]]

Digital Library

[24]

DOMANI, T., KOLODNER, E. K., AND PETRANK, E. A generational on-the-fly garbage collector for Java. In Proc. of the SIGPLAN Conference on Programming Language Design and Implementation (June 2000). SIGPLAN Notices, 35, 6, 274--284.]]

Digital Library

[25]

HAVELUND, K. Mechanical verification of a garbage collector. In Fourth International Workshop on Formal Methods for Parallel Programming: Theory and Applications (San Juan, Puerto Rico, 1999), J. D. P. Rolim et al., Eds., vol. 1586 of Lecture Notes in Computer Science, pp. 1258--1283.]]

Digital Library

[26]

HENRIKSSON, R. Scheduling Garbage Collection in Embedded Systems. PhD thesis, Lund Institute of Technology, July 1998.]]

[27]

HUDSON, R. L., AND MOSS, E. B. Incremental garbage collection for mature objects. In Proc. of the International Workshop on Memory Management (St. Malo, France, Sept. 1992), Y. Bekkers and J. Cohen, Eds., vol. 637 of Lecture Notes in Computer Science.]]

Digital Library

[28]

JACKSON, P. B. Verifying a garbage collection algorithm. In Theorem Proving in Higher Order Logics, 11th International Conference (1998), LNCS, Springer-Verlag, pp. 225--244.]]

Digital Library

[29]

JOHNSTONE, M. S. Non-Compacting Memory Allocation and Real-Time Garbage Collection. PhD thesis, University of Texas at Austin, Dec. 1997.]]

Digital Library

[30]

JONES, R., AND LINS, R. Garbage Collection. John Wiley and Sons, 1996.]]

[31]

LAMPORT, L. Garbage collection with multiple processes: an exercise in parallelism. In Proc. of the 1976 International Conference on Parallel Processing (1976), pp. 50--54.]]

[32]

LAROSE, M., AND FEELEY, M. A compacting incremental collector and its performance in a production quality compiler. In Proc. of the First International Symposium on Memory Management (Vancouver, B.C., Oct. 1998). SIGPLAN Notices, 34, 3 (Mar., 1999), 1--9.]]

Digital Library

[33]

LEVANONI, Y., AND PETRANK, E. An on-the-fly reference counting garbage collector for java. In Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications (Oct 2001), ACM Press, pp. 367--380.]]

Digital Library

[34]

NETTLES, S., AND O'TOOLE, J. Real-time garbage collection. In Proc. of the SIGPLAN Conference on Programming Language Design and Implementation (June 1993). SIGPLAN Notices, 28, 6, 217--226.]]

Digital Library

[35]

NORTH, S. C., AND REPPY, J. H. Concurrent garbage collection on stock hardware. In Functional Programming Languages and Computer Architecture (Portland, Oregon, Sept. 1987), G. Kahn, Ed., vol. 274 of Lecture Notes in Computer Science, pp. 113--133.]]

Digital Library

[36]

PAVLOVIC, D., PEPPER, P., AND SMITH, D. R. Colimits for concurrent collectors. In Verification: Theory and Practice, essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday (2003), vol. 2772 of LNCS, Springer-Verlag, pp. 568--597.]]

[37]

PIXLEY, C. An incremental garbage collection algorithm for multimutator systems. Distributed Computing 3, 1 6, 3 (Dec. 1988), 41--49.]]

Digital Library

[38]

PRENSA NIETO, L., AND ESPARZA, J. Verifying single and multimutator garbage collectors with Owicki/Gries in Isabelle/HOL. In Mathematical Foundations of Computer Science (MFCS 2000) (2000), M. Nielsen and B. Rovan, Eds., vol. 1893 of LNCS, Springer-Verlag, pp. 619--628.]]

Digital Library

[39]

RUSSINOFF, D. M. A mechanically verified incremental garbage collector. Formal Aspects of Computing 6, 4 (1994), 359--390.]]

[40]

SAGONAS, K., AND WILHELMSSON, J. Message analysisguided allocation and low-pause incremental garbage collection in a concurrent language. In Proc. of the Fourth International Symposium on Memory Management (Vancouver, Canada, 2004), ACM Press, pp. 1--12.]]

Digital Library

[41]

STEELE, G. L. Multiprocessing compactifying garbage collection. Commun. ACM 18, 9 (Sept. 1975), 495--508.]]

Digital Library

[42]

STEELE, G. L. Corrigendum: Multiprocessing compactifying garbage collection. Commun. ACM 19, 6 (June 1976), 354.]]

Digital Library

[43]

VECHEV, M., YAHAV, E., AND BACON, D. Parametric generation of concurrent collection algorithms: Online supplement. http://www.cl.cam.ac.uk/users/mv270/cgcproofs.ps.]]

[44]

VECHEV, M. T., BACON, D. F., CHENG, P., AND GROVE, D. Derivation and evaluation of concurrent collectors. In Proceedings of the Nineteenth European Conference on Object-Oriented Programming (Glasgow, Scotland, July 2005), A. Black, Ed., Lecture Notes in Computer Science, Springer-Verlag.]]

Digital Library

[45]

WADLER, P. L. Analysis of an algorithm for real time garbage collection. Commun. ACM 19, 9 (1976), 491--500.]]

Digital Library

[46]

YUASA, T. Real-time garbage collection on general-purpose machines. Journal of Systems and Software 11, 3 (Mar. 1990), 181--198.]]

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
Franco JClebsch SDrossopoulou SVitek JWrigstad T(2018)Correctness of a Concurrent Object Collector for Actor LanguagesProgramming Languages and Systems10.1007/978-3-319-89884-1_31(885-911)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_31
Jones CYatapanage N(2019)Investigating the limits of rely/guarantee relations based on a concurrent garbage collector exampleFormal Aspects of Computing10.1007/s00165-019-00482-331:3(353-374)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s00165-019-00482-3
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 ...
Correctness-preserving derivation of concurrent garbage collection algorithms
PLDI '06: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 41, Issue 6

Proceedings of the 2006 PLDI Conference

June 2006

426 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1133255

Issue’s Table of Contents

PLDI '06: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2006
438 pages
ISBN:1595933204
DOI:10.1145/1133981
General Chair:
Michael Schwartzbach
University of Aarhus, Denmark
,
Program Chair:
Thomas Ball
Microsoft Research

Copyright © 2006 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: 11 June 2006

Published in SIGPLAN Volume 41, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
701
Total Downloads

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

Reflects downloads up to 21 Nov 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
Franco JClebsch SDrossopoulou SVitek JWrigstad T(2018)Correctness of a Concurrent Object Collector for Actor LanguagesProgramming Languages and Systems10.1007/978-3-319-89884-1_31(885-911)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_31
Jones CYatapanage N(2019)Investigating the limits of rely/guarantee relations based on a concurrent garbage collector exampleFormal Aspects of Computing10.1007/s00165-019-00482-331:3(353-374)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s00165-019-00482-3
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
Chandra KBodik R(2017)Bonsai: synthesis-based reasoning for type systemsProceedings of the ACM on Programming Languages10.1145/31581502:POPL(1-34)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158150
Jones CVelykis AYatapanage N(2017)General Lessons from a Rely/Guarantee DevelopmentDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-69483-2_1(3-22)Online publication date: 17-Oct-2017
https://doi.org/10.1007/978-3-319-69483-2_1
Gammie PHosking AEngelhardt K(2015)Relaxing safely: verified on-the-fly garbage collection for x86-TSOACM SIGPLAN Notices10.1145/2813885.273800650:6(99-109)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2738006
Gammie PHosking AEngelhardt KGrove DBlackburn S(2015)Relaxing safely: verified on-the-fly garbage collection for x86-TSOProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2738006(99-109)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2738006
Wu HJi Z(2015)Improving Trace Precision for Concurrent Garbage Collection on Multicore Platform2015 Fifth International Conference on Instrumentation and Measurement, Computer, Communication and Control (IMCCC)10.1109/IMCCC.2015.316(1493-1496)Online publication date: Sep-2015
https://doi.org/10.1109/IMCCC.2015.316
Portillo-Dominguez AWang MMurphy JMagoni D(2015)Adaptive GC-Aware Load Balancing Strategy for High-Assurance Java Distributed SystemsProceedings of the 2015 IEEE 16th International Symposium on High Assurance Systems Engineering10.1109/HASE.2015.19(68-75)Online publication date: 8-Jan-2015
https://dl.acm.org/doi/10.1109/HASE.2015.19
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