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

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