2 * @brief Stack of operations for use in backtracking.
5 #ifndef __NODESTACK_H__
6 #define __NODESTACK_H__
17 * @brief A single node in a NodeStack
19 * Represents a single node in the NodeStack. Each Node is associated with up
20 * to one action and up to one parent node. A node holds information
21 * regarding the last action performed (the "associated action"), the thread
22 * choices that have been explored (explored_children) and should be explored
23 * (backtrack), and the actions that the last action may read from.
27 Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1);
29 /* return true = thread choice has already been explored */
30 bool has_been_explored(thread_id_t tid);
31 /* return true = backtrack set is empty */
32 bool backtrack_empty();
34 void explore_child(ModelAction *act);
35 /* return false = thread was already in backtrack */
36 bool set_backtrack(thread_id_t id);
37 thread_id_t get_next_backtrack();
38 bool is_enabled(Thread *t);
39 ModelAction * get_action() { return action; }
41 /** @return the parent Node to this Node; that is, the action that
42 * occurred previously in the stack. */
43 Node * get_parent() const { return parent; }
45 bool add_future_value(uint64_t value);
46 uint64_t get_future_value();
47 bool increment_future_value();
48 bool future_value_empty();
50 void add_read_from(const ModelAction *act);
51 const ModelAction * get_read_from();
52 bool increment_read_from();
53 bool read_from_empty();
55 void set_promise(uint32_t i);
56 bool get_promise(uint32_t i);
57 bool increment_promise();
61 void print_may_read_from();
65 void explore(thread_id_t tid);
70 std::vector< bool, MyAlloc<bool> > explored_children;
71 std::vector< bool, MyAlloc<bool> > backtrack;
74 /** The set of ModelActions that this the action at this Node may read
75 * from. Only meaningful if this Node represents a 'read' action. */
76 std::vector< const ModelAction *, MyAlloc< const ModelAction * > > may_read_from;
78 unsigned int read_from_index;
80 std::vector< uint64_t, MyAlloc< uint64_t > > future_values;
81 std::vector< uint32_t, MyAlloc< uint32_t > > promises;
82 unsigned int future_index;
85 typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
88 * @brief A stack of nodes
90 * Holds a Node linked-list that can be used for holding backtracking,
91 * may-read-from, and replay information. It is used primarily as a
92 * stack-like structure, in that backtracking points and replay nodes are
93 * only removed from the top (most recent).
99 ModelAction * explore_action(ModelAction *act);
102 void reset_execution();
103 void pop_restofstack(int numAhead);
104 int get_total_nodes() { return total_nodes; }
110 node_list_t node_list;
111 node_list_t::iterator iter;
116 #endif /* __NODESTACK_H__ */