model/action: move complicated read_from logic into model.cc

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.

diff --git a/action.cc b/action.cc
index 5ecc1f0e1b26f069650a47e139858eef68e05595..41a025ab7e6f463f4e1068b029e6fbf26683d39f 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
 /**
  * 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;
        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;

 }
 
 /**
 }
 
 /**

diff --git a/action.h b/action.h
index 4c40bd9bf9a4554ed7c984158334f359346031c5..82b8532dacb97b4c748620b4b5af8308d377ed6a 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; }
 
        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; }
        /** 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; }
 
        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;
        bool synchronize_with(const ModelAction *act);
 
        bool has_synchronized_with(const ModelAction *act) const;

diff --git a/model.cc b/model.cc
index f96249fcb9cf9ceeb9eb0b97b5a13c9b74b96b60..2f9ec63f00d5e6bf113c18d17386dfc22eeea7cd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -705,7 +705,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                                continue;
                        }
 
                                continue;
                        }
 

-                       curr->read_from(reads_from);
+                       read_from(curr, reads_from);

                        mo_graph->commitChanges();
                        mo_check_promises(curr->get_tid(), 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();
                        /* 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);
                }
                        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.
  *
 /**
  * @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);
                        }
                        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);
                        //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 fd99700a01c35f77ff2d87445ee228b71ae69de5..6bb4788c061b90e427720214756c144a2ff325fc 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 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();
        bool check_action_enabled(ModelAction *curr);
 
        bool take_step();