clockvector: add ClockVector class

diff --git a/Makefile b/Makefile
index 0f9bf00389680e32971f710b3d1ae88ee4eb262c..093f42299aff26c7df3d7c6b7fc3ed5065715cd9 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -8,9 +8,9 @@ LIB_SO=lib$(LIB_NAME).so
 USER_O=userprog.o
 USER_H=libthreads.h libatomic.h
 
 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 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
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc clockvector.cc main.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o clockvector.o main.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h clockvector.h

 
 CPPFLAGS=-Wall -g
 LDFLAGS=-ldl
 
 CPPFLAGS=-Wall -g
 LDFLAGS=-ldl

diff --git a/clockvector.cc b/clockvector.cc
new file mode 100644 (file)
index 0000000..15e6590
--- /dev/null
+++ b/clockvector.cc
@@ -0,0 +1,61 @@
+#include <algorithm>
+#include <cstring>
+
+#include "model.h"
+#include "action.h"
+#include "clockvector.h"
+#include "common.h"
+
+ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
+{
+       num_threads = parent ? parent->num_threads : 1;
+       if (act && act->get_type() == THREAD_CREATE)
+               num_threads++;
+       clock = (int *)myMalloc(num_threads * sizeof(int));
+       if (parent)
+               std::memcpy(clock, parent->clock, parent->num_threads * sizeof(int));
+       else
+               clock[0] = 0;
+
+       if (act)
+               clock[id_to_int(act->get_tid())] = act->get_seq_number();
+}
+
+ClockVector::~ClockVector()
+{
+       myFree(clock);
+}
+
+void ClockVector::merge(ClockVector *cv)
+{
+       int *clk = clock;
+       bool resize = false;
+
+       ASSERT(cv != NULL);
+
+       if (cv->num_threads > num_threads) {
+               resize = true;
+               clk = (int *)myMalloc(cv->num_threads * sizeof(int));
+       }
+
+       /* Element-wise maximum */
+       for (int i = 0; i < num_threads; i++)
+               clk[i] = std::max(clock[i], cv->clock[i]);
+
+       if (resize) {
+               for (int i = num_threads; i < cv->num_threads; i++)
+                       clk[i] = cv->clock[i];
+               num_threads = cv->num_threads;
+               myFree(clock);
+       }
+       clock = clk;
+}
+
+bool ClockVector::happens_before(ModelAction *act, thread_id_t id)
+{
+       int i = id_to_int(id);
+
+       if (i < num_threads)
+               return act->get_seq_number() < clock[i];
+       return false;
+}

diff --git a/clockvector.h b/clockvector.h
new file mode 100644 (file)
index 0000000..615dfeb
--- /dev/null
+++ b/clockvector.h
@@ -0,0 +1,20 @@
+#ifndef __CLOCKVECTOR_H__
+#define __CLOCKVECTOR_H__
+
+#include "threads.h"
+
+/* Forward declaration */
+class ModelAction;
+
+class ClockVector {
+public:
+       ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
+       ~ClockVector();
+       void merge(ClockVector *cv);
+       bool happens_before(ModelAction *act, thread_id_t id);
+private:
+       int *clock;
+       int num_threads;
+};
+
+#endif /* __CLOCKVECTOR_H__ */