more changes towards keeping track of promises resolved by a given write statement
[model-checker.git] / nodestack.cc
1 #include "nodestack.h"
2 #include "action.h"
3 #include "common.h"
4 #include "model.h"
5
6 /**
7  * @brief Node constructor
8  *
9  * Constructs a single Node for use in a NodeStack. Each Node is associated
10  * with exactly one ModelAction (exception: the first Node should be created
11  * as an empty stub, to represent the first thread "choice") and up to one
12  * parent.
13  *
14  * @param act The ModelAction to associate with this Node. May be NULL.
15  * @param par The parent Node in the NodeStack. May be NULL if there is no
16  * parent.
17  * @param nthreads The number of threads which exist at this point in the
18  * execution trace.
19  */
20 Node::Node(ModelAction *act, Node *par, int nthreads)
21         : action(act),
22         parent(par),
23         num_threads(nthreads),
24         explored_children(num_threads),
25         backtrack(num_threads),
26         numBacktracks(0),
27         may_read_from(),
28         read_from_index(0),
29         future_values(),
30         future_index(0)
31 {
32         if (act)
33                 act->set_node(this);
34 }
35
36 /** @brief Node desctructor */
37 Node::~Node()
38 {
39         if (action)
40                 delete action;
41 }
42
43 /** Prints debugging info for the ModelAction associated with this Node */
44 void Node::print()
45 {
46         if (action)
47                 action->print();
48         else
49                 printf("******** empty action ********\n");
50 }
51
52 /** @brief Prints info about may_read_from set */
53 void Node::print_may_read_from()
54 {
55         readfrom_set_t::iterator it;
56         for (it = may_read_from.begin(); it != may_read_from.end(); it++)
57                 (*it)->print();
58 }
59
60 void Node::set_promise(uint32_t i) {
61         if (i>=promises.size())
62                 promises.resize(i+1,0);
63         promises[i]=1;
64 }
65
66 bool Node::get_promise(uint32_t i) {
67         return (promises[i]==2);
68 }
69
70 bool Node::increment_promises() {
71         for (unsigned int i=0;i<promises.size();i++) {
72                 if (promises[i]==1) {
73                         promises[i]=2;
74                         do {
75                                 i--;
76                                 if (promises[i]==2)
77                                         promises[i]=1;
78                         } while(i>0);
79                         return true;
80                 }
81         }
82         return false;
83 }
84
85 bool Node::promises_empty() {
86         for (unsigned int i=0;i<promises.size();i++)
87                 if (promises[i]==1)
88                         return false;
89         return true;
90 }
91
92 /**
93  * Adds a value from a weakly ordered future write to backtrack to.
94  * @param value is the value to backtrack to.
95  */
96
97 bool Node::add_future_value(uint64_t value) {
98         for(unsigned int i=0;i<future_values.size();i++)
99                 if (future_values[i]==value)
100                         return false;
101         future_values.push_back(value);
102         return true;
103 }
104
105 /** 
106  * Checks whether the future_values set for this node is empty.
107  * @return true if the future_values set is empty.
108  */
109
110 bool Node::futurevalues_empty() {
111         return ((future_index+1)>=future_values.size());
112 }
113
114
115 /**
116  * Checks if the Thread associated with this thread ID has been explored from
117  * this Node already.
118  * @param tid is the thread ID to check
119  * @return true if this thread choice has been explored already, false
120  * otherwise
121  */
122 bool Node::has_been_explored(thread_id_t tid)
123 {
124         int id = id_to_int(tid);
125         return explored_children[id];
126 }
127
128 /**
129  * Checks if the backtracking set is empty.
130  * @return true if the backtracking set is empty
131  */
132 bool Node::backtrack_empty()
133 {
134         return (numBacktracks == 0);
135 }
136
137
138 /**
139  * Checks whether the readsfrom set for this node is empty.
140  * @return true if the readsfrom set is empty.
141  */
142 bool Node::readsfrom_empty() {
143         return ((read_from_index+1)>=may_read_from.size());
144 }
145
146
147
148 /**
149  * Mark the appropriate backtracking information for exploring a thread choice.
150  * @param act The ModelAction to explore
151  */
152 void Node::explore_child(ModelAction *act)
153 {
154         explore(act->get_tid());
155 }
156
157 /**
158  * Records a backtracking reference for a thread choice within this Node.
159  * Provides feedback as to whether this thread choice is already set for
160  * backtracking.
161  * @return false if the thread was already set to be backtracked, true
162  * otherwise
163  */
164 bool Node::set_backtrack(thread_id_t id)
165 {
166         int i = id_to_int(id);
167         if (backtrack[i])
168                 return false;
169         backtrack[i] = true;
170         numBacktracks++;
171         return true;
172 }
173
174 thread_id_t Node::get_next_backtrack()
175 {
176         /** @todo Find next backtrack */
177         unsigned int i;
178         for (i = 0; i < backtrack.size(); i++)
179                 if (backtrack[i] == true)
180                         break;
181         /* Backtrack set was empty? */
182         ASSERT(i != backtrack.size());
183
184         backtrack[i] = false;
185         numBacktracks--;
186         return int_to_id(i);
187 }
188
189 bool Node::is_enabled(Thread *t)
190 {
191         return id_to_int(t->get_id()) < num_threads;
192 }
193
194 /**
195  * Add an action to the may_read_from set.
196  * @param act is the action to add
197  */
198 void Node::add_read_from(const ModelAction *act)
199 {
200         may_read_from.push_back(act);
201 }
202
203 /**
204  * Gets the next 'future_value' value from this Node. Only valid for a node
205  * where this->action is a 'read'.
206  * @return The first element in future_values
207  */
208
209 uint64_t Node::get_future_value() {
210         ASSERT(future_index<future_values.size());
211         return future_values[future_index];
212 }
213
214 /**
215  * Gets the next 'may_read_from' action from this Node. Only valid for a node
216  * where this->action is a 'read'.
217  * @todo Perform reads_from backtracking/replay properly, so that this function
218  * may remove elements from may_read_from
219  * @return The first element in may_read_from
220  */
221 const ModelAction * Node::get_read_from() {
222         if (read_from_index<may_read_from.size())
223                 return may_read_from[read_from_index];
224         else
225                 return NULL;
226 }
227
228 /**
229  * Increments the index into the readsfrom set to explore the next item.
230  * @return Returns false if we have explored all items.
231  */
232 bool Node::increment_read_from() {
233         read_from_index++;
234         return (read_from_index<may_read_from.size());
235 }
236
237 /**
238  * Increments the index into the future_values set to explore the next item.
239  * @return Returns false if we have explored all values.
240  */
241
242 bool Node::increment_future_values() {
243         future_index++;
244         return (future_index<future_values.size());
245 }
246
247 void Node::explore(thread_id_t tid)
248 {
249         int i = id_to_int(tid);
250         if (backtrack[i]) {
251                 backtrack[i] = false;
252                 numBacktracks--;
253         }
254         explored_children[i] = true;
255 }
256
257 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
258                                                node_list_t::iterator end)
259 {
260         node_list_t::iterator it;
261
262         for (it = start; it != end; it++)
263                 delete (*it);
264         list->erase(start, end);
265 }
266
267 NodeStack::NodeStack()
268         : total_nodes(0)
269 {
270         node_list.push_back(new Node());
271         total_nodes++;
272         iter = node_list.begin();
273 }
274
275 NodeStack::~NodeStack()
276 {
277         clear_node_list(&node_list, node_list.begin(), node_list.end());
278 }
279
280 void NodeStack::print()
281 {
282         node_list_t::iterator it;
283         printf("............................................\n");
284         printf("NodeStack printing node_list:\n");
285         for (it = node_list.begin(); it != node_list.end(); it++) {
286                 if (it == this->iter)
287                         printf("vvv following action is the current iterator vvv\n");
288                 (*it)->print();
289         }
290         printf("............................................\n");
291 }
292
293 ModelAction * NodeStack::explore_action(ModelAction *act)
294 {
295         DBG();
296
297         ASSERT(!node_list.empty());
298         node_list_t::iterator it=iter;
299         it++;
300
301         if (it != node_list.end()) {
302                 iter++;
303                 return (*iter)->get_action();
304         }
305
306         /* Record action */
307         get_head()->explore_child(act);
308         node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
309         total_nodes++;
310         iter++;
311         return NULL;
312 }
313
314 /**
315  * Empties the stack of all trailing nodes after a given position and calls the
316  * destructor for each. This function is provided an offset which determines
317  * how many nodes (relative to the current replay state) to save before popping
318  * the stack.
319  * @param numAhead gives the number of Nodes (including this Node) to skip over
320  * before removing nodes.
321  */
322 void NodeStack::pop_restofstack(int numAhead)
323 {
324         /* Diverging from previous execution; clear out remainder of list */
325         node_list_t::iterator it = iter;
326         while (numAhead--)
327                 it++;
328         clear_node_list(&node_list, it, node_list.end());
329 }
330
331 Node * NodeStack::get_head()
332 {
333         if (node_list.empty())
334                 return NULL;
335         return *iter;
336 }
337
338 Node * NodeStack::get_next()
339 {
340         node_list_t::iterator it = iter;
341         if (node_list.empty()) {
342                 DEBUG("Empty\n");
343                 return NULL;
344         }
345         it++;
346         if (it == node_list.end()) {
347                 DEBUG("At end\n");
348                 return NULL;
349         }
350         return *it;
351 }
352
353 void NodeStack::reset_execution()
354 {
355         iter = node_list.begin();
356 }