Formal derivation of concurrent garbage collectors
From MaRDI portal
Publication:3575280
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.
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
Cited in
(11)- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- A fully concurrent garbage collector for functional programs on multicore processors
- A verified generational garbage collector for CakeML
- Smooth coalgebra: testing vector analysis
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- A verified generational garbage collector for CakeML
- Correctness of a concurrent object collector for actor languages
- Colimits for concurrent collectors
- From Gödel's incompleteness theorem to the completeness of bot beliefs (extended abstract)
- scientific article; zbMATH DE number 3990849 (Why is no real title available?)
- Developments in concurrent Kleene algebra
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)
