[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: New Book: CONCURRENCY
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?
Thanks for plugging the "Deadlock Checker" program. Further info is at
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?
Dr J. M. R. Martin
Oxford Supercomputing Centre Tel: (01865) 273849
Wolfson Building Fax: (01865) 273839
Parks Road Email: jeremy.martin@xxxxxxxxxxxxxxx
Oxford OX1 3QD WWW: http://users.ox.ac.uk/~jeremy