clockvector: fix 'happens_before', change name to 'synchronized_since'
authorBrian Norris <banorris@uci.edu>
Thu, 21 Jun 2012 08:48:03 +0000 (01:48 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 21 Jun 2012 08:48:03 +0000 (01:48 -0700)
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.

clockvector.cc
clockvector.h

index f411f50..2ef8b03 100644 (file)
@@ -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;
 }
 
index e9ffb2b..d233cdd 100644 (file)
@@ -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();