From: Brian Norris <banorris@uci.edu>
Date: Tue, 10 Apr 2012 21:51:30 +0000 (-0700)
Subject: model: add class ModelAction
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3ec8b2cabc09653e410e28531669102d2bab449b;p=c11tester.git

model: add class ModelAction

Represents a single action (sometimes called transition) in our program. This
can be a THREAD_* event (creation, join, etc.) or a relevant read/write
operation (e.g., atomic reads/writes). This object and interface is subject to
change a little...
---

diff --git a/model.cc b/model.cc
index b97352a9..19194cda 100644
--- a/model.cc
+++ b/model.cc
@@ -1,3 +1,5 @@
+#include <stdio.h>
+
 #include "model.h"
 #include "schedule.h"
 
@@ -25,3 +27,41 @@ void ModelChecker::add_system_thread(struct thread *t)
 {
 	this->system_thread = t;
 }
+
+ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
+{
+	struct thread *t = thread_current();
+	ModelAction *act = this;
+
+	act->type = type;
+	act->order = order;
+	act->location = loc;
+	act->tid = t->id;
+	act->value = value;
+}
+
+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("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
+}
diff --git a/model.h b/model.h
index a9016338..d3229b29 100644
--- a/model.h
+++ b/model.h
@@ -2,6 +2,30 @@
 #define __MODEL_H__
 
 #include "schedule.h"
+#include "libthreads.h"
+#include "libatomic.h"
+
+#define VALUE_NONE -1
+
+typedef enum action_type {
+	THREAD_CREATE,
+	THREAD_YIELD,
+	THREAD_JOIN,
+	ATOMIC_READ,
+	ATOMIC_WRITE
+} action_type_t;
+
+class ModelAction {
+public:
+	ModelAction(action_type_t type, memory_order order, void *loc, int value);
+	void print(void);
+private:
+	action_type type;
+	memory_order order;
+	void *location;
+	thread_id_t tid;
+	int value;
+};
 
 class ModelChecker {
 public: