Dissertation/Thesis Abstract

Adaptive Approximate State Storage
by Dillinger, Peter C., Ph.D., Northeastern University, 2010, 289; 3434729
Abstract (Summary)

Efficiently storing and matching visited states is key to the effectiveness of explicit-state model checkers such as SPIN. Models of concurrent programs often have too many reachable states to enumerate easily in main memory, and an efficient model checker can exhaust main memory in minutes by storing state descriptors exactly. A popular alternative is to over-approximate the set of visited states using a randomized, probabilistic data structure, such as a Bloom filter. Because the approximation is sound and does not slow down the search with revisitation of states, it tends to find errors quickly. Because it is probabilistically complete, the approach can also convincingly demonstrate lack of errors.

In this dissertation, I analyze the approximate state storage problem in unprecedented detail, improve upon standard solutions, and demonstrate a novel approach that solves a configuration dilemma facing users of the standard solutions. Especially with my improvements, the best Bloom filter or hash compaction configuration for a given situation is quite good, but choosing the best configuration depends on a good estimate of the number of reachable states. Such an estimate is usually only available after checking a model. I solve this dilemma with an efficient storage scheme that is not tied to a particular estimate, because it is adaptive. Regardless of the number of states encountered at run time, its accuracy is near the information-theoretic optimal. It is also competitively fast, thanks to a novel in-place adaptation algorithm and a favorable access pattern to memory.

Indexing (document details)
Advisor: Manolios, Panagiotis
Commitee: Aslam, Javed A., Cooperman, Gene, Visser, Willem
School: Northeastern University
Department: Computer Science
School Location: United States -- Massachusetts
Source: DAI-B 72/03, Dissertation Abstracts International
Subjects: Computer science
Keywords: Bloom filter, Hash table, Hashing, Model checking, Standard solutions, Storage problem
Publication Number: 3434729
ISBN: 978-1-124-41980-0
Copyright © 2020 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy