[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
> 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 ...
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