stackoverflow exception

Jan 14, 2014 at 9:41 PM
Edited Jan 15, 2014 at 12:43 AM
Hi,

I have two problems related to a stack overflow exception:
  1. Visual Studio 2012 Crash
    I don't know if this is a bug, but if I get a stack overflow exception in the dafny VS extension and Visual Studio 2012 crashes. This is followed by this message box stating 'Microsoft Visual Studio 2012 has stopped working. Windows is checking for a solution to the problem.' VS usually restarts afterward. Sometimes, I lose a line of code or two, so it isn't a big deal. However, it's annoying. When I encounter this, my work around is using dafny from the command prompt. When I run dafny in the command prompt, it gives a 'Process is terminated due to StackOverflowException' error (which is comparable to the VS extension crash).
  2. Verification problem (my main problem)
    I get a stack overflow exception from calling a method several times. I'm confused to if this is a verification error, dafny application error, or a little of both. I'm guessing it doesn't like 'reads *' in some of the predicates? This is most of the code that causes the stack overflow exception I'm not sure if I should overwhelm this post with a bunch of code, so this is most of it (below).
<2. continued through rest of post>
Here's a little blurb on this code snippet: it's a scheduler I'm trying to verify. There's underlying data structures that aren't listed here which includes FIFO queues, priority queues, and an unordered list. The FIFO queue is implemented as a bounded, array-based circular queue; the priority queue and unordered list is bounded and array-based. There's also a task class that's not listed.

What I don't understand: I can call stub1( ) four times with Dafny verifying it (quite cheerfully), but if I uncomment the fifth stub1( ) method call, I get the stack overflow exception. I've only guessed on how to conquer this stack overflow exception. I've tried commenting out many pre and post conditions, but the only solid lead I have is the issue is related to the Valid predicate. I've had no success.
method test_stub1()
{
    var s := new Scheduler(4, 10, false);
    s.stub1();
    s.stub1();
    s.stub1();
    s.stub1();
    //s.stub1();    // uncomment this for stackoverflow exception
}

class {:autocontracts} Scheduler {
    var readyList : ListData;   // array of fifo queues
    var waitingList : ListData;         // priority queue
    var suspendList : ListData;         // unordered list
    var delayList : ListData;           // priority queue

    //var allTasks : array<TaskCrossN>;

    var clock : int;
    var topReadyPriority : int;
    var listSize : int;
    var taskData : TaskData;    // contains idle task, running task
    var parameter : Parameter;  // contains maxprior, maxdelay, preemption

    ghost var g_waitingList : ListData;
    ghost var g_readyList : ListData;
    ghost var g_suspendList : ListData;
    ghost var g_delayList : ListData;
    ghost var g_clock : int;
    ghost var g_parameter : Parameter;
    //ghost var taskData.g_allTasks : seq<TaskCrossN>;

    ghost var Repr : set<object>;

    predicate Valid
        reads *;
        //reads this, Repr;
        //reads readyList;
    {
        ValidRepr &&
        ValidTaskData &&
        ValidLists &&
        0 <= listSize < g_suspendList.getUnorderedList().u.Length &&
        ValidClock &&
        ValidParameter && 
        g_parameter.maxPriorities > topReadyPriority >= 0 && |taskData.g_allTasks| > 0
        //10 >= g_parameter.maxPriorities > topReadyPriority >= 0 && |taskData.g_allTasks| > 0
        //taskData.runningTask.key == topReadyPriority

    }

    predicate ValidRepr() 
        reads this;
    {
        this in Repr &&
        //taskData.runningTask in Repr &&
        g_readyList in Repr &&
        g_waitingList in Repr &&
        g_suspendList in Repr &&
        g_delayList in Repr 
    }

    predicate ValidTaskData()
        //reads this, taskData, taskData.runningTask;
        reads *;
    {
        taskData != null &&
        taskData.runningTask != null &&
        taskData.Valid &&  
        taskData.runningTask.Valid 
    }

    predicate ValidLists()
        reads *;
    {
        g_readyList != null && g_readyList.Valid &&
        g_delayList != null && g_delayList.Valid &&
        g_waitingList != null &&  g_waitingList.Valid &&
        g_suspendList != null && g_suspendList.Valid  &&
        g_readyList == readyList && g_waitingList == waitingList && g_suspendList == suspendList && g_delayList == delayList 
    }

    predicate ValidClock
        reads this;
    {
        g_clock == clock &&
        g_clock >= 0 
    }

    predicate ValidParameter
        reads *;
    {
        g_parameter != null && g_parameter.Valid && parameter != null && 
        g_parameter == parameter && g_parameter.maxPriorities == parameter.maxPriorities && g_parameter.maxDelay == parameter.maxDelay && g_parameter.preemption == parameter.preemption &&
        g_parameter.maxDelay > 0 
    }

    constructor (maxPrior : int, delay : int, preemption : bool)
        modifies this; 
        requires maxPrior > 0 && delay > 0;
        requires preemption == true || preemption == false;
        ensures g_parameter.maxPriorities == maxPrior;
        ensures g_parameter.maxDelay == delay;
        ensures g_parameter.preemption == preemption;
        ensures topReadyPriority == 0;
        ensures g_clock == 0;
        ensures taskData.runningTask != null;

  method stub1()
    // blank method
}
...
I've tried commenting out and guessing the pre or post conditions that might cause a stack overflow exception. There isn't any documentation on how to handle a stack overflow exception, so, I've been guessing on how to fix this code and get it to verify. I can't run this through the BVD in VS because the application crashes and restarts when this exception occurs. Any advice, tricks, or help would be greatly appreciated.

Best,

Matt
Jan 16, 2014 at 9:10 PM
I'm not sure if anyone read this, but I (sort of) fixed point 2. Some of the code was rewritten and I removed all of the 'reads '. I think the 'reads ' had something to do with it. It's a good enough solution :) .

Matt
Developer
Jan 17, 2014 at 9:49 AM
Hi Matt,

thank you for reporting this issue. From what you are describing it seems that this stack overflow is easily reproducible even if you use the command line version of Dafny. If so, it would be great if you could send us an (ideally short) file that triggers the issue. Then we can look into it.

Best regards,

Valentin
Jan 17, 2014 at 7:50 PM
Hi Valentin,

Sure thing. I submitted it into the issue thread here. The code that causes the stack overflow exception and some command line output was submitted and posted.

Best,
Matt