From: Brian Norris <banorris@uci.edu>
Date: Thu, 19 Apr 2012 18:02:48 +0000 (-0700)
Subject: model: flesh out set_backtracking()
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=8fc5d0e4410b56a1e17e8e219397abf53f8ba462;p=c11tester.git

model: flesh out set_backtracking()

Relies on stub get_last_conflict() function.

Note: so far, implementing based on seq_cst model, not the full memory model...
---

diff --git a/model.cc b/model.cc
index 67222e9f..37baf9b5 100644
--- a/model.cc
+++ b/model.cc
@@ -35,6 +35,34 @@ void ModelChecker::add_system_thread(Thread *t)
 	this->system_thread = t;
 }
 
+void ModelChecker::set_backtracking(ModelAction *act)
+{
+	ModelAction *prev;
+	TreeNode *node;
+
+	prev = get_last_conflict(act);
+	if (prev == NULL)
+		return;
+
+	node = prev->get_node();
+
+	/* Check if this has been explored already */
+	if (node->hasBeenExplored(act->get_tid()))
+		return;
+	/* If this is a new backtracking point, mark the tree */
+	if (node->setBacktrack(act->get_tid()) != 0)
+		return;
+
+	printf("Setting backtrack: conflict = %d, instead tid = %d\n",
+			prev->get_tid(), act->get_tid());
+	prev->print();
+	act->print();
+
+	/* FIXME */
+	//Backtrack *back = new Backtrack(prev, actionList);
+	//backtrackList->Append(back);
+}
+
 void ModelChecker::check_current_action(void)
 {
 	ModelAction *next = this->current_action;
diff --git a/model.h b/model.h
index b6a0004d..152d83c3 100644
--- a/model.h
+++ b/model.h
@@ -51,6 +51,7 @@ public:
 	void add_system_thread(Thread *t);
 
 	void set_current_action(ModelAction *act) { current_action = act; }
+	ModelAction *get_last_conflict(ModelAction *act);
 	void check_current_action(void);
 	void set_backtracking(ModelAction *act);
 	void print_trace(void);