Cloud-Based Verification of Concurrent Software

Abstract

Logic model checkers are unparalleled in their ability to reveal subtle bugs in multi-threaded software systems. The underlying verification procedure is based on a systematic search of potentially faulty system behaviors, which can be computationally expensive for larger problem sizes. In this paper we consider if it is possible to significantly reduce the runtime requirements of a verification with cloud computing techniques. We explore the use of large numbers of CPU-cores, that each perform small, fast, independent, and randomly different searches to achieve the same problem coverage as a much slower stand-alone run on a single CPU. We present empirical results to demonstrate what is achievable.

G.J. Holzmann—This research was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.

A Appendix: Bitstate Hash Storage

The bitstate hash storage method [6] can most easily be understood as an application of the theory of Bloom filters [1]. The storage method is used in explicit state on-the-fly model checkers, such as Spin [8], for fast approximate searches in statespaces that are too large to be explored exhaustively. The method uses one or more hash functions with uniform random distribution to compute 64-bit signatures of each newly generated reachable state.

A hash-arena of, say, 32 GB ($2^{35}{}$ bytes) contains $2^{38}{}$  addressable bits. If using a single hash-function, we can use the 64 available bits from the hash signature to produce a 35-bit address into the hash-arena. If the bit at this address is at its initial value of zero, then we know that the newly generated state was not visited before in the search. We now record the fact that the state has been explored by setting that bit position to a one, so that the next time this state shows up in the search we know that we do not have to explore it again.

If the size of a single state descriptor for this example is $2^{10}{}$ bytes, we would not be able to store more than $2^{35}/2^{10}=2^{25}{}$  unique states in 32 GB (about 33.5 million). The bitstate storage method on the other hand, can in principle store up to $2^{38}{}$  or 275 billion unique states, for an increase of almost four orders of magnitude.

In sufficiently many bits are used to index the hash-arena, the probability of hash collisions can be very small. A hash collision would happen if two states that are not equal produce the same 35-bit hash signature. The search truncates in this case, which means that it is no longer guaranteed to be exhaustive. We can reduce the probability of hash collisions effectively by using multiple hash-functions for each state, which then corresponds to checking and setting multiple bit-positions. If $h$ hash-functions are used, for instance, a hash-collision must now occur on all $h$ bit-positions for the state to be affected. The Spin model checker uses three hash-functions per state by default, but the number is user-selectable.

For large state spaces, or large state descriptors, where exhaustive storage of a complete statespace with a traditional method is infeasible, the bitstate storage method is an attractive alternative to increase problem coverage, by a significant margin. Another advantage of the use of a bistate storage method for large problem sizes is that for a given size of the hash-arena, the maximal runtime of the algorithm is fixed and known, independent of the actual statespace size.