From 1517deafbf0cb93bfc14b4bb40609af63ccf8417 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 3 May 2012 11:33:19 -0700 Subject: [PATCH] clockvector: add ClockVector class --- Makefile | 6 ++--- clockvector.cc | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++ clockvector.h | 20 +++++++++++++++++ 3 files changed, 84 insertions(+), 3 deletions(-) create mode 100644 clockvector.cc create mode 100644 clockvector.h 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 +#include + +#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__ */ -- 2.34.1