Parallel Recursive State Compression for Free

Alfons Laarman, Jan Cornelis van de Pol, M. Weber

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

    75 Downloads (Pure)

    Abstract

    State space exploration is a basic solution to many verification problems, but is limited by time and memory usage. Due to physical limits in modern CPUs, sequential exploration algorithms do not benefit automatically from the next generation of processors anymore, hence the need for multi-core solutions. This paper focuses on reducing memory usage in enumerative model checking, while maintaining the multi-core scalability obtained in earlier work. We present a tree-based multi-core compression method, which works by leveraging sharing among sub-vectors of state vectors. An algorithmic analysis of both worst-case and optimal compression ratios shows the potential to compress even large states to a small constant on average (8 bytes). Our experiments demonstrate that this holds up in practice: the median compression ratio of 279 measured experiments is within 17% of the optimum for tree compression, and five times better than the median compression ratio of SPIN's COLLAPSE compression. Our algorithms are implemented in the LTSmin tool, and our experiments show that for model checking, multi-core tree compression pays its own way: it comes virtually without overhead compared to the fastest hash table-based methods.
    Original languageUndefined
    Title of host publicationProceedings of the 18th International SPIN Workshop, SPIN 2011
    EditorsAlex Groce, Madanlal Musuvathi
    Place of Publicationberlin
    PublisherSpringer
    Pages38-56
    Number of pages18
    ISBN (Print)978-3-642-22305-1
    DOIs
    Publication statusPublished - 14 Jul 2011
    Event18th International SPIN Workshop on Model Checking of Software 2011 - Snow Bird, United States
    Duration: 14 Jul 201115 Jul 2011
    Conference number: 18

    Publication series

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

    Workshop

    Workshop18th International SPIN Workshop on Model Checking of Software 2011
    CountryUnited States
    CitySnow Bird
    Period14/07/1115/07/11

    Keywords

    • METIS-277629
    • Multi-Core
    • Model Checking
    • IR-77024
    • CR-D.2.4
    • EWI-20146
    • tree-based algorithm
    • incremental algorithm
    • Parallel
    • state space compression

    Cite this