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 67222e9f0c5cdf1be3a22edf882910439c72dc39..37baf9b504b44c8a1894fba92e673216007c432d 100644 (file)
--- 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 b6a0004d5a3d119e413d01e5184741930ac5e505..152d83c3d633efb1d9185d6201605fdefba3c5c6 100644 (file)
--- 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);