Developed by Jeremy Martin, Oxford University, based on my D. Phil project which was supervised by Ian East and Sabah Jassim at Buckingham University.
Deadlock Checker is a tool which performs various innovative checks on parallel programs written in CSP in order to prove freedom from deadlock and livelock. It acts as a design workbench for designers of safety-critical distributed systems. Its main advantage over competing tools is scalability. Deadlock Checker may be used to verify networks built from many thousands of processes.
The program is written entirely in Java. The user interface console looks like this.
Use the Load Network button to read in a network description file (which must have previously been compiled from CSP code using a companion program to Deadlock Checker). A browser is diplayed. In this example we shall load the famous Dining Philosophers network.
We analyse this network for deadlock-freedom using the innovative SDD (State Dependence Digraph) technique. Here the algorithm detects a possible deadlock situation.
The program provides an online help facility to explain the various analysis techniques that are offered.
A useful feature of Deadlock Checker is its ability to execute a network of CSP processes. Here the Dining Philosophers are executed and deadlock is detected. This feature is intended for debugging networks -- it cannot be used to show that a network is deadlock-free.
Another important debugging facility is the Network viewer. This enables the user to explore the individual process states within the compiled network...
... and also to view the process intercommunication structure.
You can get some beautiful network visualisations this way. Here is a process farm network.
... here is the message switching system of Roscoe and Dathi
... here is a 3 x 3 toroidal game of life board with a control process
... here is a network which implements the Mad Postman Routing protocol of Yantchev and Jesshope
... finally, here is a 5 x 5 toroidal cellular array.
If your machine doesn't have Java on it you can download it from here.
The Deadlock Checker program is available as a zipped Java package Deadlock.zip. Once you have downloaded this file you need to put it into your class path, e.g.
SET CLASSPATH=".;C:/Java/bin:C:/Java/Deadlock.zip"
Then you run Deadlock Checker by typing
java Deadlock.Checker
If you want full debugging information on standard output type
java Deadlock.Checker debug
But you will also need some network files to work with. The following were created using FDR version 1.4:
Start up FDR then load in this file: compile.ml
Then you type a command like
compile "phils.csp" "phils.net" ;
to compile your network.
For compilation with FDR version 2.23 you need to use the file compile.tcl which is documented here. Note that the CSP input format is changed in version 2, as is the method of defining a CSP network for Deadlock Checker.
The new interface has been used with the examples from chapter 13 of Bill Roscoe's book. . The matrix multiplication network can be proven deadlock-free using the CSDD algorithm, the message passing ring using the FSDD algorithm, the binary switching network using the SDD3 algorithm. The virtual channel router is amenable to the plain SDD technique.
The railway track system, however, cannot be proven deadlock-free using the techniques supported by Deadlock Checker.
For full details you can read my thesis, or a paper and tutorial from the WoTUG-20 Conference.
For historical reference, here is the ml code and documentation for the prototype version of Deadlock Checker, now superseded by the above.