Re: Self-deadlock

[Denis A Nicole <dan@xxxxxxxxxxxxxxx>]

On Tue, 4 Apr 2000, Oyvind Teig wrote:

> BOOL a, b:
> SEQ
>   a := FALSE
>   b := FALSE
>   WHILE TRUE
>     ALT
>       INT v1:
>       a & c1 ? v1
>         SKIP
>       INT v2:
>       b & c2 ? v2
>         SKIP
> 
> Does KRoC detect this error at compile-time?
> 
> SPoC sees it at run-time. It writes "Deadlock, #no stopped processes"
> to stderr on return from Scheduler, in main.
> 
> Isn't it "required" to handle this by the compiler or at run-time
> already when the ALT is set up?

I think an ALT with no body is supposed to act like STOP, which it does.

I also think that the occam semantics require deadloc to be decctable---it
is distinguished from divergence.  That is, an implementation should treat

	STOP	and		WHILE TRUE
				  SKIP

differently.  SPoC does, by reporting deadlock.

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