The Universal Tiny Problem Solver (short: UTPS) is a case study to check in how far the complete state space of a multi-threaded C program can be exhaustively searched for possibly reachable deadlocks or related erroneous program configurations.
Accordingly, the key design goals for this tool are:
The obvious problem in such an approach is the number of possibly reachable configurations very easily becomes infeasibly large. The basic technology here by which we have tried to overcome this obstacle is to represent global configurations of the multi-threaded system by vectors of 32-bit int's and sets of such vectors by bdd's (Binary Decision Diagrams) and implement the individual operations of the program directly on bdd's. The hope is that even large sets of configurations may have succinct representations through bdd's.
As our result, the feasibility of the approach could be approved. Our tool meets the four design goals above and still turns out to amazingly efficient. In particular, we succeeded to check deadlock freeness of an Airbus Hoare monitor protocol in half a minute and found a possibly reachable deadlock in a corresponding flawed protocol in approx. 10 seconds. Also, we succeeded to check bounded buffer protocols with semaphores and dining philosopher problems.
The use of bdd's, though, incurs inherent limitations: both multiplication and indirect addressing for bdd's is extremely expensive. Accordingly, only multiplication with constants and dereferencing of statically known addresses is supported by our tool. These restrictions are severe if general C programs are to be analyzed. In the envisioned application area, though, the parallel flow of control is affected only by few (mainly global) int variables which are modified by addition or subtraction and tested iteratively by waiting threads. Such protocols are straight forwardly handled by our tool.
In order to syntactically ensure the restrictions of our tool, we refrained from employing (a subset of) C as our specification language. Instead, we use a (quite powerful) assembly-like notation which, however, supports some C features directly such as arrays, structs or Posix thread library functions. As a potential future environment, we envision our tool to be accompanied with a program slicer which, from large C programs, extracts the small multi-threaded core algorithms which govern thread interaction, together with an automatic translator of these programs into the input specification language of our tool.
A tarred and gzipped executable running under Linux is available for DOWNLOAD.
Helmut Seidl - DAEDALUS - Aug-13-2002