From 5ead9124f62d38a96f606ddbcfc8a62c8d5f8335 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 25 Sep 2012 16:29:14 -0700
Subject: [PATCH] action: return synchronization status for
ModelAction::read_from()
The ModelChecker may need to know if any synchronization was performed in
read_from().
Note that the return status is not used yet.
---
action.cc | 15 ++++++++++++---
action.h | 2 +-
2 files changed, 13 insertions(+), 4 deletions(-)
diff --git a/action.cc b/action.cc
index 08fe106..20777f9 100644
--- a/action.cc
+++ b/action.cc
@@ -249,18 +249,27 @@ void ModelAction::set_try_lock(bool obtainedlock) {
value=VALUE_TRYFAILED;
}
-/** Update the model action's read_from action */
-void ModelAction::read_from(const ModelAction *act)
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ * @return True if this read established synchronization
+ */
+bool ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
reads_from = act;
if (act != NULL && this->is_acquire()) {
rel_heads_list_t release_heads;
model->get_release_seq_heads(this, &release_heads);
+ int num_heads = release_heads.size();
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!synchronize_with(release_heads[i]))
+ if (!synchronize_with(release_heads[i])) {
model->set_bad_synchronization();
+ num_heads--;
+ }
+ return num_heads > 0;
}
+ return false;
}
/**
diff --git a/action.h b/action.h
index 32cada2..d178976 100644
--- a/action.h
+++ b/action.h
@@ -105,7 +105,7 @@ public:
void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
- void read_from(const ModelAction *act);
+ bool read_from(const ModelAction *act);
bool synchronize_with(const ModelAction *act);
bool has_synchronized_with(const ModelAction *act) const;
--
2.34.1