X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b5843ed6b7c5ebf6ba091e05afac6ac70593e1ae;hb=414b2df02223c9109c53228f905cea524a346cbf;hp=1598fb9a276343ba3daf59f3beedad6d452115e7;hpb=eb3b6cccf71b9eeee035e2c98566dfa279e402ae;p=model-checker.git diff --git a/model.cc b/model.cc index 1598fb9..b5843ed 100644 --- a/model.cc +++ b/model.cc @@ -99,6 +99,12 @@ 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 +145,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()) { @@ -158,8 +167,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) 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(); @@ -181,23 +194,27 @@ bool ModelChecker::next_execution() DBG(); num_executions++; + if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); - earliest_diverge->print(); + if (earliest_diverge) + earliest_diverge->print(false); + else + printf("(Not set)\n"); earliest_diverge = NULL; num_feasible_executions++; } + DEBUG("Number of acquires waiting on pending release sequences: %lu\n", + pending_acq_rel_seq->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(); @@ -423,7 +440,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { - scheduler->add_thread(get_thread((*rit)->get_tid())); + scheduler->wake(get_thread(*rit)); } waiters->clear(); break; @@ -468,11 +485,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: { @@ -489,7 +506,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) scheduler->sleep(waiting); } else { do_complete_join(curr); - synchronized = true; + updated = true; /* trigger rel-seq checks */ } break; } @@ -500,9 +517,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr) Thread *wake = get_thread(act); scheduler->wake(wake); do_complete_join(act); - synchronized = true; + updated = true; /* trigger rel-seq checks */ } th->complete(); + updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { @@ -513,7 +531,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } - return synchronized; + return updated; } /** @@ -540,6 +558,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 */ @@ -612,7 +632,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) /* Make the execution look like we chose to run this action * much later, when a lock is actually available to release */ get_current_thread()->set_pending(curr); - remove_thread(get_current_thread()); + scheduler->sleep(get_current_thread()); return get_next_thread(NULL); } @@ -1314,6 +1334,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)); @@ -1465,6 +1487,7 @@ bool ModelChecker::resolve_promises(ModelAction *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); resolved = true; } else @@ -1667,12 +1690,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) +{ + 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) +{ + 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)