Re: New Book: CONCURRENCY

[Jeremy Martin <jeremy.martin@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

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@xxxxxxxxxxxxxxx
 Oxford OX1 3QD                         WWW: http://users.ox.ac.uk/~jeremy