X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=clockvector.cc;h=95896ed3a61a7d62b725028b04d7c939245f83a8;hb=cf7518cb8c2d9cd3033ca7540ea9dc448b21912a;hp=69503aaf2a01f8df55c3f9626179cc3e39e12ba7;hpb=310276660b83b8dd313c512f07510268bcc1e3fc;p=c11tester.git diff --git a/clockvector.cc b/clockvector.cc index 69503aaf..95896ed3 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -1,31 +1,43 @@ #include #include +#include #include "model.h" #include "action.h" #include "clockvector.h" #include "common.h" +/** + * Constructs a new ClockVector, given a parent ClockVector and a first + * ModelAction. This constructor can assign appropriate default settings if no + * parent and/or action is supplied. + * @param parent is the previous ClockVector to inherit (i.e., clock from the + * same thread or the parent that created this thread) + * @param act is an action with which to update the ClockVector + */ ClockVector::ClockVector(ClockVector *parent, ModelAction *act) { - num_threads = parent ? parent->num_threads : 1; - if (act && act->get_type() == THREAD_CREATE) - num_threads++; + num_threads = model->get_num_threads(); clock = (int *)MYMALLOC(num_threads * sizeof(int)); + memset(clock, 0, 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(); } +/** @brief Destructor */ ClockVector::~ClockVector() { MYFREE(clock); } +/** + * Merge a clock vector into this vector, using a pairwise vector. The + * resulting vector length will be the maximum length of the two being merged. + * @param cv is the ClockVector being merged into this vector. + */ void ClockVector::merge(ClockVector *cv) { int *clk = clock; @@ -51,18 +63,32 @@ void ClockVector::merge(ClockVector *cv) clock = clk; } -bool ClockVector::happens_before(ModelAction *act, thread_id_t id) +/** + * Check whether this vector's thread has synchronized with another action's + * thread. This effectively checks the happens-before relation (or actually, + * happens after), but it's easier to compare two ModelAction events directly, + * using ModelAction::happens_before. + * + * @see ModelAction::happens_before + * + * @return true if this ClockVector's thread has synchronized with act's + * thread, false otherwise. That is, this function returns: + *
act <= cv[act->tid] + */ +bool ClockVector::synchronized_since(ModelAction *act) const { - int i = id_to_int(id); + int i = id_to_int(act->get_tid()); if (i < num_threads) - return act->get_seq_number() < clock[i]; + return act->get_seq_number() <= clock[i]; return false; } -void ClockVector::print() +/** @brief Formats and prints this ClockVector's data. */ +void ClockVector::print() const { int i; + printf("CV: ("); for (i = 0; i < num_threads; i++) - printf("%d%c", clock[i], (i == num_threads - 1) ? '\n' : ' '); + printf("%2d%s", clock[i], (i == num_threads - 1) ? ")\n" : ", "); }