From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 17:36:06 +0000 (-0700)
Subject: model: check_recency - "already_added" always true
X-Git-Tag: pldi2013~177^2^2~12^2~2
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8060b81309297c5d890f5229fd6c6fb2bb350b07;p=model-checker.git

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 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);