add support for freeing threads

diff --git a/execution.cc b/execution.cc
index 53b6bccf790df471600a8f555f1ed17249a72443..c1a5308712160ab4b3e1f2e3891b98d6e24466ca 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1819,7 +1819,7 @@ ClockVector * ModelExecution::computeMinimalCV() {
        //Thread 0 isn't a real thread, so skip it..
        for(unsigned int i = 1;i < thread_map.size();i++) {
                Thread * t = thread_map[i];
-               if (t->get_state() == THREAD_COMPLETED)
+               if (t->is_complete())
                        continue;
                thread_id_t tid = int_to_id(i);
                ClockVector * cv = get_cv(tid);

diff --git a/model.cc b/model.cc
index c2de31304f577187d538075de45504a94f7019b9..596e528d84e75adcacdda1d3f6bd71345333100a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -332,7 +332,7 @@ void ModelChecker::startRunExecution(Thread *old) {
                thread_chosen = false;
                curr_thread_num = 1;
 
-               Thread *thr = getNextThread();
+               Thread *thr = getNextThread(old);
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);
 
@@ -371,17 +371,21 @@ void ModelChecker::startRunExecution(Thread *old) {
        }
 }
 
-Thread* ModelChecker::getNextThread()
+Thread* ModelChecker::getNextThread(Thread *old)
 {
        Thread *nextThread = nullptr;
        for (unsigned int i = curr_thread_num;i < get_num_threads();i++) {
                thread_id_t tid = int_to_id(i);
                Thread *thr = get_thread(tid);
 
-               if (!thr->is_complete() && !thr->get_pending()) {
-                       curr_thread_num = i;
-                       nextThread = thr;
-                       break;
+               if (!thr->is_complete()) {
+                       if (!thr->get_pending()) {
+                               curr_thread_num = i;
+                               nextThread = thr;
+                               break;
+                       }
+               } else if (thr != old && !thr->is_freed()) {
+                       thr->freeResources();
                }
 
                /* Don't schedule threads which should be disabled */
@@ -481,7 +485,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        chooseThread(act, old);
 
        curr_thread_num++;
-       Thread* next = getNextThread();
+       Thread* next = getNextThread(old);
        if (next != nullptr) {
                scheduler->set_current_thread(next);
                if (Thread::swap(old, next) < 0) {

diff --git a/model.h b/model.h
index 44ed858fe85faa363d934891faefeae8d321af6f..12aeebcce1df645950ce702d07c14f459da15de6 100644 (file)
--- a/model.h
+++ b/model.h
@@ -79,7 +79,7 @@ private:
        void finishRunExecution(Thread *old);
        void consumeAction();
        void chooseThread(ModelAction *act, Thread *thr);
-       Thread * getNextThread();
+       Thread * getNextThread(Thread *old);
        void handleChosenThread(Thread *old);
 
        modelclock_t checkfree;

diff --git a/threads-model.h b/threads-model.h
index 73c1d8f78f7c8a9f79a0ee0dc5de463be7a85a68..b1aa9013bf6e7ee174976fafc8e286dca7183f39 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -33,7 +33,8 @@ typedef enum thread_state {
         */
        THREAD_BLOCKED,
        /** Thread has completed its execution */
-       THREAD_COMPLETED
+       THREAD_COMPLETED,
+       THREAD_FREED
 } thread_state;
 
 
@@ -81,7 +82,10 @@ public:
        void * get_pthread_return() { return pthread_return; }
 
        /** @return True if this thread is finished executing */
-       bool is_complete() const { return state == THREAD_COMPLETED; }
+       bool is_complete() const { return state == THREAD_COMPLETED || state == THREAD_FREED; }
+
+       /** @return True if this thread has finished and its resources have been freed */
+       bool is_freed() const { return state == THREAD_FREED; }
 
        /** @return True if this thread is blocked */
        bool is_blocked() const { return state == THREAD_BLOCKED; }

diff --git a/threads.cc b/threads.cc
index 942d183fd2b23a025e702ea48bdf2cc29391b1f4..aef263ec4624418c2fc050cd3a998e8ad80bd878 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -357,12 +357,12 @@ void Thread::freeResources() {
                stack_free(stack);
 #ifdef TLS
        if (this != model->getInitThread()) {
-               ASSERT(thread_current()==NULL);
                real_pthread_mutex_unlock(&mutex2);
                real_pthread_join(thread, NULL);
                stack_free(helper_stack);
        }
 #endif
+       state = THREAD_FREED;
 }
 
 /**
@@ -378,6 +378,7 @@ Thread::Thread(thread_id_t tid) :
        acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
+       wakeup_state(false),
        start_routine(NULL),
        arg(NULL),
        stack(NULL),
@@ -404,6 +405,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread
        acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
+       wakeup_state(false),
        start_routine(func),
        pstart_routine(NULL),
        arg(a),
@@ -437,6 +439,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Threa
        acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
+       wakeup_state(false),
        start_routine(NULL),
        pstart_routine(func),
        arg(a),