model/action: move complicated read_from logic into model.cc
authorBrian Norris <banorris@uci.edu>
Tue, 4 Dec 2012 02:14:55 +0000 (18:14 -0800)
committerBrian Norris <banorris@uci.edu>
Tue, 4 Dec 2012 02:26:48 +0000 (18:26 -0800)
The release sequence wrapper logic will only get more complicated, so
rather than spreading across two files and exporting more interfaces,
just integrate into ModelChecker.

action.cc
action.h
model.cc
model.h

index 5ecc1f0..41a025a 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -337,24 +337,10 @@ void ModelAction::set_try_lock(bool obtainedlock) {
 /**
  * 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)
+void ModelAction::set_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])) {
-                               model->set_bad_synchronization();
-                               num_heads--;
-                       }
-               return num_heads > 0;
-       }
-       return false;
 }
 
 /**
index 4c40bd9..82b8532 100644 (file)
--- a/action.h
+++ b/action.h
@@ -85,6 +85,8 @@ public:
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
 
+       void set_read_from(const ModelAction *act);
+
        /** Store the most recent fence-release from the same thread
         *  @param fence The fence-release that occured prior to this */
        void set_last_fence_release(const ModelAction *fence) { last_fence_release = fence; }
@@ -123,7 +125,6 @@ public:
 
        void create_cv(const ModelAction *parent = NULL);
        ClockVector * get_cv() const { return cv; }
-       bool read_from(const ModelAction *act);
        bool synchronize_with(const ModelAction *act);
 
        bool has_synchronized_with(const ModelAction *act) const;
index f96249f..2f9ec63 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -705,7 +705,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                                continue;
                        }
 
-                       curr->read_from(reads_from);
+                       read_from(curr, reads_from);
                        mo_graph->commitChanges();
                        mo_check_promises(curr->get_tid(), reads_from);
 
@@ -714,7 +714,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        /* Read from future value */
                        value = curr->get_node()->get_future_value();
                        modelclock_t expiration = curr->get_node()->get_future_value_expiration();
-                       curr->read_from(NULL);
+                       read_from(curr, NULL);
                        Promise *valuepromise = new Promise(curr, value, expiration);
                        promises->push_back(valuepromise);
                }
@@ -1047,6 +1047,34 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
        }
 }
 
+/**
+ * @brief Establish reads-from relation between two actions
+ *
+ * Perform basic operations involved with establishing a concrete rf relation,
+ * including setting the ModelAction data and checking for release sequences.
+ *
+ * @param act The action that is reading (must be a read)
+ * @param rf The action from which we are reading (must be a write)
+ *
+ * @return True if this read established synchronization
+ */
+bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
+{
+       act->set_read_from(rf);
+       if (rf != NULL && act->is_acquire()) {
+               rel_heads_list_t release_heads;
+               get_release_seq_heads(act, &release_heads);
+               int num_heads = release_heads.size();
+               for (unsigned int i = 0; i < release_heads.size(); i++)
+                       if (!act->synchronize_with(release_heads[i])) {
+                               set_bad_synchronization();
+                               num_heads--;
+                       }
+               return num_heads > 0;
+       }
+       return false;
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -2154,7 +2182,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        if (read->is_rmw()) {
                                mo_graph->addRMWEdge(write, read);
                        }
-                       read->read_from(write);
+                       read_from(read, write);
                        //First fix up the modification order for actions that happened
                        //before the read
                        r_modification_order(read, write);
diff --git a/model.h b/model.h
index fd99700..6bb4788 100644 (file)
--- a/model.h
+++ b/model.h
@@ -153,6 +153,7 @@ private:
        bool process_mutex(ModelAction *curr);
        bool process_thread_action(ModelAction *curr);
        void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
+       bool read_from(ModelAction *act, const ModelAction *rf);
        bool check_action_enabled(ModelAction *curr);
 
        bool take_step();