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

    74 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

    Laarman, A., van de Pol, J. C., & Weber, M. (2011). Parallel Recursive State Compression for Free. In A. Groce, & M. Musuvathi (Eds.), Proceedings of the 18th International SPIN Workshop, SPIN 2011 (pp. 38-56). (Lecture Notes in Computer Science; Vol. 6823). berlin: Springer. https://doi.org/10.1007/978-3-642-22306-8_4
    Laarman, Alfons ; van de Pol, Jan Cornelis ; Weber, M. / Parallel Recursive State Compression for Free. Proceedings of the 18th International SPIN Workshop, SPIN 2011. editor / Alex Groce ; Madanlal Musuvathi. berlin : Springer, 2011. pp. 38-56 (Lecture Notes in Computer Science).
    @inproceedings{569f63ebea9c4f4c8e44fabcbf445fa3,
    title = "Parallel Recursive State Compression for Free",
    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.",
    keywords = "METIS-277629, Multi-Core, Model Checking, IR-77024, CR-D.2.4, EWI-20146, tree-based algorithm, incremental algorithm, Parallel, state space compression",
    author = "Alfons Laarman and {van de Pol}, {Jan Cornelis} and M. Weber",
    note = "10.1007/978-3-642-22306-8_4",
    year = "2011",
    month = "7",
    day = "14",
    doi = "10.1007/978-3-642-22306-8_4",
    language = "Undefined",
    isbn = "978-3-642-22305-1",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "38--56",
    editor = "Alex Groce and Madanlal Musuvathi",
    booktitle = "Proceedings of the 18th International SPIN Workshop, SPIN 2011",

    }

    Laarman, A, van de Pol, JC & Weber, M 2011, Parallel Recursive State Compression for Free. in A Groce & M Musuvathi (eds), Proceedings of the 18th International SPIN Workshop, SPIN 2011. Lecture Notes in Computer Science, vol. 6823, Springer, berlin, pp. 38-56, 18th International SPIN Workshop on Model Checking of Software 2011, Snow Bird, United States, 14/07/11. https://doi.org/10.1007/978-3-642-22306-8_4

    Parallel Recursive State Compression for Free. / Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M.

    Proceedings of the 18th International SPIN Workshop, SPIN 2011. ed. / Alex Groce; Madanlal Musuvathi. berlin : Springer, 2011. p. 38-56 (Lecture Notes in Computer Science; Vol. 6823).

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

    TY - GEN

    T1 - Parallel Recursive State Compression for Free

    AU - Laarman, Alfons

    AU - van de Pol, Jan Cornelis

    AU - Weber, M.

    N1 - 10.1007/978-3-642-22306-8_4

    PY - 2011/7/14

    Y1 - 2011/7/14

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

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

    KW - METIS-277629

    KW - Multi-Core

    KW - Model Checking

    KW - IR-77024

    KW - CR-D.2.4

    KW - EWI-20146

    KW - tree-based algorithm

    KW - incremental algorithm

    KW - Parallel

    KW - state space compression

    U2 - 10.1007/978-3-642-22306-8_4

    DO - 10.1007/978-3-642-22306-8_4

    M3 - Conference contribution

    SN - 978-3-642-22305-1

    T3 - Lecture Notes in Computer Science

    SP - 38

    EP - 56

    BT - Proceedings of the 18th International SPIN Workshop, SPIN 2011

    A2 - Groce, Alex

    A2 - Musuvathi, Madanlal

    PB - Springer

    CY - berlin

    ER -

    Laarman A, van de Pol JC, Weber M. Parallel Recursive State Compression for Free. In Groce A, Musuvathi M, editors, Proceedings of the 18th International SPIN Workshop, SPIN 2011. berlin: Springer. 2011. p. 38-56. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-22306-8_4