clockvector: fix 'happens_before', change name to 'synchronized_since'

First, the 'happens_before' function needed to use an inclusive 'less-than'
(i.e., <=) instead of 'strictly less-than' (i.e., <) in order to fit with
most of the algorithm.

Second, the association of 'happens_before' directly with the ClockVector is
not very intuitive to use. I will write an additional happens_before()
function that can easily compare two ModelAction objects. So change this
happens_before() (with it awkward usage) to be called synchronized_since(),
representing whether the ClockVector's thread has previously synchronized
with the ModelAction's thread.

diff --git a/clockvector.cc b/clockvector.cc
index f411f50d64bcb9ca6c1b7eefe48f871bcc1c1bff..2ef8b03d9e36e22ce4ee6989ec31d20633717ed2 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -49,12 +49,18 @@ void ClockVector::merge(ClockVector *cv)
        clock = clk;
 }
 
-bool ClockVector::happens_before(ModelAction *act, thread_id_t id)
+/**
+ *
+ * @return true if this ClockVector's thread has synchronized with act's
+ * thread, false otherwise. That is, this function returns:
+ * <BR><CODE>act <= cv[act->tid]</CODE>
+ */
+bool ClockVector::synchronized_since(ModelAction *act)
 {
-       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;
 }
 

diff --git a/clockvector.h b/clockvector.h
index e9ffb2bf5c4997452bbddb0f8d650e319ce7f777..d233cdd136c46f7e00c547f9ac1d4be95d62cdee 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -16,7 +16,7 @@ public:
        ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
        ~ClockVector();
        void merge(ClockVector *cv);
-       bool happens_before(ModelAction *act, thread_id_t id);
+       bool synchronized_since(ModelAction *act);
 
        void print();