On Thu, 22 Apr 1999, Oyvind Teig wrote: > Jeremy Martin and S.A.Jassim did a state-implosion(?) in their > "A Tool for Proving Deadlock Freedom" at WoTUG-20. Jeremy mentioned > at the presentation that it might be done on occam, or a subset > of it. What's the state? Dear Oyvind, Thanks for plugging the "Deadlock Checker" program. Further info is at http://users.ox.ac.uk/~jeremy/Deadlock/index.html A few points... * This program is only for proving deadlock freedom and livelock freedom, not for general behavioural specifications. However most people are only bothered about deadlock and livelock. * The method employed is very efficient and can be potentially applied to networks containing millions of processes. * The price of this efficiency is incompleteness. There are certain classes of deadlock-free network which are not susceptible to this proof technique. (For networks with sufficiently small state spaces it is usually better to use something like FDR.) * However this technique always does succeed for networks built according to a certain wide range of design rules (such as those discovered by Dijkstra, Roscoe, Brookes, Welch, and Brinch-Hansen). * The input format for the Deadlock Checker is a collection of finite state machines -- one for each process in the network. At present these are generated from CSP code using FDR, but it would be possible to rig up an occam compiler to generate them. (I haven't done this but Barry Cook told me that it would be fairly easy to do with the occam compiler that he has developed.) * This leads us to the point that Bryan made about state-space explosion. A single input of an INT32 variable in an Occam process would give rise to at least 2^32 states in the equivalent state transition system, so we need to apply some sort abstraction to reduce the number of states in each constitutent process. * This abstraction is difficult to automate - how do we decide how much information may be safely thrown away? Some very important work in this area has been done by Ranko Lazic (see Bill Roscoe's book: The Theory and Practice of Concurrency - Prentice Hall). * Much work has also been done regarding state-space compression. I wonder if there might not be some kind of higher-level state machine, that could be used, where the input of an INT32 variable would only require one new state to be added? Best wishes, Jeremy ------------------------------------------------------------------------- Dr J. M. R. Martin Oxford Supercomputing Centre Tel: (01865) 273849 Wolfson Building Fax: (01865) 273839 Parks Road Email: jeremy.martin@comlab.ox.ac.uk Oxford OX1 3QD WWW: http://users.ox.ac.uk/~jeremy