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...]
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.
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 {
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);
~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);