Re: Self-deadlock

[Frederick Barnes <frmb2@xxxxxxxxx>]

Hi,

> 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?

The toolset compiler appears to generate a CCNT1 instruction,
presumably to check that at least one of the pre-conditions is
TRUE.

KRoC for linux produces the following (with debugging on):
    KRoC: Range error on operation CCNT1 in PROC "selfdead"
          in file "selfdead.occ" near line 15

Line 15 is where "b & c2 ? v2" lives.  Although the error message
isn't too helpful, it at least detects it.  So, the error isn't
detected at compile-time, but is at run-time.  An optimiser (when
it gets written) would be able to detect it at compile-time.


Cheers,
  Fred.
-- 
Fred Barnes, PhD research student, UKC.  http://nuked.xylene.com/
frmb2@xxxxxxxxx         http://www.cs.ukc.ac.uk/people/rpg/frmb2/