From 8060b81309297c5d890f5229fd6c6fb2bb350b07 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 18 Sep 2012 10:36:06 -0700 Subject: [PATCH] model: check_recency - "already_added" always true The current action is always part of the lists now. Bugfix thanks to Brian D. --- model.cc | 14 ++++++-------- model.h | 2 +- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/model.cc b/model.cc index 96ee3de..d8ae7ea 100644 --- 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 9c8fa87..030d7dd 100644 --- 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); -- 2.34.1