Formal derivation of concurrent garbage collectors

DOI10.1007/978-3-642-13321-3_20zbMATH Open1286.68090arXiv1006.4342OpenAlexW2109524688MaRDI QIDQ3575280FDOQ3575280

Authors: Dusko Pavlovic, Peter Pepper, Douglas R. Smith 

Publication date: 26 July 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verification or on the application of domain-specific templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specification, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection.

Full work available at URL: https://arxiv.org/abs/1006.4342

Recommendations

• Colimits for concurrent collectors
• Formal Verification of an Incremental Garbage Collector
• Simple concurrent garbage collection almost without synchronization
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Verifying a concurrent garbage collector using a rely-guarantee methodology

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (11)

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Correctness of a concurrent object collector for actor languages
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• A verified generational garbage collector for CakeML
• Developments in concurrent Kleene algebra
• Smooth coalgebra: testing vector analysis
• From Gödel's incompleteness theorem to the completeness of bot beliefs (extended abstract)
• A verified generational garbage collector for CakeML
• A fully concurrent garbage collector for functional programs on multicore processors
• Colimits for concurrent collectors
• Title not available (Why is that?)

This page was built for publication: Formal derivation of concurrent garbage collectors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3575280)