action: return synchronization status for ModelAction::read_from()
authorBrian Norris <banorris@uci.edu>
Tue, 25 Sep 2012 23:29:14 +0000 (16:29 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 4 Oct 2012 00:01:42 +0000 (17:01 -0700)
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
action.h

index 08fe106..20777f9 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;
 }
 
 /**
index 32cada2..d178976 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;