#include <stdio.h>
#define __STDC_FORMAT_MACROS
#include <inttypes.h>
+#include <vector>
#include "model.h"
#include "action.h"
void ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
- if (act!=NULL && act->is_release() && this->is_acquire()) {
- synchronize_with(act);
- }
reads_from = act;
+ if (act != NULL && this->is_acquire()) {
+ std::vector<const ModelAction *> release_heads;
+ model->get_release_seq_heads(this, &release_heads);
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ synchronize_with(release_heads[i]);
+ }
}
/**
* @param act The ModelAction to synchronize with
*/
void ModelAction::synchronize_with(const ModelAction *act) {
+ ASSERT(*act < *this);
model->check_promises(cv, act->cv);
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.