Parallel Recursive State Compression for Free

Laarman, Alfons and Pol van de, Jaco and Weber, Michael (2011) Parallel Recursive State Compression for Free. In: 18th International SPIN Workshop on Model Checking of Software, SPIN 2011, 14-15 July 2011, Snow Bird, Utah.

PDF
Restricted to UT campus only: Request a copy
1263Kb

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.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/77024
Conference URL:	http://research.microsoft.com/en-us/um/redmond/events/spin2011/
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page