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.

diff --git a/action.cc b/action.cc
index 08fe10677c5d1e7e518c15fc27a4638c7f4494f4..20777f96161cfa84c3130c07f11177258481eb5f 100644 (file)
--- 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 32cada2b9db88f306cf3dc52df6b1bd473640709..d178976a2c8e0206128750b5eaddac1485a4b432 100644 (file)
--- 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;