From: Brian Norris <banorris@uci.edu>
Date: Sat, 5 May 2012 07:25:57 +0000 (-0700)
Subject: action: split ModelAction off into action.cc
X-Git-Tag: pldi2013~451
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e759b60e0b2dc31623ba3b03303a9d0d204fdd4c;p=model-checker.git

action: split ModelAction off into action.cc
---

diff --git a/Makefile b/Makefile
index 3de1869..0f9bf00 100644
--- a/Makefile
+++ b/Makefile
@@ -8,8 +8,8 @@ LIB_SO=lib$(LIB_NAME).so
 USER_O=userprog.o
 USER_H=libthreads.h libatomic.h
 
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc main.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o main.o
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc main.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o main.o
 MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h
 
 CPPFLAGS=-Wall -g
diff --git a/action.cc b/action.cc
new file mode 100644
index 0000000..bd9e29f
--- /dev/null
+++ b/action.cc
@@ -0,0 +1,100 @@
+#include <stdio.h>
+
+#include "model.h"
+#include "action.h"
+
+ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
+{
+	Thread *t = thread_current();
+	ModelAction *act = this;
+
+	act->type = type;
+	act->order = order;
+	act->location = loc;
+	act->tid = t->get_id();
+	act->value = value;
+	act->seq_number = model->get_next_seq_num();
+}
+
+bool ModelAction::is_read()
+{
+	return type == ATOMIC_READ;
+}
+
+bool ModelAction::is_write()
+{
+	return type == ATOMIC_WRITE;
+}
+
+bool ModelAction::is_acquire()
+{
+	switch (order) {
+	case memory_order_acquire:
+	case memory_order_acq_rel:
+	case memory_order_seq_cst:
+		return true;
+	default:
+		return false;
+	}
+}
+
+bool ModelAction::is_release()
+{
+	switch (order) {
+	case memory_order_release:
+	case memory_order_acq_rel:
+	case memory_order_seq_cst:
+		return true;
+	default:
+		return false;
+	}
+}
+
+bool ModelAction::same_var(ModelAction *act)
+{
+	return location == act->location;
+}
+
+bool ModelAction::same_thread(ModelAction *act)
+{
+	return tid == act->tid;
+}
+
+bool ModelAction::is_dependent(ModelAction *act)
+{
+	if (!is_read() && !is_write())
+		return false;
+	if (!act->is_read() && !act->is_write())
+		return false;
+	if (same_var(act) && !same_thread(act) &&
+			(is_write() || act->is_write()))
+		return true;
+	return false;
+}
+
+void ModelAction::print(void)
+{
+	const char *type_str;
+	switch (this->type) {
+	case THREAD_CREATE:
+		type_str = "thread create";
+		break;
+	case THREAD_YIELD:
+		type_str = "thread yield";
+		break;
+	case THREAD_JOIN:
+		type_str = "thread join";
+		break;
+	case ATOMIC_READ:
+		type_str = "atomic read";
+		break;
+	case ATOMIC_WRITE:
+		type_str = "atomic write";
+		break;
+	default:
+		type_str = "unknown type";
+	}
+
+	printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
+			seq_number, id_to_int(tid), type_str, order, location, value);
+}
diff --git a/model.cc b/model.cc
index 2c74047..643ad95 100644
--- a/model.cc
+++ b/model.cc
@@ -300,99 +300,3 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	old->set_state(THREAD_READY);
 	return Thread::swap(old, get_system_context());
 }
-
-ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
-{
-	Thread *t = thread_current();
-	ModelAction *act = this;
-
-	act->type = type;
-	act->order = order;
-	act->location = loc;
-	act->tid = t->get_id();
-	act->value = value;
-	act->seq_number = model->get_next_seq_num();
-}
-
-bool ModelAction::is_read()
-{
-	return type == ATOMIC_READ;
-}
-
-bool ModelAction::is_write()
-{
-	return type == ATOMIC_WRITE;
-}
-
-bool ModelAction::is_acquire()
-{
-	switch (order) {
-	case memory_order_acquire:
-	case memory_order_acq_rel:
-	case memory_order_seq_cst:
-		return true;
-	default:
-		return false;
-	}
-}
-
-bool ModelAction::is_release()
-{
-	switch (order) {
-	case memory_order_release:
-	case memory_order_acq_rel:
-	case memory_order_seq_cst:
-		return true;
-	default:
-		return false;
-	}
-}
-
-bool ModelAction::same_var(ModelAction *act)
-{
-	return location == act->location;
-}
-
-bool ModelAction::same_thread(ModelAction *act)
-{
-	return tid == act->tid;
-}
-
-bool ModelAction::is_dependent(ModelAction *act)
-{
-	if (!is_read() && !is_write())
-		return false;
-	if (!act->is_read() && !act->is_write())
-		return false;
-	if (same_var(act) && !same_thread(act) &&
-			(is_write() || act->is_write()))
-		return true;
-	return false;
-}
-
-void ModelAction::print(void)
-{
-	const char *type_str;
-	switch (this->type) {
-	case THREAD_CREATE:
-		type_str = "thread create";
-		break;
-	case THREAD_YIELD:
-		type_str = "thread yield";
-		break;
-	case THREAD_JOIN:
-		type_str = "thread join";
-		break;
-	case ATOMIC_READ:
-		type_str = "atomic read";
-		break;
-	case ATOMIC_WRITE:
-		type_str = "atomic write";
-		break;
-	default:
-		type_str = "unknown type";
-	}
-
-	printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
-			seq_number, id_to_int(tid), type_str, order, location, value);
-}