From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 17:29:04 +0000 (-0700)
Subject: model: bugfix get_last_seq_action()
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=85234dee853ecfdc0ccdb44703a1119b806a465b;p=cdsspec-compiler.git

model: bugfix get_last_seq_action()

The action lists may include the current action, which we don't want to
consider for 'get_last_seq_action()'.

Also, rewrite some of the comments for this function.

Bugfix thanks to Brian D.
---

diff --git a/model.cc b/model.cc
index acd2079..96ee3de 100644
--- a/model.cc
+++ b/model.cc
@@ -758,7 +758,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 	if (curr->is_seqcst()) {
 		/* We have to at least see the last sequentially consistent write,
 			 so we are initialized. */
-		ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
+		ModelAction *last_seq_cst = get_last_seq_cst(curr);
 		if (last_seq_cst != NULL) {
 			mo_graph->addEdge(last_seq_cst, curr);
 			added = true;
@@ -1079,18 +1079,21 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
 }
 
 /**
- * Gets the last memory_order_seq_cst action (in the total global sequence)
- * performed on a particular object (i.e., memory location).
- * @param location The object location to check
- * @return The last seq_cst action performed
+ * Gets the last memory_order_seq_cst write (in the total global sequence)
+ * performed on a particular object (i.e., memory location), not including the
+ * current action.
+ * @param curr The current ModelAction; also denotes the object location to
+ * check
+ * @return The last seq_cst write
  */
-ModelAction * ModelChecker::get_last_seq_cst(const void *location)
+ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr)
 {
+	void *location = curr->get_location();
 	action_list_t *list = obj_map->get_safe_ptr(location);
 	/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
 	for (rit = list->rbegin(); rit != list->rend(); rit++)
-		if ((*rit)->is_write() && (*rit)->is_seqcst())
+		if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
 			return *rit;
 	return NULL;
 }
@@ -1204,7 +1207,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 	bool initialized = false;
 
 	if (curr->is_seqcst()) {
-		last_seq_cst = get_last_seq_cst(curr->get_location());
+		last_seq_cst = get_last_seq_cst(curr);
 		/* We have to at least see the last sequentially consistent write,
 			 so we are initialized. */
 		if (last_seq_cst != NULL)
diff --git a/model.h b/model.h
index 4fc32c6..9c8fa87 100644
--- a/model.h
+++ b/model.h
@@ -129,7 +129,7 @@ private:
 	void check_curr_backtracking(ModelAction * curr);
 	void add_action_to_lists(ModelAction *act);
 	ModelAction * get_last_action(thread_id_t tid);
-	ModelAction * get_last_seq_cst(const void *location);
+	ModelAction * get_last_seq_cst(ModelAction *curr);
 	void build_reads_from_past(ModelAction *curr);
 	ModelAction * process_rmw(ModelAction *curr);
 	void post_r_modification_order(ModelAction *curr, const ModelAction *rf);