model: remove unnecessary parameter to ModelChecker::process_read

The current Thread can be generated later.

diff --git a/model.cc b/model.cc
index 031f6a935ec5701bdf72fdf2bdfe321e70712a28..80cbbe0302709d18bc7c173c40a1d400760a6fea 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -262,11 +262,11 @@ ModelAction * ModelChecker::get_next_backtrack()
 /**
  * Processes a read or rmw model action.
  * @param curr is the read model action to process.
- * @param th is the thread
  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
  * @return True if processing this read updates the mo_graph.
  */
-bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
+bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+{
        uint64_t value;
        bool updated = false;
        while (true) {
@@ -300,7 +300,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                        Promise *valuepromise = new Promise(curr, value, expiration);
                        promises->push_back(valuepromise);
                }
-               th->set_return_value(value);
+               get_thread(curr)->set_return_value(value);
                return updated;
        }
 }
@@ -395,7 +395,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        bool updated = false;
 
        if (curr->is_read()) {
-               updated = process_read(curr, get_thread(curr), second_part_of_rmw);
+               updated = process_read(curr, second_part_of_rmw);
        }
 
        if (curr->is_write()) {

diff --git a/model.h b/model.h
index bd8791964baee4982c058c05c42d3678a7f621da..7db1a8d8701922d691c9827f1be52b7bcb5b002d 100644 (file)
--- a/model.h
+++ b/model.h
@@ -110,7 +110,7 @@ private:
         */
        void set_current_action(ModelAction *act) { priv->current_action = act; }
        Thread * check_current_action(ModelAction *curr);
-       bool process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw);
+       bool process_read(ModelAction *curr, bool second_part_of_rmw);
 
        bool take_step();