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 b97352a97f15baebbf2c0ff578bab195a444928c..19194cda06a766ccb84b1674b6fb5142bcc4bef4 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1,3 +1,5 @@
+#include <stdio.h>
+

 #include "model.h"
 #include "schedule.h"
 
 #include "model.h"
 #include "schedule.h"
 


@@ -25,3 +27,41 @@ void ModelChecker::add_system_thread(struct thread *t)
 {
        this->system_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 a9016338508eac25e4f1b97bc76a3e429d51fa40..d3229b296526db6ee54c07d0055e22a336011b5a 100644 (file)
--- a/model.h
+++ b/model.h
@@ -2,6 +2,30 @@
 #define __MODEL_H__
 
 #include "schedule.h"
 #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:
 
 class ModelChecker {
 public: