Memoised Garbage Collection for Software Model Checking

Viet Yen Nguyen, Theo C. Ruys

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

    4 Citations (Scopus)
    18 Downloads (Pure)

    Abstract

    Virtual machine based software model checkers like JPF and MOONWALKER spend up to half of their verification time on garbage collection. This is no surprise as after nearly each transition the heap has to be cleaned from garbage. To improve this, this paper presents the Memoised Garbage Collection (MGC) algorithm, which exploits the (typical) locality of transitions to incrementally perform garbage collection. MGC tracks the depths of objects efficiently and only purges objects whose depths have become infinite, hence unreachable. MGC was experimentally evaluated via an implementation in our model checker MOONWALKER and benchmarks using the parallel Java Grande Forum benchmark suite. By using MGC, a performance increase up to 78% was measured over the traditional Mark&Sweep implementation.

    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    Subtitle of host publication15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings
    EditorsStefan Kowalewski, Anna Philippou
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages201-214
    Number of pages14
    ISBN (Electronic)978-3-642-00768-2
    ISBN (Print)978-3-642-00767-5
    DOIs
    Publication statusPublished - Mar 2009
    Event15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009 - York, United Kingdom
    Duration: 22 Mar 200929 Mar 2009
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume5505
    ISSN (Print)0302-9743
    NameTheoretical Computer Science and General Issues
    PublisherSpringer
    ISSN (Print)2512-2010
    ISSN (Electronic)2512-2029

    Conference

    Conference15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009
    Abbreviated titleTACAS
    Country/TerritoryUnited Kingdom
    CityYork
    Period22/03/0929/03/09

    Keywords

    • FMT-MC: MODEL CHECKING
    • n/a OA procedure

    Fingerprint

    Dive into the research topics of 'Memoised Garbage Collection for Software Model Checking'. Together they form a unique fingerprint.

    Cite this