Formal Derivation of Concurrent Garbage Collectors

Dusko Pavlovic; Peter Pepper; Douglas R. Smith

doi:10.1007/978-3-642-13321-3_20

Formal Derivation of Concurrent Garbage Collectors

Dusko Pavlovic
, Peter Pepper
, Douglas R. Smith

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

23 Citations (Scopus)

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.

Original language	English
Title of host publication	Mathematics of Program Construction
Subtitle of host publication	10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings
Editors	Claude Bolduc, Jules Desharnais, Béchir Ktari
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	353-376
Number of pages	24
ISBN (Electronic)	978-3-642-13321-3
ISBN (Print)	978-3-642-13320-6
DOIs	https://doi.org/10.1007/978-3-642-13321-3_20
Publication status	Published - Jun 2010
Event	10th International Conference on Mathematics of Program Construction, MPC 2010 - Québec City, Canada Duration: 21 Jun 2010 → 23 Jun 2010 Conference number: 10

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	6120
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Conference on Mathematics of Program Construction, MPC 2010
Abbreviated title	MPC
Country/Territory	Canada
City	Québec City
Period	21/06/10 → 23/06/10

Keywords

Garbage collection
Formal derivation
Abstract problem
Live node
Garbage collector

Access to Document

10.1007/978-3-642-13321-3_20

Cite this

Pavlovic, D., Pepper, P., & Smith, D. R. (2010). Formal Derivation of Concurrent Garbage Collectors. In C. Bolduc, J. Desharnais, & B. Ktari (Eds.), Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings (pp. 353-376). (Lecture Notes in Computer Science; Vol. 6120). Springer. https://doi.org/10.1007/978-3-642-13321-3_20

Pavlovic, Dusko ; Pepper, Peter ; Smith, Douglas R. / Formal Derivation of Concurrent Garbage Collectors. Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings. editor / Claude Bolduc ; Jules Desharnais ; Béchir Ktari. Berlin, Heidelberg : Springer, 2010. pp. 353-376 (Lecture Notes in Computer Science).

@inproceedings{8e4d709d40984bf4888eff5da01b027e,

title = "Formal Derivation of Concurrent Garbage Collectors",

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

keywords = "Garbage collection, Formal derivation, Abstract problem, Live node, Garbage collector",

author = "Dusko Pavlovic and Peter Pepper and Smith, \{Douglas R.\}",

year = "2010",

month = jun,

doi = "10.1007/978-3-642-13321-3\_20",

language = "English",

isbn = "978-3-642-13320-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "353--376",

editor = "Claude Bolduc and Jules Desharnais and B{\'e}chir Ktari",

booktitle = "Mathematics of Program Construction",

address = "Germany",

note = "10th International Conference on Mathematics of Program Construction, MPC 2010, MPC ; Conference date: 21-06-2010 Through 23-06-2010",

}

Pavlovic, D, Pepper, P & Smith, DR 2010, Formal Derivation of Concurrent Garbage Collectors. in C Bolduc, J Desharnais & B Ktari (eds), Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6120, Springer, Berlin, Heidelberg, pp. 353-376, 10th International Conference on Mathematics of Program Construction, MPC 2010, Québec City, Quebec, Canada, 21/06/10. https://doi.org/10.1007/978-3-642-13321-3_20

Formal Derivation of Concurrent Garbage Collectors. / Pavlovic, Dusko; Pepper, Peter; Smith, Douglas R.
Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings. ed. / Claude Bolduc; Jules Desharnais; Béchir Ktari. Berlin, Heidelberg: Springer, 2010. p. 353-376 (Lecture Notes in Computer Science; Vol. 6120).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formal Derivation of Concurrent Garbage Collectors

AU - Pavlovic, Dusko

AU - Pepper, Peter

AU - Smith, Douglas R.

N1 - Conference code: 10

PY - 2010/6

Y1 - 2010/6

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

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

KW - Garbage collection

KW - Formal derivation

KW - Abstract problem

KW - Live node

KW - Garbage collector

U2 - 10.1007/978-3-642-13321-3_20

DO - 10.1007/978-3-642-13321-3_20

M3 - Conference contribution

SN - 978-3-642-13320-6

T3 - Lecture Notes in Computer Science

SP - 353

EP - 376

BT - Mathematics of Program Construction

A2 - Bolduc, Claude

A2 - Desharnais, Jules

A2 - Ktari, Béchir

PB - Springer

CY - Berlin, Heidelberg

T2 - 10th International Conference on Mathematics of Program Construction, MPC 2010

Y2 - 21 June 2010 through 23 June 2010

ER -

Pavlovic D, Pepper P, Smith DR. Formal Derivation of Concurrent Garbage Collectors. In Bolduc C, Desharnais J, Ktari B, editors, Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings. Berlin, Heidelberg: Springer. 2010. p. 353-376. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-13321-3_20

Formal Derivation of Concurrent Garbage Collectors

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this