From: Brian Demsky Date: Sat, 3 Nov 2012 03:26:19 +0000 (-0700) Subject: previous synchronization was weird... X-Git-Tag: pldi2013~13^2~7^2~1 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=37bf8e7d54c72e0aeee029a491e45bb9d7b2f409 previous synchronization was weird... --- diff --git a/action.cc b/action.cc index 140d590..1387ed1 100644 --- a/action.cc +++ b/action.cc @@ -365,7 +365,7 @@ bool ModelAction::synchronize_with(const ModelAction *act) { bool ModelAction::has_synchronized_with(const ModelAction *act) const { - return cv->has_synchronized_with(act->cv); + return cv->synchronized_since(act); } /** diff --git a/clockvector.cc b/clockvector.cc index 7d947c6..e56c2ac 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -75,17 +75,6 @@ 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 6a902c5..9000a5d 100644 --- a/clockvector.h +++ b/clockvector.h @@ -17,7 +17,6 @@ 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);