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...]

diff --git a/action.cc b/action.cc
index b435524d6d4a423405e221724794e8fcfeae4f84..a321a85edede7f0b12a47142f61e44a33f561cbd 100644 (file)
--- 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 a87e1f2343ad82eb1428bdf696e5766e6d05886c..6559928b14f6131489fe0c1e6ddc508e28a58ae5 100644 (file)
--- 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 6c6e2fa579e606377ec45bed18bddac8d357cbb8..594daa8a75d968f500d3248085045a559c3e13fa 100644 (file)
--- 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 56037eb6bfcd2f37a5110d12a7f733e79faad8b0..f2716dbd90497c9f260b1730bee9d25bc9c622fd 100644 (file)
--- 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);