From: Brian Norris <banorris@uci.edu>
Date: Wed, 14 Mar 2012 22:05:54 +0000 (-0700)
Subject: model: change 'struct model_checker' to 'class ModelChecker'
X-Git-Tag: pldi2013~581
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=dcd84cc88d70497bdc173c4bb78ce30afe4fb5c5;p=model-checker.git

model: change 'struct model_checker' to 'class ModelChecker'
---

diff --git a/libthreads.c b/libthreads.c
index ca31067..2ffe958 100644
--- a/libthreads.c
+++ b/libthreads.c
@@ -5,7 +5,7 @@
 #include "schedule.h"
 #include "common.h"
 
-/* global "model" struct */
+/* global "model" object */
 #include "model.h"
 
 #define STACK_SIZE (1024 * 1024)
@@ -47,7 +47,7 @@ static int create_context(struct thread *t)
 static int create_initial_thread(struct thread *t)
 {
 	memset(t, 0, sizeof(*t));
-	model_checker_assign_id(t);
+	model->assign_id(t);
 	return create_context(t);
 }
 
@@ -107,7 +107,7 @@ int thread_create(struct thread *t, void (*start_routine)(), void *arg)
 	DBG();
 
 	memset(t, 0, sizeof(*t));
-	model_checker_assign_id(t);
+	model->assign_id(t);
 	DEBUG("create thread %d\n", t->id);
 
 	t->start_routine = start_routine;
@@ -154,11 +154,11 @@ int main()
 	struct thread user_thread;
 	struct thread *main_thread;
 
-	model_checker_init();
+	model = new ModelChecker();
 
 	main_thread = (struct thread *)malloc(sizeof(*main_thread));
 	create_initial_thread(main_thread);
-	model_checker_add_system_thread(main_thread);
+	model->add_system_thread(main_thread);
 
 	/* Start user program */
 	thread_create(&user_thread, &user_main, NULL);
diff --git a/model.c b/model.c
index a8a6936..858b919 100644
--- a/model.c
+++ b/model.c
@@ -3,35 +3,31 @@
 #include <stdlib.h>
 #include <string.h>
 
-struct model_checker *model;
+ModelChecker *model;
 
-void model_checker_add_system_thread(struct thread *t)
+ModelChecker::ModelChecker()
 {
-	model->system_thread = t;
-}
-
-void model_checker_init(void)
-{
-	model = (struct model_checker *)malloc(sizeof(*model));
-	memset(model, 0, sizeof(*model));
-
 	/* First thread created (system_thread) will have id 1 */
-	model->used_thread_id = 0;
+	this->used_thread_id = 0;
 
-	scheduler_init(model);
+	scheduler_init(this);
 }
 
-void model_checker_exit(void)
+ModelChecker::~ModelChecker()
 {
 	struct scheduler *sched = model->scheduler;
 
 	if (sched->exit)
 		sched->exit();
 	free(sched);
-	free(model);
 }
 
-void model_checker_assign_id(struct thread *t)
+void ModelChecker::assign_id(struct thread *t)
 {
-	t->id = ++model->used_thread_id;
+	t->id = ++this->used_thread_id;
+}
+
+void ModelChecker::add_system_thread(struct thread *t)
+{
+	model->system_thread = t;
 }
diff --git a/model.h b/model.h
index 625d272..31e88fe 100644
--- a/model.h
+++ b/model.h
@@ -1,18 +1,20 @@
 #ifndef __MODEL_H__
 #define __MODEL_H__
 
-struct model_checker {
+class ModelChecker {
+public:
+	ModelChecker();
+	~ModelChecker();
 	struct scheduler *scheduler;
 	struct thread *system_thread;
 
-	/* "Private" fields */
+	void add_system_thread(struct thread *t);
+	void assign_id(struct thread *t);
+
+private:
 	int used_thread_id;
 };
 
-extern struct model_checker *model;
-
-void model_checker_init(void);
-void model_checker_add_system_thread(struct thread *t);
-void model_checker_assign_id(struct thread *t);
+extern ModelChecker *model;
 
 #endif /* __MODEL_H__ */
diff --git a/schedule.c b/schedule.c
index f4f1c13..0cb1648 100644
--- a/schedule.c
+++ b/schedule.c
@@ -73,7 +73,7 @@ static struct thread *default_thread_current(void)
 	return current;
 }
 
-void scheduler_init(struct model_checker *mod)
+void scheduler_init(ModelChecker *mod)
 {
 	struct scheduler *sched;
 
diff --git a/schedule.h b/schedule.h
index bae8c1f..28f5b8d 100644
--- a/schedule.h
+++ b/schedule.h
@@ -14,6 +14,6 @@ struct scheduler {
 	void *priv;
 };
 
-void scheduler_init(struct model_checker *mod);
+void scheduler_init(ModelChecker *mod);
 
 #endif /* __SCHEDULE_H__ */