Formal Derivation of Concurrent Garbage Collectors

Dusko Pavlovic, Peter Pepper, Douglas R. Smith

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    20 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 languageEnglish
    Title of host publicationMathematics of Program Construction
    Subtitle of host publication10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings
    EditorsClaude Bolduc, Jules Desharnais, Béchir Ktari
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages353-376
    Number of pages24
    ISBN (Electronic)978-3-642-13321-3
    ISBN (Print)978-3-642-13320-6
    DOIs
    Publication statusPublished - Jun 2010
    Event10th International Conference on Mathematics of Program Construction, MPC 2010 - Québec City, Canada
    Duration: 21 Jun 201023 Jun 2010
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume6120
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference10th International Conference on Mathematics of Program Construction, MPC 2010
    Abbreviated titleMPC
    CountryCanada
    CityQuébec City
    Period21/06/1023/06/10

    Keywords

    • Garbage collection
    • Formal derivation
    • Abstract problem
    • Live node
    • Garbage collector

    Fingerprint

    Dive into the research topics of 'Formal Derivation of Concurrent Garbage Collectors'. Together they form a unique fingerprint.

    Cite this