From 53748c53db55c1230d4b191caf0e4016a2b9c0a6 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 23 Aug 2012 12:31:08 -0700
Subject: [PATCH] action, clockvector: add 'has_synchronized_with()' functions

These functions will check whether a ClockVector (or corresponding ModelAction)
is *completely* synchronized with another already. This is different from
simply "happens before," because I may need to update and propagate a clock
vector after initial execution as more information becomes available, and so
this function helps determine whether a particular pair of vectors is worth
merging (and then - expensively - propagating) before actually performing the
synchronization.

[Not documented properly yet...]
---
 action.cc      |  5 +++++
 action.h       |  1 +
 clockvector.cc | 11 +++++++++++
 clockvector.h  |  1 +
 4 files changed, 18 insertions(+)

diff --git a/action.cc b/action.cc
index b435524..a321a85 100644
--- a/action.cc
+++ b/action.cc
@@ -186,6 +186,11 @@ void ModelAction::synchronize_with(const ModelAction *act) {
 	cv->merge(act->cv);
 }
 
+bool ModelAction::has_synchronized_with(const ModelAction *act) const
+{
+	return cv->has_synchronized_with(act->cv);
+}
+
 /**
  * Check whether 'this' happens before act, according to the memory-model's
  * happens before relation. This is checked via the ClockVector constructs.
diff --git a/action.h b/action.h
index a87e1f2..6559928 100644
--- a/action.h
+++ b/action.h
@@ -83,6 +83,7 @@ public:
 	void read_from(const ModelAction *act);
 	void synchronize_with(const ModelAction *act);
 
+	bool has_synchronized_with(const ModelAction *act) const;
 	bool happens_before(const ModelAction *act) const;
 
 	inline bool operator <(const ModelAction& act) const {
diff --git a/clockvector.cc b/clockvector.cc
index 6c6e2fa..594daa8 100644
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -84,6 +84,17 @@ bool ClockVector::synchronized_since(const ModelAction *act) const
 	return false;
 }
 
+bool ClockVector::has_synchronized_with(const ClockVector *cv) const
+{
+	ASSERT(cv);
+	if (cv->num_threads > num_threads)
+		return false;
+	for (int i = 0; i < cv->num_threads; i++)
+		if (cv->clock[i] > clock[i])
+			return false;
+	return true;
+}
+
 /** Gets the clock corresponding to a given thread id from the clock vector. */
 modelclock_t ClockVector::getClock(thread_id_t thread) {
 	int threadid = id_to_int(thread);
diff --git a/clockvector.h b/clockvector.h
index 56037eb..f2716db 100644
--- a/clockvector.h
+++ b/clockvector.h
@@ -18,6 +18,7 @@ public:
 	~ClockVector();
 	void merge(const ClockVector *cv);
 	bool synchronized_since(const ModelAction *act) const;
+	bool has_synchronized_with(const ClockVector *cv) const;
 
 	void print() const;
 	modelclock_t getClock(thread_id_t thread);
-- 
2.34.1