Paper Details

Parallel Algorithms for Deadlock and Livelock Analysis of Concurrent Systems

Authors: Martin, Jeremy M. R., Huddart, Yvonne

Abstract:

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.

Proceedings:

Communicating Process Architectures 2000, Peter H. Welch, André W. P. Bakkers, 2000, pp 1 - 14 published by IOS Press, Amsterdam

Files: PDF, PS

This record in other formats:

Web page: BibTEX, Refer
Plain text: BibTEX, Refer

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.