From: Brian Norris <banorris@uci.edu>
Date: Thu, 21 Jun 2012 08:48:03 +0000 (-0700)
Subject: clockvector: fix 'happens_before', change name to 'synchronized_since'
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=e8bc4a0715ce1c86f3ff7d24179e1164bf3ee61b

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 f411f50d..2ef8b03d 100644
--- 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 e9ffb2bf..d233cdd1 100644
--- 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();