model: check_recency - "already_added" always true

The current action is always part of the lists now.

Bugfix thanks to Brian D.

diff --git a/model.cc b/model.cc
index 96ee3de6325156a75f1952df6cbba0415232ed80..d8ae7ea4bf1eaa3c4ec2830d8c69f882ddb873c0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -281,7 +281,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        bool r_status = false;
 
                        if (!second_part_of_rmw) {
-                               check_recency(curr,false);
+                               check_recency(curr);
                                r_status = r_modification_order(curr, reads_from);
                        }
 
@@ -531,7 +531,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  *
  * If so, we decide that the execution is no longer feasible.
  */
-void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
+void ModelChecker::check_recency(ModelAction *curr) {
        if (params.maxreads != 0) {
                if (curr->get_node()->get_read_from_size() <= 1)
                        return;
@@ -552,12 +552,10 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 
                action_list_t::reverse_iterator rit = list->rbegin();
                /* Skip past curr */
-               if (already_added) {
-                       for (; (*rit) != curr; rit++)
-                               ;
-                       /* go past curr now */
-                       rit++;
-               }
+               for (; (*rit) != curr; rit++)
+                       ;
+               /* go past curr now */
+               rit++;
 
                action_list_t::reverse_iterator ritcopy = rit;
                //See if we have enough reads from the same value

diff --git a/model.h b/model.h
index 9c8fa87f2076a5f7c369c231d3bba89c0b93ca3b..030d7ddf67723aa1878364e4a7f84c8898136f81 100644 (file)
--- a/model.h
+++ b/model.h
@@ -117,7 +117,7 @@ private:
 
        bool take_step();
 
-       void check_recency(ModelAction *curr, bool already_added);
+       void check_recency(ModelAction *curr);
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
        Thread * get_next_thread(ModelAction *curr);