Check out the new USENIX Web site. next up previous
Next: Time Taken for a Up: Handling Large States Previous: Handling Large States

Managing Memory Resources

During the state space search, CMC maintains two data structures: a hash table of states seen during the search, and a queue of states seen but whose successors are yet to be generated. It is not necessary to store the entire state in a hash table [36]. CMC uses a hash compaction algorithm [36] to store only a small signature (typically, 8 bytes) for each state in the hash table. By doing so, the memory requirements of the hash table depend only on the number of states explored during model checking.

The queue, however, has to maintain the states in their entirety, as all of the information in the state is necessary to generate the successor states. However, the queue has good locality of reference, so much of it can be swapped to disk during model checking. Moreover, the states in the queue can be efficiently compressed; as states can simply be regenerated by remembering the sequence of events that generated them from the initial system state.


Table 2: Time taken for a single CMC transition, averaged over the first million transitions. The experiment involves CMC checking the TCP model in a server running a $800$MHz Intel Pentium III processor with $256$KB cache and $2$GB of memory.
  Time in microseconds
  State Transition Hash State Total
  Restore Execution Computation Store  
Processing Entire States 656 305 17816 608 19385
With Incremental States 298 363 2927 64 3652
With Incremental Heap Canonicalization 305 365 1453 65 2188


In practice, the large amount of memory available in modern machines makes managing memory much easier. For instance, a gigabyte hash table is more than sufficient to explore $100$ million states when using a $8$ byte compacted signature for each state. The remaining memory can be allocated for the queue. As will be shown below, CMC is limited more by the time required for the state space exploration than by the memory available.


next up previous
Next: Time Taken for a Up: Handling Large States Previous: Handling Large States
Madanlal Musuvathi 2004-03-03