research-article

Relaxing safely: verified on-the-fly garbage collection for x86-TSO

Authors:

Antony L. Hosking,

Kai EngelhardtAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 6

Pages 99 - 109

https://doi.org/10.1145/2813885.2738006

Published: 03 June 2015 Publication History

Abstract

We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.

References

[1]

S. Abraham and J. Patel. Parallel garbage collection on a virtual memory system. In International Conference on Parallel Processing, pages 243–246, University Park, Pennsylvania, Aug. 1987.

[2]

J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig. Software verification for weak memory via program transformation. In European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 512–532, Rome, Italy, Mar. 2013. Springer.

Digital Library

[3]

E. Cohen and B. Schirmer. From total store order to sequential consistency: A practical reduction theorem. In International Conference on Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 403–418, Edinburgh, Scotland, July 2010.

Digital Library

[4]

Springer.

[5]

S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In International Conference on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 160–171, Trento, Italy, July 1999. Springer.

Digital Library

[6]

W. P. de Roever, F. S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume 54 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.

Digital Library

[7]

E. W. Dijkstra, L. Lamport, A. J. Martin, C. S. Scholten, and E. F. M. Steffens. On-the-fly garbage collection: An exercise in cooperation. Commun. ACM, 21(11):966–975, Nov. 1978.

Digital Library

[8]

359655.

[9]

D. Doligez and G. Gonthier. Portable, unobtrusive garbage collection for multiprocessor systems. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 70–83, Portland, Oregon, Jan. 1994.

Digital Library

[10]

D. Doligez and X. Leroy. A concurrent generational garbage collector for a multi-threaded implementation of ML. In ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 113–123, Charleston, South Carolina, Jan. 1993.

Digital Library

[11]

158511.158611.

[12]

M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103(2): 235–271, Sept. 1992.

Digital Library

[13]

X. Feng. Local rely-guarantee reasoning. In ACM SIGPLAN Symposium on Principles of Programming Languages, pages 315–327, Savannah, Georgia, Jan. 2009.

Digital Library

[14]

G. Gonthier. Verifying the safety of a practical concurrent garbage collector. In International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 462–465, New Brunswick, New Jerseu, July–Aug. 1996. Springer. 3-540-61474-5_103.

Digital Library

[15]

D. Gries. An exercise in proving parallel programs correct. Commun. ACM, 20(12):921–930, Dec. 1977.

Digital Library

[16]

C. Hawblitzel and E. Petrank. Automated verification of practical garbage collectors. In ACM SIGPLAN Symposium on Principles of Programming Languages, pages 441–453, Savannah, GA, Jan. 2009.

Digital Library

[17]

[18]

S. Jagannathan, V. Laporte, G. Petri, D. Pichardie, and J. Vitek. Atomicity refinement for verified compilation. ACM Trans. Prog. Lang. Syst., 36(2):6:1–30, Apr. 2014.

Digital Library

[19]

R. Jones, A. Hosking, and E. Moss. The Garbage Collection Handbook: The Art of Automatic Memory Management. CRC Applied Algorithms and Data Structures. Chapman & Hall, Aug. 2012.

Digital Library

[20]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In ACM SIGOPS Symposium on Operating Systems Principles, pages 207– 220, Big Sky Resort, Montana, Oct. 2009.

Digital Library

[21]

1629596.

[22]

H. T. Kung and S. W. Song. An efficient parallel garbage collection system and its correctness proof. In Symposium on Foundations of Computer Science, pages 120–131, Providence, Rhode Island, Oct. 1977. IEEE.

Digital Library

[23]

L. Lamport. Garbage collection with multiple processes: an exercise in parallelism. In International Conference on Parallel Processing, pages 50–54, 1976.

[24]

L. Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.

Digital Library

[25]

L. Lamport. Who builds a house without drawing blueprints? Commun. ACM, 58(4):38–41, Apr. 2015.

Digital Library

[26]

C. Lin, Y. Chen, and B. Hua. Verification of an incremental garbage collector in Hoare-style logic. International Journal of Software and Informatics, 3(1):67–88, Mar. 2009.

[27]

J. McCarthy. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM, 3(4):184–195, Apr. 1960.

Digital Library

[28]

A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 468–479, San Diego, California, June 2007. 1250734.1250788.

Digital Library

[29]

A. McCreight, T. Chevalier, and A. Tolmach. A certified framework for compiling and executing garbage-collected languages. In ACM SIGPLAN International Conference on Functional Programming, pages 273–284, Baltimore, Maryland, Sept. 2010.

Digital Library

[30]

1863584.

[31]

R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, New Jersey, 1989.

Digital Library

[32]

S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In European Conference on Object-Oriented Programming, volume 6183 of Lecture Notes in Computer Science, pages 478–503, Maribor, Slovenia, June 2010. Springer. 978-3-642-14107-2_23.

Digital Library

[33]

S. Park and D. L. Dill. An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers, 48(2):227– 235, 1999.

Digital Library

[34]

D. Pavlovic, P. Pepper, and D. R. Smith. Formal derivation of concurrent garbage collectors. In International Conference on Mathematics of Program Construction, volume 6120, pages 353–376, Québec City, Canada, June 2010. Springer. 20.

Digital Library

[35]

A. M. Pitts. Operational semantics and program equivalence. In International Summer School on Applied Semantics, Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, pages 378–412. Springer, Caminha, Portugal, Sept. 2000. 3-540-45699-6_8.

Digital Library

[36]

F. Pizlo, L. Ziarek, P. Maj, A. L. Hosking, E. Blanton, and J. Vitek. Schism: Fragmentation-tolerant real-time garbage collection. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 146–159, Toronto, Canada, June 2010. 1806596.1806615.

Digital Library

[37]

