1 #define __STDC_FORMAT_MACROS
10 #include "threads-model.h"
11 #include "modeltypes.h"
12 #include "execution.h"
16 * @brief Node constructor
18 * Constructs a single Node for use in a NodeStack. Each Node is associated
19 * with exactly one ModelAction (exception: the first Node should be created
20 * as an empty stub, to represent the first thread "choice") and up to one
23 * @param params The model-checker parameters
24 * @param act The ModelAction to associate with this Node. May be NULL.
25 * @param par The parent Node in the NodeStack. May be NULL if there is no
27 * @param nthreads The number of threads which exist at this point in the
30 Node::Node(const struct model_params *params, ModelAction *act, Node *par,
31 int nthreads, Node *prevfairness) :
32 read_from_status(READ_FROM_PAST),
37 num_threads(nthreads),
38 explored_children(num_threads),
39 backtrack(num_threads),
40 fairness(num_threads),
44 read_from_past_idx(0),
45 relseq_break_writes(),
46 relseq_break_index(0),
53 int currtid = id_to_int(act->get_tid());
54 int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0;
56 if (get_params()->fairwindow != 0) {
57 for (int i = 0; i < num_threads; i++) {
58 ASSERT(i < ((int)fairness.size()));
59 struct fairness_info *fi = &fairness[i];
60 struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL;
64 if (parent && parent->is_enabled(int_to_id(i))) {
71 /* Do window processing */
72 if (prevfairness != NULL) {
73 if (prevfairness->parent->is_enabled(int_to_id(i)))
78 /* Need full window to start evaluating
80 * If we meet the enabled count and have no
81 * turns, give us priority */
82 if ((fi->enabled_count >= get_params()->enabledcount) &&
90 int Node::get_yield_data(int tid1, int tid2) const {
91 if (tid1<num_threads && tid2 < num_threads)
92 return yield_data[YIELD_INDEX(tid1,tid2,num_threads)];
94 return YIELD_S | YIELD_D;
97 void Node::update_yield(Scheduler * scheduler) {
99 yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
101 if (parent == NULL) {
102 for(int i = 0; i < num_threads*num_threads; i++) {
103 yield_data[i] = YIELD_S | YIELD_D;
107 int curr_tid=id_to_int(action->get_tid());
109 for(int u = 0; u < num_threads; u++) {
110 for(int v = 0; v < num_threads; v++) {
111 int yield_state=parent->get_yield_data(u, v);
112 bool next_enabled=scheduler->is_enabled(int_to_id(v));
113 bool curr_enabled=parent->is_enabled(int_to_id(v));
115 //Compute intersection of ES and E
116 yield_state&=~YIELD_E;
117 //Check to see if we disabled the thread
118 if (u==curr_tid && curr_enabled)
119 yield_state|=YIELD_D;
121 yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state;
123 yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S;
125 //handle curr.yield(t) part of computation
126 if (action->is_yield()) {
127 for(int v = 0; v < num_threads; v++) {
128 int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)];
129 if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S)))
130 yield_state |= YIELD_P;
131 yield_state &= YIELD_P;
132 if (scheduler->is_enabled(int_to_id(v))) {
133 yield_state|=YIELD_E;
135 yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state;
140 /** @brief Node desctructor */
145 delete uninit_action;
147 model_free(enabled_array);
149 model_free(yield_data);
152 /** Prints debugging info for the ModelAction associated with this Node */
153 void Node::print() const
156 model_print(" thread status: ");
158 for (int i = 0; i < num_threads; i++) {
160 enabled_type_to_string(enabled_array[i], str);
161 model_print("[%d: %s]", i, str);
165 model_print("(info not available)\n");
166 model_print(" backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
167 for (int i = 0; i < (int)backtrack.size(); i++)
168 if (backtrack[i] == true)
169 model_print("[%d]", i);
172 model_print(" read from past: %s", read_from_past_empty() ? "empty" : "non-empty ");
173 for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
174 model_print("[%d]", read_from_past[i]->get_seq_number());
177 model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty");
178 model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
181 /****************************** threads backtracking **************************/
184 * Checks if the Thread associated with this thread ID has been explored from
186 * @param tid is the thread ID to check
187 * @return true if this thread choice has been explored already, false
190 bool Node::has_been_explored(thread_id_t tid) const
192 int id = id_to_int(tid);
193 return explored_children[id];
197 * Checks if the backtracking set is empty.
198 * @return true if the backtracking set is empty
200 bool Node::backtrack_empty() const
202 return (numBacktracks == 0);
205 void Node::explore(thread_id_t tid)
207 int i = id_to_int(tid);
208 ASSERT(i < ((int)backtrack.size()));
210 backtrack[i] = false;
213 explored_children[i] = true;
217 * Mark the appropriate backtracking information for exploring a thread choice.
218 * @param act The ModelAction to explore
220 void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled)
223 enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads);
224 if (is_enabled != NULL)
225 memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads);
227 for (int i = 0; i < num_threads; i++)
228 enabled_array[i] = THREAD_DISABLED;
231 explore(act->get_tid());
235 * Records a backtracking reference for a thread choice within this Node.
236 * Provides feedback as to whether this thread choice is already set for
238 * @return false if the thread was already set to be backtracked, true
241 bool Node::set_backtrack(thread_id_t id)
243 int i = id_to_int(id);
244 ASSERT(i < ((int)backtrack.size()));
252 thread_id_t Node::get_next_backtrack()
254 /** @todo Find next backtrack */
256 for (i = 0; i < backtrack.size(); i++)
257 if (backtrack[i] == true)
259 /* Backtrack set was empty? */
260 ASSERT(i != backtrack.size());
262 backtrack[i] = false;
267 void Node::clear_backtracking()
269 for (unsigned int i = 0; i < backtrack.size(); i++)
270 backtrack[i] = false;
271 for (unsigned int i = 0; i < explored_children.size(); i++)
272 explored_children[i] = false;
276 /************************** end threads backtracking **************************/
278 void Node::set_misc_max(int i)
283 int Node::get_misc() const
288 bool Node::increment_misc()
290 return (misc_index < misc_max) && ((++misc_index) < misc_max);
293 bool Node::misc_empty() const
295 return (misc_index + 1) >= misc_max;
298 bool Node::is_enabled(Thread *t) const
300 int thread_id = id_to_int(t->get_id());
301 return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
304 enabled_type_t Node::enabled_status(thread_id_t tid) const
306 int thread_id = id_to_int(tid);
307 if (thread_id < num_threads)
308 return enabled_array[thread_id];
310 return THREAD_DISABLED;
313 bool Node::is_enabled(thread_id_t tid) const
315 int thread_id = id_to_int(tid);
316 return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
319 bool Node::has_priority(thread_id_t tid) const
321 return fairness[id_to_int(tid)].priority;
324 bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
326 return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P;
329 /*********************************** read from ********************************/
332 * Get the current state of the may-read-from set iteration
333 * @return The read-from type we should currently be checking (past)
335 read_from_type_t Node::get_read_from_status()
337 if (read_from_status == READ_FROM_PAST && read_from_past.empty())
338 increment_read_from();
339 return read_from_status;
343 * Iterate one step in the may-read-from iteration. This includes a step in
344 * reading from the either the past or the future.
345 * @return True if there is a new read-from to explore; false otherwise
347 bool Node::increment_read_from()
349 if (increment_read_from_past()) {
350 read_from_status = READ_FROM_PAST;
353 read_from_status = READ_FROM_NONE;
358 * @return True if there are any new read-froms to explore
360 bool Node::read_from_empty() const
362 return read_from_past_empty();
366 * Get the total size of the may-read-from set, including both past
367 * @return The size of may-read-from
369 unsigned int Node::read_from_size() const
371 return read_from_past.size();
374 /******************************* end read from ********************************/
376 /****************************** read from past ********************************/
378 /** @brief Prints info about read_from_past set */
379 void Node::print_read_from_past()
381 for (unsigned int i = 0; i < read_from_past.size(); i++)
382 read_from_past[i]->print();
386 * Add an action to the read_from_past set.
387 * @param act is the action to add
389 void Node::add_read_from_past(const ModelAction *act)
391 read_from_past.push_back(act);
395 * Gets the next 'read_from_past' action from this Node. Only valid for a node
396 * where this->action is a 'read'.
397 * @return The first element in read_from_past
399 const ModelAction * Node::get_read_from_past() const
401 if (read_from_past_idx < read_from_past.size()) {
402 int random_index = rand() % read_from_past.size();
403 return read_from_past[random_index];
405 // return read_from_past[read_from_past_idx];
410 const ModelAction * Node::get_read_from_past(int i) const
412 return read_from_past[i];
415 int Node::get_read_from_past_size() const
417 return read_from_past.size();
421 * Checks whether the readsfrom set for this node is empty.
422 * @return true if the readsfrom set is empty.
424 bool Node::read_from_past_empty() const
426 return ((read_from_past_idx + 1) >= read_from_past.size());
430 * Increments the index into the readsfrom set to explore the next item.
431 * @return Returns false if we have explored all items.
433 bool Node::increment_read_from_past()
436 if (read_from_past_idx < read_from_past.size()) {
437 read_from_past_idx++;
438 return read_from_past_idx < read_from_past.size();
443 /************************** end read from past ********************************/
445 /*********************** breaking release sequences ***************************/
448 * Add a write ModelAction to the set of writes that may break the release
449 * sequence. This is used during replay exploration of pending release
450 * sequences. This Node must correspond to a release sequence fixup action.
452 * @param write The write that may break the release sequence. NULL means we
453 * allow the release sequence to synchronize.
455 void Node::add_relseq_break(const ModelAction *write)
457 relseq_break_writes.push_back(write);
461 * Get the write that may break the current pending release sequence,
462 * according to the replay / divergence pattern.
464 * @return A write that may break the release sequence. If NULL, that means
465 * the release sequence should not be broken.
467 const ModelAction * Node::get_relseq_break() const
469 if (relseq_break_index < (int)relseq_break_writes.size())
470 return relseq_break_writes[relseq_break_index];
476 * Increments the index into the relseq_break_writes set to explore the next
478 * @return Returns false if we have explored all values.
480 bool Node::increment_relseq_break()
483 if (relseq_break_index < ((int)relseq_break_writes.size())) {
484 relseq_break_index++;
485 return (relseq_break_index < ((int)relseq_break_writes.size()));
491 * @return True if all writes that may break the release sequence have been
494 bool Node::relseq_break_empty() const
496 return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
499 /******************* end breaking release sequences ***************************/
502 * Increments some behavior's index, if a new behavior is available
503 * @return True if there is a new behavior available; otherwise false
505 bool Node::increment_behaviors()
507 /* satisfy a different misc_index values */
508 if (increment_misc())
510 /* read from a different value */
511 if (increment_read_from())
513 /* resolve a release sequence differently */
514 if (increment_relseq_break())
519 NodeStack::NodeStack() :
527 NodeStack::~NodeStack()
529 for (unsigned int i = 0; i < node_list.size(); i++)
534 * @brief Register the model-checker object with this NodeStack
535 * @param exec The execution structure for the ModelChecker
537 void NodeStack::register_engine(const ModelExecution *exec)
539 this->execution = exec;
542 const struct model_params * NodeStack::get_params() const
544 return execution->get_params();
547 void NodeStack::print() const
549 model_print("............................................\n");
550 model_print("NodeStack printing node_list:\n");
551 for (unsigned int it = 0; it < node_list.size(); it++) {
552 if ((int)it == this->head_idx)
553 model_print("vvv following action is the current iterator vvv\n");
554 node_list[it]->print();
556 model_print("............................................\n");
559 /** Note: The is_enabled set contains what actions were enabled when
561 ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
565 if ((head_idx + 1) < (int)node_list.size()) {
567 return node_list[head_idx]->get_action();
571 Node *head = get_head();
572 Node *prevfairness = NULL;
574 head->explore_child(act, is_enabled);
575 if (get_params()->fairwindow != 0 && head_idx > (int)get_params()->fairwindow)
576 prevfairness = node_list[head_idx - get_params()->fairwindow];
579 int next_threads = execution->get_num_threads();
580 if (act->get_type() == THREAD_CREATE || act->get_type() == PTHREAD_CREATE ) // may need to be changed
582 node_list.push_back(new Node(get_params(), act, head, next_threads, prevfairness));
589 * Empties the stack of all trailing nodes after a given position and calls the
590 * destructor for each. This function is provided an offset which determines
591 * how many nodes (relative to the current replay state) to save before popping
593 * @param numAhead gives the number of Nodes (including this Node) to skip over
594 * before removing nodes.
596 void NodeStack::pop_restofstack(int numAhead)
598 /* Diverging from previous execution; clear out remainder of list */
599 unsigned int it = head_idx + numAhead;
600 for (unsigned int i = it; i < node_list.size(); i++)
602 node_list.resize(it);
603 node_list.back()->clear_backtracking();
606 /** Reset the node stack. */
607 void NodeStack::full_reset()
609 for (unsigned int i = 0; i < node_list.size(); i++)
616 Node * NodeStack::get_head() const
618 if (node_list.empty() || head_idx < 0)
620 return node_list[head_idx];
623 Node * NodeStack::get_next() const
625 if (node_list.empty()) {
629 unsigned int it = head_idx + 1;
630 if (it == node_list.size()) {
634 return node_list[it];
637 void NodeStack::reset_execution()