nodestack: add class NodeStack and class Node

These will replace class TreeNode in the near future, since I don't need to
retain the entire execution tree: just the stack of the current tree, along
with some backtracking information.

diff --git a/Makefile b/Makefile
index 093f42299aff26c7df3d7c6b7fc3ed5065715cd9..e61de2a159ae066d8be1471b0e259a0307a5177a 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -8,9 +8,9 @@ LIB_SO=lib$(LIB_NAME).so
 USER_O=userprog.o
 USER_H=libthreads.h libatomic.h
 
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc clockvector.cc main.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o clockvector.o main.o
-MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h clockvector.h
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o nodestack.o clockvector.o main.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h nodestack.h clockvector.h
 
 CPPFLAGS=-Wall -g
 LDFLAGS=-ldl

diff --git a/action.h b/action.h
index 9391591a5c7cf3bab5f2c3dbf407445b00fb478d..530436d87b8465a7cb33025da42097e684d93983 100644 (file)
--- a/action.h
+++ b/action.h
@@ -18,6 +18,7 @@ typedef enum action_type {
 
 /* Forward declaration */
 class TreeNode;
+class Node;
 
 class ModelAction {
 public:
@@ -32,6 +33,7 @@ public:
 
        TreeNode * get_treenode() { return treenode; }
        void set_node(TreeNode *n) { treenode = n; }
+       void set_node(Node *n) { node = n; }
 
        bool is_read();
        bool is_write();
@@ -47,6 +49,7 @@ private:
        thread_id_t tid;
        int value;
        TreeNode *treenode;
+       Node *node;
        int seq_number;
 };
 

diff --git a/nodestack.cc b/nodestack.cc
new file mode 100644 (file)
index 0000000..7cef4b6
--- /dev/null
+++ b/nodestack.cc
@@ -0,0 +1,173 @@
+#include "nodestack.h"
+#include "action.h"
+#include "common.h"
+
+int Node::total_nodes = 0;
+
+Node::Node(ModelAction *act, Node *parent)
+       : action(act),
+       num_threads(parent ? parent->num_threads : 1),
+       explored_children(num_threads),
+       backtrack(num_threads)
+{
+       total_nodes++;
+       if (act && act->get_type() == THREAD_CREATE) {
+               num_threads++;
+               explored_children.resize(num_threads);
+               backtrack.resize(num_threads);
+       }
+}
+
+Node::~Node()
+{
+       if (action)
+               delete action;
+}
+
+void Node::print()
+{
+       if (action)
+               action->print();
+       else
+               printf("******** empty action ********\n");
+}
+
+bool Node::has_been_explored(thread_id_t tid)
+{
+       int id = id_to_int(tid);
+       return explored_children[id];
+}
+
+bool Node::backtrack_empty()
+{
+       unsigned int i;
+       for (i = 0; i < backtrack.size(); i++)
+               if (backtrack[i] == true)
+                       return false;
+       return true;
+}
+
+void Node::explore_child(ModelAction *act)
+{
+       act->set_node(this);
+       explore(act->get_tid());
+}
+
+bool Node::set_backtrack(thread_id_t id)
+{
+       int i = id_to_int(id);
+       if (backtrack[i])
+               return false;
+       backtrack[i] = true;
+       return true;
+}
+
+thread_id_t Node::get_next_backtrack()
+{
+       /* TODO: find next backtrack */
+       unsigned int i;
+       for (i = 0; i < backtrack.size(); i++)
+               if (backtrack[i] == true)
+                       break;
+       if (i >= backtrack.size())
+               return THREAD_ID_T_NONE;
+       backtrack[i] = false;
+       return int_to_id(i);
+}
+
+bool Node::is_enabled(Thread *t)
+{
+       return id_to_int(t->get_id()) < num_threads;
+}
+
+void Node::explore(thread_id_t tid)
+{
+       int i = id_to_int(tid);
+       backtrack[i] = false;
+       explored_children[i] = true;
+}
+
+static void clear_node_list(node_list_t *list, node_list_t::iterator start,
+                                              node_list_t::iterator end)
+{
+       node_list_t::iterator it;
+
+       for (it = start; it != end; it++)
+               delete (*it);
+       list->erase(start, end);
+}
+
+NodeStack::NodeStack()
+{
+       node_list.push_back(new Node());
+       iter = node_list.begin();
+}
+
+NodeStack::~NodeStack()
+{
+       clear_node_list(&node_list, node_list.begin(), node_list.end());
+}
+
+void NodeStack::print()
+{
+       node_list_t::iterator it;
+       printf("............................................\n");
+       printf("NodeStack printing node_list:\n");
+       for (it = node_list.begin(); it != node_list.end(); it++) {
+               if (it == this->iter)
+                       printf("vvv following action is the current iterator vvv\n");
+               (*it)->print();
+       }
+       printf("............................................\n");
+}
+
+ModelAction * NodeStack::explore_action(ModelAction *act)
+{
+       DBG();
+       if (node_list.empty()) {
+               node_list.push_back(new Node(act));
+               iter = node_list.begin();
+       } else if (get_head()->has_been_explored(act->get_tid())) {
+               /* Discard duplicate ModelAction */
+               delete act;
+               iter++;
+       } else { /* Diverging from previous execution */
+               /* Clear out remainder of list */
+               node_list_t::iterator it = iter;
+               it++;
+               clear_node_list(&node_list, it, node_list.end());
+
+               /* Record action */
+               get_head()->explore_child(act);
+               node_list.push_back(new Node(act, get_head()));
+               iter++;
+       }
+       return (*iter)->get_action();
+}
+
+Node * NodeStack::get_head()
+{
+       if (node_list.empty())
+               return NULL;
+       return *iter;
+}
+
+Node * NodeStack::get_next()
+{
+       node_list_t::iterator it = iter;
+       if (node_list.empty()) {
+               DEBUG("Empty\n");
+               return NULL;
+       }
+       it++;
+       if (it == node_list.end()) {
+               DEBUG("At end\n");
+               return NULL;
+       }
+       return *it;
+}
+
+void NodeStack::reset_execution()
+{
+       iter = node_list.begin();
+}

diff --git a/nodestack.h b/nodestack.h
new file mode 100644 (file)
index 0000000..2fd84dd
--- /dev/null
+++ b/nodestack.h
@@ -0,0 +1,56 @@
+#ifndef __NODESTACK_H__
+#define __NODESTACK_H__
+
+#include <list>
+#include <vector>
+#include <cstddef>
+#include "threads.h"
+
+class ModelAction;
+
+class Node {
+public:
+       Node(ModelAction *act = NULL, Node *parent = NULL);
+       ~Node();
+       /* return true = thread choice has already been explored */
+       bool has_been_explored(thread_id_t tid);
+       /* return true = backtrack set is empty */
+       bool backtrack_empty();
+       void explore_child(ModelAction *act);
+       /* return false = thread was already in backtrack */
+       bool set_backtrack(thread_id_t id);
+       thread_id_t get_next_backtrack();
+       bool is_enabled(Thread *t);
+       ModelAction * get_action() { return action; }
+
+       void print();
+
+       static int get_total_nodes() { return total_nodes; }
+private:
+       void explore(thread_id_t tid);
+
+       static int total_nodes;
+       ModelAction *action;
+       int num_threads;
+       std::vector<bool> explored_children;
+       std::vector<bool> backtrack;
+};
+
+typedef std::list<class Node *> node_list_t;
+
+class NodeStack {
+public:
+       NodeStack();
+       ~NodeStack();
+       ModelAction * explore_action(ModelAction *act);
+       Node * get_head();
+       Node * get_next();
+       void reset_execution();
+
+       void print();
+private:
+       node_list_t node_list;
+       node_list_t::iterator iter;
+};
+
+#endif /* __NODESTACK_H__ */