Re: Self-deadlock

["P.H.Welch" <P.H.Welch@xxxxxxxxx>]

Oyvind,

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!

So, the following programs both compile under KRoC and generate almost
exactly the same code:

  PROC silly.alt (CHAN OF BYTE keyboard, screen, error)
    ALT
  :

  PROC silly.stop (CHAN OF BYTE keyboard, screen, error)
    STOP
  :

Compiled in the default (halt) checking mode, both produce the transputer
"seterr" instruction.  That's all there is for the silly.stop PROC.  The
silly.alt PROC surrounds the "seterr" with an "adj" (adjust workspace) up
and down by one.  When run, both raise the same run-time error.

So, two questions:

  1. if the compiler can detect deadlock, should it reject the program?

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

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.