No Exit Hang Detection

Some hangs can be detected via static analysis on the interpreted program. This analysis should run whenever a new program block is finalized during the search.

Basic detection

The basic detection determines all program blocks that can be reached from the program block that has just been finalized. If all are already finalized and not known to exit then the program is known to hang.

Figure 1 shows an example of a hang that can be detected this way. Its interpreted program is shown below. It is known to hang as from Program Block #4 to #12 no exit can be reached.

 0: INC 1 => -/1
 1: SHR 1 => 2/3
 2: INC 2 => -/4
 3: EXIT
 4: DEC 1 => 5/6
 5: SHL 2 => 9/10
 6: SHL 1 => 7/8
 7: SHR 2 => 5/6
 8: INC 2 => 9/10
 9: DEC 1 => -/8
10: SHR 1 => 11/12
11: SHL 2 => 9/10
12: DEC 1 => 5/6

Figure 1. Hang detected by basic No Exit algorithm

Reachability analysis

A more advanced variant checks if the entry conditions of the possible exits can actually be met. This is best illustrated via an example.

Figure 2 shows a program with relatively complex behaviour that is known to hang this way. Its interpreted program is shown below.

 0: INC 1 =>  -/1
 1: SHR 1 =>  2/3
 2: INC 1 =>  -/4
 3: EXIT
 4: SHR 2 =>  5/6
 5: INC 1 =>  -/7
 6: DEC 1 => 11/9
 7: SHL 1 =>  8/7
 8: DEC 2 =>  -/9
 9: INC 1 => 10/4
10: EXIT
11: INC 2 =>  -/7

Here the basic analysis does not suffice as Program Block #10 can (indirectly) be reached from all other blocks. However, examining the program block graph more closely shows that Block #10 can only be reached via two paths:

  1. #7 =(0)=> #8 (DEC 2) =(!0)=> #9 (INC 1) =(0)=> #10
  2. #4 =(!0)=> #6 (DEC 1) =(!0)=> #9 (INC 1) =(0)=> #10

In the first path, Block #8 can only be entered with a value of 0. This value is then decreased by two and subsequently increased by one, so it is never zero, so the entry condition for Block #10 cannot be met this way.

In the second path, Block #6 can only be entered with a non-zero value. This value is then decreased by one, and subsequently increased by one again. So also here it follows that it will be non-zero, which means Block #10 cannot be entered via this path either.

Figure 2. Hang detected by No Exit detection with reachability analysis