From: Brian Norris <banorris@uci.edu>
Date: Mon, 12 Mar 2012 22:49:59 +0000 (-0700)
Subject: schedule: add replaceable scheduler struct
X-Git-Tag: pldi2013~597
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3ffc7186fd49a2dd2a5f5756511614fb3f06ac56;p=model-checker.git

schedule: add replaceable scheduler struct

I may need to replace the scheduler in the future, so modularize it.
---

diff --git a/model.h b/model.h
index 7116d54..73c3d0c 100644
--- a/model.h
+++ b/model.h
@@ -2,6 +2,7 @@
 #define __MODEL_H__
 
 struct model_checker {
+	struct scheduler *scheduler;
 };
 
 #endif /* __MODEL_H__ */
diff --git a/schedule.c b/schedule.c
index d567dd7..4ac8b49 100644
--- a/schedule.c
+++ b/schedule.c
@@ -1,6 +1,9 @@
+#include <stdlib.h>
+
 #include "libthreads.h"
 #include "schedule.h"
 #include "common.h"
+#include "model.h"
 
 struct thread_list_node {
 	struct thread *this;
@@ -58,3 +61,17 @@ struct thread *schedule_choose_next(void)
 {
 	return dequeue_thread();
 }
+
+void scheduler_init(struct model_checker *mod)
+{
+	struct scheduler *sched;
+
+	/* Initialize FCFS scheduler */
+	sched = malloc(sizeof(*sched));
+	sched->init = NULL;
+	sched->exit = NULL;
+	sched->add_thread = schedule_add_thread;
+	sched->next_thread = schedule_choose_next;
+	sched->get_current_thread = thread_current;
+	mod->scheduler = sched;
+}
diff --git a/schedule.h b/schedule.h
index ac69fa1..360b390 100644
--- a/schedule.h
+++ b/schedule.h
@@ -2,7 +2,19 @@
 #define __SCHEDULE_H__
 
 #include "libthreads.h"
+#include "model.h"
 
+struct scheduler {
+	void (*init)(void);
+	void (*exit)(void);
+	void (*add_thread)(struct thread *t);
+	struct thread * (*next_thread)(void);
+	struct thread * (*get_current_thread)(void);
+
+	void *priv;
+};
+
+void scheduler_init(struct model_checker *mod);
 void schedule_add_thread(struct thread *t);
 struct thread *schedule_choose_next(void);