From: Brian Norris <banorris@uci.edu>
Date: Tue, 24 Apr 2012 03:13:02 +0000 (-0700)
Subject: threads: set up Thread to be freed properly
X-Git-Tag: pldi2013~513
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c0eda11361a71ff8cef84164ddedab9dd875c20a;p=model-checker.git

threads: set up Thread to be freed properly

To ensure that we can free memory properly, set up a destructor and rename
dispose() to complete().
---

diff --git a/threads.cc b/threads.cc
index 3af7496..7d4d22e 100644
--- a/threads.cc
+++ b/threads.cc
@@ -53,11 +53,13 @@ int Thread::swap(Thread *t)
 	return swapcontext(&this->context, &t->context);
 }
 
-void Thread::dispose()
+void Thread::complete()
 {
-	DEBUG("completed thread %d\n", thread_current()->get_id());
-	state = THREAD_COMPLETED;
-	stack_free(stack);
+	if (state != THREAD_COMPLETED) {
+		DEBUG("completed thread %d\n", get_id());
+		state = THREAD_COMPLETED;
+		stack_free(stack);
+	}
 }
 
 Thread::Thread(thrd_t *t, void (*func)(), void *a) {
@@ -90,6 +92,12 @@ Thread::Thread(thrd_t *t) {
 	model->add_system_thread(this);
 }
 
+Thread::~Thread()
+{
+	complete();
+	model->remove_thread(this);
+}
+
 thread_id_t Thread::get_id()
 {
 	return id;
@@ -109,7 +117,7 @@ static int thread_system_next(void)
 			model->scheduler->add_thread(curr);
 		else if (curr->get_state() == THREAD_RUNNING)
 			/* Stopped while running; i.e., completed */
-			curr->dispose();
+			curr->complete();
 		else
 			DEBUG("ERROR: current thread in unexpected state??\n");
 	}
diff --git a/threads.h b/threads.h
index 0c5fdab..4a80251 100644
--- a/threads.h
+++ b/threads.h
@@ -18,8 +18,9 @@ class Thread {
 public:
 	Thread(thrd_t *t, void (*func)(), void *a);
 	Thread(thrd_t *t);
+	~Thread();
+	void complete();
 	int swap(Thread *t);
-	void dispose();
 
 	thread_state get_state() { return state; }
 	void set_state(thread_state s) { state = s; }