X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e46a18cb8e2f6132706e52a8f9312abd82e672be;hb=27a6b2d336785fa3d30d937a397242c0a6823cfc;hp=ce9e0660ff33021bc53bfaa0ada87cd60b12434f;hpb=620ae95ce4fed006d18a41b6ccfd949d7e77f677;p=model-checker.git diff --git a/model.cc b/model.cc index ce9e066..e46a18c 100644 --- a/model.cc +++ b/model.cc @@ -12,6 +12,7 @@ #include "promise.h" #include "datarace.h" #include "mutex.h" +#include "threads.h" #define INITIAL_THREAD_ID 0 @@ -33,7 +34,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - pending_acq_rel_seq(new std::vector()), + pending_rel_seqs(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -51,7 +52,7 @@ ModelChecker::ModelChecker(struct model_params params) : /** @brief Destructor */ ModelChecker::~ModelChecker() { - for (int i = 0; i < get_num_threads(); i++) + for (unsigned int i = 0; i < get_num_threads(); i++) delete thread_map->get(i); delete thread_map; @@ -64,7 +65,7 @@ ModelChecker::~ModelChecker() delete (*promises)[i]; delete promises; - delete pending_acq_rel_seq; + delete pending_rel_seqs; delete thrd_last_action; delete node_stack; @@ -94,11 +95,17 @@ thread_id_t ModelChecker::get_next_id() } /** @return the number of user threads created during this execution */ -int ModelChecker::get_num_threads() +unsigned int ModelChecker::get_num_threads() { return priv->next_thread_id; } +/** @return The currently executing Thread. */ +Thread * ModelChecker::get_current_thread() +{ + return scheduler->get_current_thread(); +} + /** @return a sequence number for a new ModelAction */ modelclock_t ModelChecker::get_next_seq_num() { @@ -139,6 +146,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) ModelAction *next = node_stack->get_next()->get_action(); if (next == diverge) { + if (earliest_diverge == NULL || *diverge < *earliest_diverge) + earliest_diverge=diverge; + Node *nextnode = next->get_node(); /* Reached divergence point */ if (nextnode->increment_promise()) { @@ -153,18 +163,26 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* The next node will try to read from a different future value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); + } else if (nextnode->increment_relseq_break()) { + /* The next node will try to resolve a release sequence differently */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); } else { /* Make a different thread execute for next step */ Node *node = nextnode->get_parent(); tid = node->get_next_backtrack(); node_stack->pop_restofstack(1); + if (diverge==earliest_diverge) { + earliest_diverge=node->get_action(); + } } DEBUG("*** Divergence point ***\n"); + diverge = NULL; } else { tid = next->get_tid(); } - DEBUG("*** ModelChecker chose next thread = %d ***\n", tid); + DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid)); ASSERT(tid != THREAD_ID_T_NONE); return thread_map->get(id_to_int(tid)); } @@ -181,10 +199,11 @@ bool ModelChecker::next_execution() DBG(); num_executions++; + if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) - earliest_diverge->print(false); + earliest_diverge->print(); else printf("(Not set)\n"); @@ -192,15 +211,15 @@ bool ModelChecker::next_execution() num_feasible_executions++; } + DEBUG("Number of acquires waiting on pending release sequences: %zu\n", + pending_rel_seqs->size()); + if (isfinalfeasible() || DBG_ENABLED()) print_summary(); if ((diverge = get_next_backtrack()) == NULL) return false; - if (earliest_diverge == NULL || *diverge < *earliest_diverge) - earliest_diverge=diverge; - if (DBG_ENABLED()) { printf("Next execution will diverge at:\n"); diverge->print(); @@ -221,7 +240,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (act->is_synchronizing(prev)) + if (prev->could_synchronize_with(act)) return prev; } break; @@ -309,7 +328,8 @@ void ModelChecker::set_backtracking(ModelAction *act) if (!node->set_backtrack(tid)) continue; DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", - prev->get_tid(), t->get_id()); + id_to_int(prev->get_tid()), + id_to_int(t->get_id())); if (DBG_ENABLED()) { prev->print(); act->print(); @@ -361,6 +381,8 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) curr->read_from(reads_from); mo_graph->commitChanges(); + mo_check_promises(curr->get_tid(), reads_from); + updated |= r_status; } else if (!second_part_of_rmw) { /* Read from future value */ @@ -458,6 +480,8 @@ bool ModelChecker::process_write(ModelAction *curr) } mo_graph->commitChanges(); + mo_check_promises(curr->get_tid(), curr); + get_thread(curr)->set_return_value(VALUE_NONE); return updated_mod_order || updated_promises; } @@ -471,11 +495,11 @@ bool ModelChecker::process_write(ModelAction *curr) * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.) * * @param curr The current action - * @return True if synchronization was updated + * @return True if synchronization was updated or a thread completed */ bool ModelChecker::process_thread_action(ModelAction *curr) { - bool synchronized = false; + bool updated = false; switch (curr->get_type()) { case THREAD_CREATE: { @@ -484,30 +508,40 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } case THREAD_JOIN: { - Thread *blocking = (Thread *)curr->get_location(); - ModelAction *act = get_last_action(blocking->get_id()); - curr->synchronize_with(act); - synchronized = true; + Thread *waiting, *blocking; + waiting = get_thread(curr); + blocking = (Thread *)curr->get_location(); + if (!blocking->is_complete()) { + blocking->push_wait_list(curr); + scheduler->sleep(waiting); + } else { + do_complete_join(curr); + updated = true; /* trigger rel-seq checks */ + } break; } case THREAD_FINISH: { Thread *th = get_thread(curr); while (!th->wait_list_empty()) { ModelAction *act = th->pop_wait_list(); - scheduler->wake(get_thread(act)); + Thread *wake = get_thread(act); + scheduler->wake(wake); + do_complete_join(act); + updated = true; /* trigger rel-seq checks */ } th->complete(); + updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { - check_promises(NULL, curr->get_cv()); + check_promises(curr->get_tid(), NULL, curr->get_cv()); break; } default: break; } - return synchronized; + return updated; } /** @@ -534,6 +568,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) return newcurr; } + curr->set_seq_number(get_next_seq_num()); + newcurr = node_stack->explore_action(curr, scheduler->get_enabled()); if (newcurr) { /* First restore type and order in case of RMW operation */ @@ -559,17 +595,16 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) */ if (newcurr->is_write()) compute_promises(newcurr); + else if (newcurr->is_relseq_fixup()) + compute_relseq_breakwrites(newcurr); } return newcurr; } /** - * @brief Check whether a model action is enabled. - * - * Checks whether a lock or join operation would be successful (i.e., is the - * lock already locked, or is the joined thread already complete). If not, put - * the action in a waiter list. - * + * This method checks whether a model action is enabled at the given point. + * At this point, it checks whether a lock operation would be successful at this point. + * If not, it puts the thread in a waiter list. * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. */ @@ -582,12 +617,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); return false; } - } else if (curr->get_type() == THREAD_JOIN) { - Thread *blocking = (Thread *)curr->get_location(); - if (!blocking->is_complete()) { - blocking->push_wait_list(curr); - return false; - } } return true; @@ -613,7 +642,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (!check_action_enabled(curr)) { /* Make the execution look like we chose to run this action - * much later, when a lock/join can succeed */ + * much later, when a lock is actually available to release */ get_current_thread()->set_pending(curr); scheduler->sleep(get_current_thread()); return get_next_thread(NULL); @@ -717,7 +746,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { if ((!parnode->backtrack_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || - !currnode->promise_empty()) + !currnode->promise_empty() || + !currnode->relseq_break_empty()) && (!priv->next_backtrack || *curr > *priv->next_backtrack)) { priv->next_backtrack = curr; @@ -737,7 +767,7 @@ bool ModelChecker::promises_expired() { /** @return whether the current partial trace must be a prefix of a * feasible trace. */ bool ModelChecker::isfeasibleprefix() { - return promises->size() == 0 && pending_acq_rel_seq->size() == 0; + return promises->size() == 0 && pending_rel_seqs->size() == 0; } /** @return whether the current partial trace is feasible. */ @@ -776,8 +806,7 @@ bool ModelChecker::isfinalfeasible() { /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ ModelAction * ModelChecker::process_rmw(ModelAction *act) { - int tid = id_to_int(act->get_tid()); - ModelAction *lastread = get_last_action(tid); + ModelAction *lastread = get_last_action(act->get_tid()); lastread->process_rmw(act); if (act->is_rmw() && lastread->get_reads_from()!=NULL) { mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); @@ -923,7 +952,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf } } else { const ModelAction *prevreadfrom = act->get_reads_from(); - if (prevreadfrom != NULL && rf != prevreadfrom) { + //if the previous read is unresolved, keep going... + if (prevreadfrom == NULL) + continue; + + if (rf != prevreadfrom) { mo_graph->addEdge(prevreadfrom, rf); added = true; } @@ -1048,14 +1081,22 @@ bool ModelChecker::w_modification_order(ModelAction *curr) ModelAction *act = *rit; if (act == curr) { /* - * If RMW, we already have all relevant edges, - * so just skip to next thread. - * If normal write, we need to look at earlier - * actions, so continue processing list. + * 1) If RMW and it actually read from something, then we + * already have all relevant edges, so just skip to next + * thread. + * + * 2) If RMW and it didn't read from anything, we should + * whatever edge we can get to speed up convergence. + * + * 3) If normal write, we need to look at earlier actions, so + * continue processing list. */ - if (curr->is_rmw()) - break; - else + if (curr->is_rmw()) { + if (curr->get_reads_from()!=NULL) + break; + else + continue; + } else continue; } @@ -1072,11 +1113,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (act->is_write()) mo_graph->addEdge(act, curr); - else if (act->is_read() && act->get_reads_from() != NULL) + else if (act->is_read()) { + //if previous read accessed a null, just keep going + if (act->get_reads_from() == NULL) + continue; mo_graph->addEdge(act->get_reads_from(), curr); + } added = true; break; - } else if (act->is_read() && !act->is_synchronizing(curr) && + } else if (act->is_read() && !act->could_synchronize_with(curr) && !act->same_thread(curr)) { /* We have an action that: (1) did not happen before us @@ -1136,13 +1181,19 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @todo Finish lazy updating, when promises are fulfilled in the future * @param rf The action that might be part of a release sequence. Must be a * write. - * @param release_heads A pass-by-reference style return parameter. After + * @param release_heads A pass-by-reference style return parameter. After * execution of this function, release_heads will contain the heads of all the - * relevant release sequences, if any exists + * relevant release sequences, if any exists with certainty + * @param pending A pass-by-reference style return parameter which is only used + * when returning false (i.e., uncertain). Returns most information regarding + * an uncertain release sequence, including any write operations that might + * break the sequence. * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const +bool ModelChecker::release_seq_heads(const ModelAction *rf, + rel_heads_list_t *release_heads, + struct release_seq *pending) const { /* Only check for release sequences if there are no cycles */ if (mo_graph->checkForCycles()) @@ -1171,6 +1222,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel }; if (!rf) { /* read from future: need to settle this later */ + pending->rf = NULL; return false; /* incomplete */ } @@ -1200,6 +1252,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel ASSERT(rf->same_thread(release)); + pending->writes.clear(); + bool certain = true; for (unsigned int i = 0; i < thrd_lists->size(); i++) { if (id_to_int(rf->get_tid()) == (int)i) @@ -1211,8 +1265,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel bool future_ordered = false; ModelAction *last = get_last_action(int_to_id(i)); - if (last && (rf->happens_before(last) || - last->get_type() == THREAD_FINISH)) + Thread *th = get_thread(int_to_id(i)); + if ((last && rf->happens_before(last)) || + !scheduler->is_enabled(th) || + th->is_complete()) future_ordered = true; for (rit = list->rbegin(); rit != list->rend(); rit++) { @@ -1243,14 +1299,21 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel /* release --mo-> act --mo--> rf */ return true; /* complete */ } + /* act may break release sequence */ + pending->writes.push_back(act); certain = false; } if (!future_ordered) - return false; /* This thread is uncertain */ + certain = false; /* This thread is uncertain */ } - if (certain) + if (certain) { release_heads->push_back(release); + pending->writes.clear(); + } else { + pending->release = release; + pending->rf = rf; + } return certain; } @@ -1264,16 +1327,19 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * @param act The 'acquire' action that may read from a release sequence * @param release_heads A pass-by-reference return parameter. Will be filled * with the head(s) of the release sequence(s), if they exists with certainty. - * @see ModelChecker::release_seq_head + * @see ModelChecker::release_seq_heads */ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); - bool complete; - complete = release_seq_head(rf, release_heads); - if (!complete) { + struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq)); + sequence->acquire = act; + + if (!release_seq_heads(rf, release_heads, sequence)) { /* add act to 'lazy checking' list */ - pending_acq_rel_seq->push_back(act); + pending_rel_seqs->push_back(sequence); + } else { + snapshot_free(sequence); } } @@ -1293,9 +1359,10 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { bool updated = false; - std::vector::iterator it = pending_acq_rel_seq->begin(); - while (it != pending_acq_rel_seq->end()) { - ModelAction *act = *it; + std::vector::iterator it = pending_rel_seqs->begin(); + while (it != pending_rel_seqs->end()) { + struct release_seq *pending = *it; + ModelAction *act = pending->acquire; /* Only resolve sequences on the given location, if provided */ if (location && act->get_location() != location) { @@ -1306,7 +1373,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; - complete = release_seq_head(rf, &release_heads); + complete = release_seq_heads(rf, &release_heads, pending); for (unsigned int i = 0; i < release_heads.size(); i++) { if (!act->has_synchronized_with(release_heads[i])) { if (act->synchronize_with(release_heads[i])) @@ -1317,6 +1384,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } if (updated) { + /* Re-check all pending release sequences */ + work_queue->push_back(CheckRelSeqWorkEntry(NULL)); /* Re-check act for mo_graph edges */ work_queue->push_back(MOEdgeWorkEntry(act)); @@ -1331,10 +1400,12 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } } } - if (complete) - it = pending_acq_rel_seq->erase(it); - else + if (complete) { + it = pending_rel_seqs->erase(it); + snapshot_free(pending); + } else { it++; + } } // If we resolved promises or data races, see if we have realized a data race. @@ -1450,6 +1521,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; + std::vector threads_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; @@ -1467,12 +1539,22 @@ bool ModelChecker::resolve_promises(ModelAction *write) post_r_modification_order(read, write); //Make sure the promise's value matches the write's value ASSERT(promise->get_value() == write->get_value()); - + delete(promise); + promises->erase(promises->begin() + promise_index); + threads_to_check.push_back(read->get_tid()); + resolved = true; } else promise_index++; } + + //Check whether reading these writes has made threads unable to + //resolve promises + + for(unsigned int i=0;iget_action(); if (!act->happens_before(curr) && act->is_read() && - !act->is_synchronizing(curr) && + !act->could_synchronize_with(curr) && !act->same_thread(curr) && promise->get_value() == curr->get_value()) { curr->get_node()->set_promise(i); @@ -1498,16 +1580,14 @@ void ModelChecker::compute_promises(ModelAction *curr) } /** Checks promises in response to change in ClockVector Threads. */ -void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) +void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv) { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; const ModelAction *act = promise->get_action(); if ((old_cv == NULL || !old_cv->synchronized_since(act)) && merge_cv->synchronized_since(act)) { - //This thread is no longer able to send values back to satisfy the promise - int num_synchronized_threads = promise->increment_threads(); - if (num_synchronized_threads == get_num_threads()) { + if (promise->increment_threads(tid)) { //Promise has failed failed_promise = true; return; @@ -1516,6 +1596,92 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) } } +/** Checks promises in response to addition to modification order for threads. + * Definitions: + * pthread is the thread that performed the read that created the promise + * + * pread is the read that created the promise + * + * pwrite is either the first write to same location as pread by + * pthread that is sequenced after pread or the value read by the + * first read to the same lcoation as pread by pthread that is + * sequenced after pread.. + * + * 1. If tid=pthread, then we check what other threads are reachable + * through the mode order starting with pwrite. Those threads cannot + * perform a write that will resolve the promise due to modification + * order constraints. + * + * 2. If the tid is not pthread, we check whether pwrite can reach the + * action write through the modification order. If so, that thread + * cannot perform a future write that will resolve the promise due to + * modificatin order constraints. + * + * @parem tid The thread that either read from the model action + * write, or actually did the model action write. + * + * @parem write The ModelAction representing the relevant write. + */ + +void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) { + void * location = write->get_location(); + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + const ModelAction *act = promise->get_action(); + + //Is this promise on the same location? + if ( act->get_location() != location ) + continue; + + //same thread as the promise + if ( act->get_tid()==tid ) { + + //do we have a pwrite for the promise, if not, set it + if (promise->get_write() == NULL ) { + promise->set_write(write); + } + if (mo_graph->checkPromise(write, promise)) { + failed_promise = true; + return; + } + } + + //Don't do any lookups twice for the same thread + if (promise->has_sync_thread(tid)) + continue; + + if (mo_graph->checkReachable(promise->get_write(), write)) { + if (promise->increment_threads(tid)) { + failed_promise = true; + return; + } + } + } +} + +/** + * Compute the set of writes that may break the current pending release + * sequence. This information is extracted from previou release sequence + * calculations. + * + * @param curr The current ModelAction. Must be a release sequence fixup + * action. + */ +void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) +{ + if (pending_rel_seqs->empty()) + return; + + struct release_seq *pending = pending_rel_seqs->back(); + for (unsigned int i = 0; i < pending->writes.size(); i++) { + const ModelAction *write = pending->writes[i]; + curr->get_node()->add_relseq_break(write); + } + + /* NULL means don't break the sequence; just synchronize */ + curr->get_node()->add_relseq_break(NULL); +} + /** * Build up an initial set of all past writes that this 'read' action may read * from. This set is determined by the clock vector's "happens before" @@ -1614,7 +1780,8 @@ void ModelChecker::dumpGraph(char *filename) { ModelAction *action=*it; if (action->is_read()) { fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid()); - fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number()); + if (action->get_reads_from()!=NULL) + fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number()); } if (thread_array[action->get_tid()] != NULL) { fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number()); @@ -1670,12 +1837,35 @@ void ModelChecker::remove_thread(Thread *t) scheduler->remove_thread(t); } +/** + * @brief Get a Thread reference by its ID + * @param tid The Thread's ID + * @return A Thread reference + */ +Thread * ModelChecker::get_thread(thread_id_t tid) const +{ + return thread_map->get(id_to_int(tid)); +} + +/** + * @brief Get a reference to the Thread in which a ModelAction was executed + * @param act The ModelAction + * @return A Thread reference + */ +Thread * ModelChecker::get_thread(ModelAction *act) const +{ + return get_thread(act->get_tid()); +} + /** * Switch from a user-context to the "master thread" context (a.k.a. system * context). This switch is made with the intention of exploring a particular * model-checking action (described by a ModelAction object). Must be called * from a user-thread context. - * @param act The current action that will be explored. Must not be NULL. + * + * @param act The current action that will be explored. May be NULL only if + * trace is exiting via an assertion (see ModelChecker::set_assert and + * ModelChecker::has_asserted). * @return Return status from the 'swap' call (i.e., success/fail, 0/-1) */ int ModelChecker::switch_to_master(ModelAction *act) @@ -1695,7 +1885,7 @@ bool ModelChecker::take_step() { if (has_asserted()) return false; - Thread * curr = thread_current(); + Thread *curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); @@ -1709,22 +1899,23 @@ bool ModelChecker::take_step() { ASSERT(false); } } - Thread * next = scheduler->next_thread(priv->nextThread); + Thread *next = scheduler->next_thread(priv->nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) return false; - if (next) - next->set_state(THREAD_RUNNING); - DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); + DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, + next ? id_to_int(next->get_id()) : -1); /* next == NULL -> don't take any more steps */ if (!next) return false; - if ( next->get_pending() != NULL ) { - //restart a pending action + next->set_state(THREAD_RUNNING); + + if (next->get_pending() != NULL) { + /* restart a pending action */ set_current_action(next->get_pending()); next->set_pending(NULL); next->set_state(THREAD_READY);