From: Brian Norris <banorris@uci.edu>
Date: Thu, 3 May 2012 18:33:19 +0000 (-0700)
Subject: clockvector: add ClockVector class
X-Git-Tag: pldi2013~450
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1517deafbf0cb93bfc14b4bb40609af63ccf8417;p=model-checker.git

clockvector: add ClockVector class
---

diff --git a/Makefile b/Makefile
index 0f9bf00..093f422 100644
--- a/Makefile
+++ b/Makefile
@@ -8,9 +8,9 @@ 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 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
diff --git a/clockvector.cc b/clockvector.cc
new file mode 100644
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
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__ */