db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%T Parallel Algorithms for Deadlock and Livelock Analysis of Concurrent Systems
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%A Jeremy M. R. Martin, Yvonne Huddart
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%E Peter H. Welch, Andr\[`e] W. P. Bakkers
%B Communicating Process Architectures 2000
%X Conventional model\-checking techniques for analysing
concurrent systems for deadlock or livelock are hampered by
the problem of exponential state explosion: the overall
number of global states that needs to be checked may grow
exponentially with the number of component processes in the
system. The state\-of\-the\-art commercial tool FDR provides
deadlock and livelock analysis but it is limited at present
to analysing systems of up to one hundred million global
states. The Deadlock Checker tool is capable of analysing
very much larger systems by taking certain short\-cuts. But
this is achieved at the cost of incompleteness \-\- there
are certain deadlock\-free and livelock\-free networks that
may not be proven so using that tool. Here we investigate a
different approach. We present parallelised model\-checking
algorithms for deadlock and livelock analysis and describe
their implementation. The techniques are found to scale well
running either on a conventional supercomputer or on a PC
cluster.