[Javapathfinder-devel] Re: infinite POR loop

[Peter C. M. <pcm...@em...>]

[..we should move all these discussions to the mailing list..]

That was my original thinking too, but no. The forward succeeds (it 
executed something), the state is new (changed the stack), so DFSearch 
happily goes one step down and restarts to search with thread 0. It's 
almost like we want to switch to BFS for one depth. So there's three 
solutions I could see:

(1) request a backtrack after breaking the por loop, to force the 
scheduler to advance past the suspicious thread at the same search 
level

(2) just 'blank out' the suspicious thread from the next forward 
scheduling sequence (i.e. skip it for the next search depth)

(3) re-order threads

While (1) seems to be less disruptive, there is of course a pretty 
hefty 'optimization' issue. If the thread doesn't recover (which is 
very likely), it will henceforth always cause one additional backtrack 
per search depth. I think it basically kills DFSearch at this point. 
Wonder what effects re-ordering would have on 
state-storage/backtracking, though. Don't know about (2) yet, either

the case is pretty easy to get:

public class Starve implements Runnable {
      public void run () {
           throw new RuntimeException("blow it up");
      }

      public static void main (String[] args) {
           Starve o = new Starve();
           Thread t = new Thread(o);
           t.start();

           int sum=0;
           while (true) { // starve t
                sum++;
           }
      }
}

-- Peter

On May 5, 2005, at 9:18 PM, Willem Visser wrote:

> Changing the thread order does seem extreme, but I'll think if there 
> is a
> reason not to do that.
>
> Of course you could also just break the loop and forget about it, if 
> there
> is something interesting in the rest of the system it will come out -
> pushing the "dead-thread" to the end would be an optimization.
>
> The thing here is that this issue should seldom come up, in fact if it 
> comes
> up in a "real" program then frankly it is a bug - you obviously didn't 
> want
> a non-progressing, non-interacting cycle in your code. The only 
> scenario
> this could legitimately happen is when you abstract a program - but we 
> don't
> do these kind of abstractions (we do the abstract state storing 
> variety).
>
> Others that have dealt with this kind of issue either punt by stating 
> these
> idle-loops are not allowed, or they use some clever loop breaking via
> back-edges etc.
>
> ----- Original Message -----
> From: "Peter C. Mehlitz" <pcm...@em...>
> To: "Willem Visser" <wv...@em...>; "John Penix"
> <Joh...@na...>
> Sent: Thursday, May 05, 2005 8:10 PM
> Subject: infinite POR loop
>
>
>> that's of course a bit more interesting - what we need in addition to 
>> a
>> trivial loop breaker is some sort of a Thread.yield, i.e. if we have a
>> suspicious thread that seems to bore us to death with idling, we have
>> to make sure we change the scheduling order, so that this sucker
>> henceforth always gets explored last. Should be simple enough by
>> pushing it to the end of the ThreadList when resetting the scheduler
>> (which is effectively an index re-order in SystemState.prepareNext()),
>> but I'm a bit uncertain what re-ordering does to us. I think, so far
>> thread indexes were invariant.
>>
>> Any insights, thoughts, suggestions?
>>
>> -- Peter
>>
>