Spade: Verification of Multithreaded Dynamic and Recursive Programs (Tool Paper)

摘要

Spade has been applied to several examples. The performances are given in Table 1. The experiments were obtained on a 4GHz Pentium IV with 4GB of memory. The BlueTooth v1 is the Spad model of the BlueTooth driver program used by Windows NT and given in [QW04]. We were able to find a bug in this program. To find this error, the [QW04] authors needed to guess the number of driver's requests for which the error occurs, and then run their tool; whereas with Spade, the verification was done in a completely automatic manner, since we did not have to guess the number of requests for which the error occurs because our tool can deal with dynamic creation of processes. The BlueTooth v2 is a corrected version of BlueTooth v1 proposed by the authors of [QW04]. Spade finds an error in this version as well. This bug was already found in [CCK+06]. Again, to be able to find the bug, the authors of [CCK+06] needed to guess the number of requests that causes the bug before running their tool, whereas Spade did not need to perform this guess. ConcVector is a Spad model of a multithreaded program using concurrently methods of the class java.util.Vector from the Java Standard Collection Framework. The program's threads create and remove the elements of a Vector object. Wand and Stoller [WS03] reported a high-level data race that occurs on such programs because the constructor of the Vector class is not atomic. Spade found this bug for a program with an unbounded number of threads (ConcVector v1). Version v2 fixes the bug by taking an atomic implementation of the constructor. Spade was able to prove that this version is correct. The Lock/unlock example is a system that handles an arbitrary number of concurrent insertions on a binary search tree. The algorithm was proposed in [KL80], and can be applied to handle simultaneous insertions (done by several users) into a database, or to reduce the time necessary for a single insertion. We considered a buggy version of the algorithm where one or several processes do not adhere to the required lock and unlock policy. This version was considered in [CCK+06], where the bug was found only for systems where the number of concurrent processes is less or equal to 7. With Spade, we were able to check this buggy program for arbitrary number of concurrent insertion processes.