fix edge case

diff --git a/model.cc b/model.cc
index 53bb7b0d04b5f0ba6a34d1a9ed24218acdfbdbe3..2f744eee754e43126b071638f8f81568b834ed53 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -351,9 +351,9 @@ void ModelChecker::continueExecution(Thread *old)
                checkfree += params.checkthreshold;
                execution->collectActions();
        }
                checkfree += params.checkthreshold;
                execution->collectActions();
        }

+       thread_chosen = false;

        curr_thread_num = 1;
        curr_thread_num = 1;

-       thread_id_t tid = int_to_id(1);
-       Thread *thr = get_thread(tid);
+       Thread *thr = getNextThread();

        scheduler->set_current_thread(thr);
        if (Thread::swap(old, thr) < 0) {
                perror("swap threads");
        scheduler->set_current_thread(thr);
        if (Thread::swap(old, thr) < 0) {
                perror("swap threads");


@@ -361,6 +361,20 @@ void ModelChecker::continueExecution(Thread *old)
        }
 }
 
        }
 }
 

+Thread* ModelChecker::getNextThread()
+{
+       Thread *thr = NULL;
+       for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
+               thread_id_t tid = int_to_id(i);
+               thr = get_thread(tid);
+               if (!thr->is_complete() && !thr->get_pending()) {
+                       curr_thread_num = i;
+                       break;
+               }
+       }
+       return thr;
+}
+

 void ModelChecker::finishExecution(Thread *old) 
 {
        scheduler->set_current_thread(NULL);
 void ModelChecker::finishExecution(Thread *old) 
 {
        scheduler->set_current_thread(NULL);


@@ -399,18 +413,11 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 
        old->set_pending(act);
 
 
        old->set_pending(act);
 

-       Thread *next = NULL;

        curr_thread_num++;
        curr_thread_num++;

-       while (curr_thread_num < get_num_threads()) {
-               thread_id_t tid = int_to_id(curr_thread_num);
-               next = get_thread(tid);
-               if (!next->is_complete() && !next->get_pending())
-                       break;
-               curr_thread_num++;
-       }
+       Thread* next = getNextThread();

 
        if (old->is_waiting_on(old))
 
        if (old->is_waiting_on(old))

-               assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+               assert_bug("Deadlock detected (thread %u)", curr_thread_num-1);

 
        ModelAction *act2 = old->get_pending();
                
 
        ModelAction *act2 = old->get_pending();
                

diff --git a/model.h b/model.h
index dc36eb6339f8dc3d3d13d6908500858bf4d45d27..cabd9904eb2d5bf64dc667c6ab78c33a2e4897f2 100644 (file)
--- a/model.h
+++ b/model.h
@@ -58,6 +58,7 @@ public:
        void continueExecution(Thread *old);
        void finishExecution(Thread *old);
        void consumeAction();
        void continueExecution(Thread *old);
        void finishExecution(Thread *old);
        void consumeAction();

+       Thread * getNextThread();

 
        void assert_bug(const char *msg, ...);
 
 
        void assert_bug(const char *msg, ...);