Re: Self-deadlock

[Denis A Nicole <dan@xxxxxxxxxxxxxxx>]

On Wed, 5 Apr 2000, P.H.Welch wrote:

> An ALT with no guarded processes - or an ALT with pre-conditioned guarded
> processes all of whose pre-conditions are FALSE - is a perfectly legal
> program in occam.  Similarly, occam does not attempt to outlaw deadlock.
> A deadlocking occam system is still a legal occam system.  So, even if the
> compiler could detect a definite path to deadlock, it ought still to compile
> the program (?) ... although issuing some concerned warnings might be nice!

Yes, just like SPoC.  The deadlock _is_ detected at run time.  This
correctly distinguishes it from divergence.

> So, two questions:
> 
>   1. if the compiler can detect deadlock, should it reject the program?

It should warn. 

>   2. should we be looking to develop languages whose syntax/semantics do
>      not allow the writing of programs that deadlock?

We should be developing tools that allow us to detect deadlock and other
undesirable behaviours by static analysis and model checking.  I am.

Deadlock is not a big issue for parallel correctness; there  are much
worse and more insidious failure modes.  As deadlock is detected at run
time, appropriate failure mitigation can take place.  Eg, deadlock on an
in-flight 747 can trigger a self destruct so as to prevent ground
casualties.

> In a sense, (2) was what the graphical occam Design Tool (oDT) was trying
> to do.  That was a graphical language for designing process networks which
> understood certain design patterns (client-server, I/O-PAR and hybrids of
> these) for which we had formal proofs that the resulting designs were free
> from deadlock, livelock and process starvation.  occam template codes were
> automatically generated from the designs.  The problem was that the design
> patterns it knew about were not complete - there were some designs that
> were safe, but which neither wanted nor required the known patterns.
> In those cases, oDT allowed the designer not to specify to what pattern
> he/she was designing and turned off the checks.
> 
> If we could devise a complete set of safe design patterns, then a very
> powerful language could be designed.  But that's probably not possible!??
> Maybe we should try though ... and allow the programmer to drop into
> free-wheeling low-level occam when the application didn't fit the patterns
> supported ...
> 
> Peter.
> 
> 

Denis A Nicole                 WWW:   http://www.hpcc.ecs.soton.ac.uk/~dan
High Performance Computing     Email: dan@xxxxxxxxxxxxxxx
Department of Electronics      Phone: +44 23 8059 2703
       & Computer Science      Fax:   +44 23 8059 3903
University of Southampton
SO17  1BJ
United Kingdom