The Future of Testing Tools (Continued)

FTPOnline: What is SPIN?

Gerard Holzmann: SPIN is a software verification tool that can help the user to find and diagnose subtle, concurrency-related bugs in multi-threaded and distributed software systems. The tool is the result of a long-term research project that pretty much started in 1980, when I joined the Unix research group at Bell Labs.

The tool can be used to trap race-conditions, deadlock errors, and errors caused by data corruption that can result when different threads of execution step on each other's data without proper synchronization. It can also be used to prove more sophisticated temporal properties of systems of asynchronous processes.

Curiously, the class of concurrency-related software defects is largely ignored by the classical approaches to software testing, yet it is the one that worries software developers the most. Probably the majority of code that is being written today is designed to execute in a multi-threaded context. Our software development tools have not kept pace with this change: there are virtually no mainstream tools available today that can help a developer to design truly reliable multi-threaded systems software.

Ask any developer and they will admit that trying to fix a concurrency-related bug shortly before a product deadline is one of their worst nightmares. What makes these types of bugs so hard to diagnose is that they are rarely reproducible: a concurrent system behaves like a non-deterministic system, where the precise executions can depend on subtle timings of uncorrelated events. The result is that a damaging bug will manifest itself only intermittently. After a fix has been made for the suspected cause of a race, a developer will almost always have a lingering doubt that the bug will still be there, to strike again and do more damage.

When we first ran into these problems at Bell Labs, we decided that there had to be a better way to deal with these types of software development problems. The result was the SPIN tool. Last year the tool was recognized by the ACM with its prestigious Software Systems award, the same award that this year recognized Java, and earlier had been awarded to systems such as Unix, Tex, TCP/IP, and the World Wide Web.