2 * @brief Stack of operations for use in backtracking.
5 #ifndef __NODESTACK_H__
6 #define __NODESTACK_H__
13 #include "clockvector.h"
18 * A flag used for the promise counting/combination problem within a node,
19 * denoting whether a particular Promise is
20 * <ol><li>@b applicable: can be satisfied by this Node's ModelAction and</li>
21 * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
22 * configuration.</li></ol>
25 PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */
26 PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */
27 PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
32 modelclock_t expiration;
35 struct fairness_info {
36 unsigned int enabled_count;
43 * @brief A single node in a NodeStack
45 * Represents a single node in the NodeStack. Each Node is associated with up
46 * to one action and up to one parent node. A node holds information
47 * regarding the last action performed (the "associated action"), the thread
48 * choices that have been explored (explored_children) and should be explored
49 * (backtrack), and the actions that the last action may read from.
53 Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL);
55 /* return true = thread choice has already been explored */
56 bool has_been_explored(thread_id_t tid);
57 /* return true = backtrack set is empty */
58 bool backtrack_empty();
60 void explore_child(ModelAction *act, bool * is_enabled);
61 /* return false = thread was already in backtrack */
62 bool set_backtrack(thread_id_t id);
63 thread_id_t get_next_backtrack();
64 bool is_enabled(Thread *t);
65 bool is_enabled(thread_id_t tid);
66 ModelAction * get_action() { return action; }
67 bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;}
68 int get_num_threads() {return num_threads;}
69 /** @return the parent Node to this Node; that is, the action that
70 * occurred previously in the stack. */
71 Node * get_parent() const { return parent; }
73 bool add_future_value(uint64_t value, modelclock_t expiration);
74 uint64_t get_future_value();
75 modelclock_t get_future_value_expiration();
76 bool increment_future_value();
77 bool future_value_empty();
79 void add_read_from(const ModelAction *act);
80 const ModelAction * get_read_from();
81 bool increment_read_from();
82 bool read_from_empty();
83 int get_read_from_size();
84 const ModelAction * get_read_from_at(int i);
86 void set_promise(unsigned int i);
87 bool get_promise(unsigned int i);
88 bool increment_promise();
92 void print_may_read_from();
96 void explore(thread_id_t tid);
101 std::vector< bool, MyAlloc<bool> > explored_children;
102 std::vector< bool, MyAlloc<bool> > backtrack;
103 std::vector< struct fairness_info, MyAlloc< struct fairness_info> > fairness;
107 /** The set of ModelActions that this the action at this Node may read
108 * from. Only meaningful if this Node represents a 'read' action. */
109 std::vector< const ModelAction *, MyAlloc< const ModelAction * > > may_read_from;
111 unsigned int read_from_index;
113 std::vector< struct future_value, MyAlloc<struct future_value> > future_values;
114 std::vector< promise_t, MyAlloc<promise_t> > promises;
118 typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;
121 * @brief A stack of nodes
123 * Holds a Node linked-list that can be used for holding backtracking,
124 * may-read-from, and replay information. It is used primarily as a
125 * stack-like structure, in that backtracking points and replay nodes are
126 * only removed from the top (most recent).
132 ModelAction * explore_action(ModelAction *act, bool * is_enabled);
135 void reset_execution();
136 void pop_restofstack(int numAhead);
137 int get_total_nodes() { return total_nodes; }
143 node_list_t node_list;
149 #endif /* __NODESTACK_H__ */