From f52c40fdba5d4648020927cfb942518ed02362df Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 14 May 2012 11:05:02 -0700 Subject: [PATCH] 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. --- Makefile | 6 +- action.h | 3 + nodestack.cc | 173 +++++++++++++++++++++++++++++++++++++++++++++++++++ nodestack.h | 56 +++++++++++++++++ 4 files changed, 235 insertions(+), 3 deletions(-) create mode 100644 nodestack.cc create mode 100644 nodestack.h diff --git a/Makefile b/Makefile index 093f422..e61de2a 100644 --- 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 9391591..530436d 100644 --- 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 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 index 0000000..2fd84dd --- /dev/null +++ b/nodestack.h @@ -0,0 +1,56 @@ +#ifndef __NODESTACK_H__ +#define __NODESTACK_H__ + +#include +#include +#include +#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 explored_children; + std::vector backtrack; +}; + +typedef std::list 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__ */ -- 2.34.1