T. Ridge. Verifying distributed systems: the operational approach. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 429–440, Savannah, Georgia, Jan. 2009. 1145/1480881.1480934.

Digital Library

[38]

T. Ridge. A rely-guarantee proof system for x86-TSO. In International Conference on Verified Software: Theories, Tools, Experiments, volume 6217 of Lecture Notes in Computer Science, pages 55–70, Edinburgh, Scotland, Aug. 2010. Springer. 4.

Digital Library

[39]

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 175–186, San Jose, California, June 2011.

Digital Library

[40]

J. Sevcík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60(3):22, 2013.

Digital Library

[41]

P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89–97, July 2010. 1785414.1785443.

Digital Library

[42]

N. Torp-Smith, L. Birkedal, and J. C. Reynolds. Local reasoning about a copying garbage collector. ACM Trans. Prog. Lang. Syst., 30(4), July 2008.

Digital Library

[43]

A. Turon, V. Vafeiadis, and D. Dreyer. GPS: Navigating weak memory with ghosts, protocols, and separation. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 691–707, Portland, Oregon, Oct. 2014. 1145/2660193.2660243.

Digital Library

[44]

M. T. Vechev, D. F. Bacon, P. Cheng, and D. Grove. Derivation and evaluation of concurrent collectors. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 341–353, Ottawa, Canada, June 2007.

[45]

M. Wenzel. Shared-memory multiprocessing for interactive theorem proving. In International Conference on Interactive Theorem Proving, volume 7998 of Lecture Notes in Computer Science, pages 418–434, Rennes, France, July 2013. Springer. 978-3-642-39634-2_30.

Digital Library

[46]

G. Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993.

Digital Library

[47]

T. Yuasa. Real-time garbage collection on general-purpose machines. Journal of Systems and Software, 11(3):181–198, Mar. 1990. 1016/0164-1212(90)90084-Y. Introduction Contributions The Verified Collector Abstractions and Invariants The Collector Marking Relaxed Memory: x86-TSO Formal Verification in Isabelle/HOL Model Formal Abstractions and Invariants Concluding Remarks

Digital Library

Cited By

Havelund KShankar N(2024)What Is a Garbage Collector? An Exercise in Compositional RefinementThe Practice of Formal Methods10.1007/978-3-031-66676-6_10(195-215)Online publication date: 4-Sep-2024
https://doi.org/10.1007/978-3-031-66676-6_10
Polito GTesone PPalumbo NDucasse SPrivat J(2023)Heap Fuzzing: Automatic Garbage Collection Testing with Expert-Guided Random Events2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00019(107-116)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00019
Appel ANaumann DDing CMaas M(2020)Verified sequential Malloc/FreeProceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management10.1145/3381898.3397211(48-59)Online publication date: 16-Jun-2020
https://dl.acm.org/doi/10.1145/3381898.3397211
Show More Cited By

Index Terms

Relaxing safely: verified on-the-fly garbage collection for x86-TSO

Recommendations

Relaxing safely: verified on-the-fly garbage collection for x86-TSO
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed ...
Age-based garbage collection

Modern generational garbage collectors look for garbage among the young objects, because they have high mortality; however, these objects include the very youngest objects, which clearly are still live. We introduce new garbage collection algorithms, ...
Age-based garbage collection
OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications

Modern generational garbage collectors look for garbage among the young objects, because they have high mortality; however, these objects include the very youngest objects, which clearly are still live. We introduce new garbage collection algorithms, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 6

PLDI '15

June 2015

630 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2813885

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2015
630 pages
ISBN:9781450334686
DOI:10.1145/2737924
General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

Copyright © 2015 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: 03 June 2015

Published in SIGPLAN Volume 50, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
368
Total Downloads

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

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Havelund KShankar N(2024)What Is a Garbage Collector? An Exercise in Compositional RefinementThe Practice of Formal Methods10.1007/978-3-031-66676-6_10(195-215)Online publication date: 4-Sep-2024
https://doi.org/10.1007/978-3-031-66676-6_10
Polito GTesone PPalumbo NDucasse SPrivat J(2023)Heap Fuzzing: Automatic Garbage Collection Testing with Expert-Guided Random Events2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00019(107-116)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00019
Appel ANaumann DDing CMaas M(2020)Verified sequential Malloc/FreeProceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management10.1145/3381898.3397211(48-59)Online publication date: 16-Jun-2020
https://dl.acm.org/doi/10.1145/3381898.3397211
Sandberg Ericsson AMyreen MÅman Pohjola J(2019)A Verified Generational Garbage Collector for CakeMLJournal of Automated Reasoning10.1007/s10817-018-9487-z63:2(463-488)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9487-z
Havelund KShankar N(2019)A Refinement Proof for a Garbage CollectorFrom Reactive Systems to Cyber-Physical Systems10.1007/978-3-030-31514-6_6(73-103)Online publication date: 23-Sep-2019
https://doi.org/10.1007/978-3-030-31514-6_6
Österlund ELöwe W(2018)Self-adaptive concurrent componentsAutomated Software Engineering10.1007/s10515-017-0219-025:1(47-99)Online publication date: 1-Mar-2018
https://dl.acm.org/doi/10.1007/s10515-017-0219-0
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
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
Yang AWrigstad T(2022)Deep Dive into ZGC: A Modern Garbage Collector in OpenJDKACM Transactions on Programming Languages and Systems10.1145/353853244:4(1-34)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3538532
Sivaramakrishnan KDolan SWhite LJaffer SKelly TSahoo AParimala SDhiman AMadhavapeddy A(2020)Retrofitting parallelism onto OCamlProceedings of the ACM on Programming Languages10.1145/34089954:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408995
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.

Figures

Tables

Media

View Issue’s Table of Contents