X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=11cbdfa801d772d70e210668db374fd71f718b71;hb=a124fdeef4ab9a7bcadf8d601742619ec06db5e3;hp=eebfa5ba1c0c8c4771bb625e490fb6dbfeb97c16;hpb=ee410adc01be424c3e5e28f273153afd66a49a83;p=model-checker.git diff --git a/nodestack.h b/nodestack.h index eebfa5b..11cbdfa 100644 --- a/nodestack.h +++ b/nodestack.h @@ -1,3 +1,7 @@ +/** @file nodestack.h + * @brief Stack of operations for use in backtracking. +*/ + #ifndef __NODESTACK_H__ #define __NODESTACK_H__ @@ -9,9 +13,20 @@ class ModelAction; +typedef std::list< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t; + +/** + * @brief A single node in a NodeStack + * + * Represents a single node in the NodeStack. Each Node is associated with up + * to one action and up to one parent node. A node holds information + * regarding the last action performed (the "associated action"), the thread + * choices that have been explored (explored_children) and should be explored + * (backtrack), and the actions that the last action may read from. + */ class Node { public: - Node(ModelAction *act = NULL, Node *parent = NULL); + Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1); ~Node(); /* return true = thread choice has already been explored */ bool has_been_explored(thread_id_t tid); @@ -24,23 +39,42 @@ public: bool is_enabled(Thread *t); ModelAction * get_action() { return action; } - void print(); + /** @return the parent Node to this Node; that is, the action that + * occurred previously in the stack. */ + Node * get_parent() const { return parent; } + + void add_read_from(const ModelAction *act); + const ModelAction * get_next_read_from(); - static int get_total_nodes() { return total_nodes; } + void print(); + void print_may_read_from(); MEMALLOC private: void explore(thread_id_t tid); - static int total_nodes; ModelAction *action; + Node *parent; int num_threads; std::vector< bool, MyAlloc > explored_children; std::vector< bool, MyAlloc > backtrack; + int numBacktracks; + + /** The set of ModelActions that this the action at this Node may read + * from. Only meaningful if this Node represents a 'read' action. */ + readfrom_set_t may_read_from; }; -typedef std::list > node_list_t; +typedef std::list< Node *, MyAlloc< Node * > > node_list_t; +/** + * @brief A stack of nodes + * + * Holds a Node linked-list that can be used for holding backtracking, + * may-read-from, and replay information. It is used primarily as a + * stack-like structure, in that backtracking points and replay nodes are + * only removed from the top (most recent). + */ class NodeStack { public: NodeStack(); @@ -50,12 +84,16 @@ public: Node * get_next(); void reset_execution(); + int get_total_nodes() { return total_nodes; } + void print(); MEMALLOC private: node_list_t node_list; node_list_t::iterator iter; + + int total_nodes; }; #endif /* __NODESTACK_H__ */