X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=8b7201f1b88c4edf98475e0ebeadc7ecd6fd6f32;hp=a7c99af24b7b05633183e9f96494e873e9e3a5b3;hb=bbc3405aa23e6eafb3863738c4e203764694e9a4;hpb=8521b24fa3f8bc2c903c9b82350c61828bf67520 diff --git a/model.cc b/model.cc index a7c99af..8b7201f 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 @@ -20,11 +21,12 @@ ModelChecker *model; /** @brief Constructor */ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ + params(params), scheduler(new Scheduler()), num_executions(0), num_feasible_executions(0), - params(params), diverge(NULL), + earliest_diverge(NULL), action_trace(new action_list_t()), thread_map(new HashTable()), obj_map(new HashTable()), @@ -32,20 +34,19 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - lazy_sync_with_release(new HashTable()), + pending_acq_rel_seq(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), failed_promise(false), too_many_reads(false), - asserted(false) + asserted(false), + bad_synchronization(false) { /* Allocate this "size" on the snapshotting heap */ priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); /* First thread created will have id INITIAL_THREAD_ID */ priv->next_thread_id = INITIAL_THREAD_ID; - - lazy_sync_size = &priv->lazy_sync_size; } /** @brief Destructor */ @@ -64,7 +65,7 @@ ModelChecker::~ModelChecker() delete (*promises)[i]; delete promises; - delete lazy_sync_with_release; + delete pending_acq_rel_seq; delete thrd_last_action; delete node_stack; @@ -82,6 +83,7 @@ void ModelChecker::reset_to_initial_state() node_stack->reset_execution(); failed_promise = false; too_many_reads = false; + bad_synchronization = false; reset_asserted(); snapshotObject->backTrackBeforeStep(0); } @@ -98,6 +100,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() { @@ -138,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()) { @@ -157,8 +168,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(); @@ -180,8 +195,20 @@ bool ModelChecker::next_execution() DBG(); num_executions++; - if (isfinalfeasible()) + + if (isfinalfeasible()) { + printf("Earliest divergence point since last feasible execution:\n"); + 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(); @@ -243,6 +270,11 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) return NULL; } +/** This method find backtracking points where we should try to + * reorder the parameter ModelAction against. + * + * @param the ModelAction to find backtracking points for. + */ void ModelChecker::set_backtracking(ModelAction *act) { Thread *t = get_thread(act); @@ -254,26 +286,40 @@ void ModelChecker::set_backtracking(ModelAction *act) int low_tid, high_tid; if (node->is_enabled(t)) { - low_tid=id_to_int(act->get_tid()); - high_tid=low_tid+1; + low_tid = id_to_int(act->get_tid()); + high_tid = low_tid+1; } else { - low_tid=0; - high_tid=get_num_threads(); + low_tid = 0; + high_tid = get_num_threads(); } - - for(int i=low_tid;iis_enabled(tid)) continue; /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; - + + /* See if fairness allows */ + if (model->params.fairwindow != 0 && !node->has_priority(tid)) { + bool unfair=false; + for(int t=0;tget_num_threads();t++) { + thread_id_t tother=int_to_id(t); + if (node->is_enabled(tother) && node->has_priority(tother)) { + unfair=true; + break; + } + } + if (unfair) + continue; + } + /* Cache the latest backtracking point */ if (!priv->next_backtrack || *prev > *priv->next_backtrack) priv->next_backtrack = prev; - + /* If this is a new backtracking point, mark the tree */ if (!node->set_backtrack(tid)) continue; @@ -317,7 +363,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) bool r_status = false; if (!second_part_of_rmw) { - check_recency(curr); + check_recency(curr, reads_from); r_status = r_modification_order(curr, reads_from); } @@ -346,7 +392,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) /** * Processes a lock, trylock, or unlock model action. @param curr is - * the read model action to process. + * the read model action to process. * * The try lock operation checks whether the lock is taken. If not, * it falls to the normal lock operation case. If so, it returns @@ -357,14 +403,15 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) * * The unlock operation has to re-enable all of the threads that are * waiting on the lock. + * + * @return True if synchronization was updated; false otherwise */ - -void ModelChecker::process_mutex(ModelAction *curr) { - std::mutex * mutex=(std::mutex *) curr->get_location(); - struct std::mutex_state * state=mutex->get_state(); - switch(curr->get_type()) { +bool ModelChecker::process_mutex(ModelAction *curr) { + std::mutex *mutex = (std::mutex *)curr->get_location(); + struct std::mutex_state *state = mutex->get_state(); + switch (curr->get_type()) { case ATOMIC_TRYLOCK: { - bool success=!state->islocked; + bool success = !state->islocked; curr->set_try_lock(success); if (!success) { get_thread(curr)->set_return_value(0); @@ -374,25 +421,27 @@ void ModelChecker::process_mutex(ModelAction *curr) { } //otherwise fall into the lock case case ATOMIC_LOCK: { - if (curr->get_cv()->getClock(state->alloc_tid)<=state->alloc_clock) { + if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) { printf("Lock access before initialization\n"); set_assert(); } - state->islocked=true; - ModelAction *unlock=get_last_unlock(curr); + state->islocked = true; + ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement - if ( unlock != NULL ) + if (unlock != NULL) { curr->synchronize_with(unlock); + return true; + } break; } case ATOMIC_UNLOCK: { //unlock the lock - state->islocked=false; + state->islocked = false; //wake up the other threads - action_list_t * waiters = lock_waiters_map->get_safe_ptr(curr->get_location()); + 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())); + for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { + scheduler->wake(get_thread(*rit)); } waiters->clear(); break; @@ -400,9 +449,9 @@ void ModelChecker::process_mutex(ModelAction *curr) { default: ASSERT(0); } + return false; } - /** * Process a write ModelAction * @param curr The ModelAction to process @@ -414,7 +463,7 @@ bool ModelChecker::process_write(ModelAction *curr) bool updated_promises = resolve_promises(curr); if (promises->size() == 0) { - for (unsigned int i = 0; isize(); i++) { + for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) && (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) @@ -428,6 +477,64 @@ bool ModelChecker::process_write(ModelAction *curr) return updated_mod_order || updated_promises; } +/** + * @brief Process the current action for thread-related activity + * + * Performs current-action processing for a THREAD_* ModelAction. Proccesses + * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN + * synchronization, etc. This function is a no-op for non-THREAD actions + * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.) + * + * @param curr The current action + * @return True if synchronization was updated or a thread completed + */ +bool ModelChecker::process_thread_action(ModelAction *curr) +{ + bool updated = false; + + switch (curr->get_type()) { + case THREAD_CREATE: { + Thread *th = (Thread *)curr->get_location(); + th->set_creation(curr); + break; + } + case THREAD_JOIN: { + 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(); + 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()); + break; + } + default: + break; + } + + return updated; +} + /** * Initialize the current action by performing one or more of the following * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward @@ -446,34 +553,39 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) if (curr->is_rmwc() || curr->is_rmw()) { newcurr = process_rmw(curr); delete curr; - compute_promises(newcurr); + + if (newcurr->is_rmw()) + compute_promises(newcurr); 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 */ if (curr->is_rmwr()) newcurr->copy_typeandorder(curr); - ASSERT(curr->get_location()==newcurr->get_location()); + ASSERT(curr->get_location() == newcurr->get_location()); newcurr->copy_from_new(curr); /* Discard duplicate ModelAction; use action from NodeStack */ delete curr; - /* If we have diverged, we need to reset the clock vector. */ - if (diverge == NULL) - newcurr->create_cv(get_parent_action(newcurr->get_tid())); + /* Always compute new clock vector */ + newcurr->create_cv(get_parent_action(newcurr->get_tid())); } else { newcurr = curr; + + /* Always compute new clock vector */ + newcurr->create_cv(get_parent_action(newcurr->get_tid())); /* * Perform one-time actions when pushing new ModelAction onto * NodeStack */ - curr->create_cv(get_parent_action(curr->get_tid())); - if (curr->is_write()) - compute_promises(curr); + if (newcurr->is_write()) + compute_promises(newcurr); } return newcurr; } @@ -485,10 +597,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. */ - bool ModelChecker::check_action_enabled(ModelAction *curr) { if (curr->is_lock()) { - std::mutex * lock=(std::mutex *) curr->get_location(); + std::mutex * lock = (std::mutex *)curr->get_location(); struct std::mutex_state * state = lock->get_state(); if (state->islocked) { //Stick the action in the appropriate waiting queue @@ -519,10 +630,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); if (!check_action_enabled(curr)) { - //we'll make the execution look like we chose to run this action - //much later...when a lock is actually available to relese + /* 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); } @@ -537,44 +648,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) build_reads_from_past(curr); curr = newcurr; - /* Thread specific actions */ - switch (curr->get_type()) { - case THREAD_CREATE: { - Thread *th = (Thread *)curr->get_location(); - th->set_creation(curr); - break; - } - case THREAD_JOIN: { - 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); - } - break; - } - case THREAD_FINISH: { - Thread *th = get_thread(curr); - while (!th->wait_list_empty()) { - ModelAction *act = th->pop_wait_list(); - Thread *wake = get_thread(act); - scheduler->wake(wake); - do_complete_join(act); - } - th->complete(); - break; - } - case THREAD_START: { - check_promises(NULL, curr->get_cv()); - break; - } - default: - break; - } - + /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); while (!work_queue.empty()) { @@ -584,17 +658,24 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) switch (work.type) { case WORK_CHECK_CURR_ACTION: { ModelAction *act = work.action; - bool updated = false; + bool update = false; /* update this location's release seq's */ + bool update_all = false; /* update all release seq's */ + + if (process_thread_action(curr)) + update_all = true; + if (act->is_read() && process_read(act, second_part_of_rmw)) - updated = true; + update = true; if (act->is_write() && process_write(act)) - updated = true; + update = true; - if (act->is_mutex_op()) - process_mutex(act); + if (act->is_mutex_op() && process_mutex(act)) + update_all = true; - if (updated) + if (update_all) + work_queue.push_back(CheckRelSeqWorkEntry(NULL)); + else if (update) work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); break; } @@ -607,13 +688,15 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) bool updated = false; if (act->is_read()) { - if (r_modification_order(act, act->get_reads_from())) + const ModelAction *rf = act->get_reads_from(); + if (rf != NULL && r_modification_order(act, rf)) updated = true; } if (act->is_write()) { if (w_modification_order(act)) updated = true; } + mo_graph->commitChanges(); if (updated) work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); @@ -672,11 +755,14 @@ 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 && *lazy_sync_size == 0; + return promises->size() == 0 && pending_acq_rel_seq->size() == 0; } /** @return whether the current partial trace is feasible. */ bool ModelChecker::isfeasible() { + if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) + DEBUG("Infeasible: RMW violation\n"); + return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW(); } @@ -690,10 +776,12 @@ bool ModelChecker::isfeasibleotherthanRMW() { DEBUG("Infeasible: failed promise\n"); if (too_many_reads) DEBUG("Infeasible: too many reads\n"); + if (bad_synchronization) + DEBUG("Infeasible: bad synchronization ordering\n"); if (promises_expired()) DEBUG("Infeasible: promises expired\n"); } - return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired(); + return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired(); } /** Returns whether the current completed trace is feasible. */ @@ -727,23 +815,21 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { * * If so, we decide that the execution is no longer feasible. */ -void ModelChecker::check_recency(ModelAction *curr) { +void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { if (params.maxreads != 0) { + if (curr->get_node()->get_read_from_size() <= 1) return; - //Must make sure that execution is currently feasible... We could //accidentally clear by rolling back if (!isfeasible()) return; - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); int tid = id_to_int(curr->get_tid()); /* Skip checks */ if ((int)thrd_lists->size() <= tid) return; - action_list_t *list = &(*thrd_lists)[tid]; action_list_t::reverse_iterator rit = list->rbegin(); @@ -762,17 +848,18 @@ void ModelChecker::check_recency(ModelAction *curr) { ModelAction *act = *rit; if (!act->is_read()) return; - if (act->get_reads_from() != curr->get_reads_from()) + + if (act->get_reads_from() != rf) return; if (act->get_node()->get_read_from_size() <= 1) return; } - for (int i = 0; iget_node()->get_read_from_size(); i++) { //Get write const ModelAction * write = curr->get_node()->get_read_from_at(i); + //Need a different write - if (write==curr->get_reads_from()) + if (write==rf) continue; /* Test to see whether this is a feasible write to read from*/ @@ -812,7 +899,7 @@ void ModelChecker::check_recency(ModelAction *curr) { /** * Updates the mo_graph with the constraints imposed from the current - * read. + * read. * * Basic idea is the following: Go through each other thread and find * the lastest action that happened before our read. Two cases: @@ -854,7 +941,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; } @@ -871,7 +962,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf * promises. The basic problem is that actions that occur after the * read curr could not property add items to the modification order * for our read. - * + * * So for each thread, we find the earliest item that happens after * the read curr. This is the item we have to fix up with additional * constraints. If that action is write, we add a MO edge between @@ -882,7 +973,6 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf * @param rf is the write ModelAction that curr reads from. * */ - void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf) { std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); @@ -896,10 +986,10 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio action_list_t::reverse_iterator rit; ModelAction *lastact = NULL; - /* Find last action that happens after curr */ + /* Find last action that happens after curr that is either not curr or a rmw */ for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - if (curr->happens_before(act)) { + if (curr->happens_before(act) && (curr != act || curr->is_rmw())) { lastact = act; } else break; @@ -907,12 +997,25 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio /* Include at most one act per-thread that "happens before" curr */ if (lastact != NULL) { - if (lastact->is_read()) { + if (lastact==curr) { + //Case 1: The resolved read is a RMW, and we need to make sure + //that the write portion of the RMW mod order after rf + + mo_graph->addEdge(rf, lastact); + } else if (lastact->is_read()) { + //Case 2: The resolved read is a normal read and the next + //operation is a read, and we need to make sure the value read + //is mod ordered after rf + const ModelAction *postreadfrom = lastact->get_reads_from(); if (postreadfrom != NULL&&rf != postreadfrom) mo_graph->addEdge(rf, postreadfrom); - } else if (rf != lastact) { - mo_graph->addEdge(rf, lastact); + } else { + //Case 3: The resolved read is a normal read and the next + //operation is a write, and we need to make sure that the + //write is mod ordered after rf + if (lastact!=rf) + mo_graph->addEdge(rf, lastact); } break; } @@ -967,14 +1070,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; } @@ -991,8 +1102,12 @@ 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) && @@ -1007,7 +1122,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (thin_air_constraint_may_allow(curr, act)) { if (isfeasible() || - (curr->is_rmw() && act->is_rmw() && curr->get_reads_from()==act->get_reads_from() && isfeasibleotherthanRMW())) { + (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) { struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act}; futurevalues->push_back(pfv); } @@ -1022,7 +1137,6 @@ bool ModelChecker::w_modification_order(ModelAction *curr) /** Arbitrary reads from the future are not allowed. Section 29.3 * part 9 places some constraints. This method checks one result of constraint * constraint. Others require compiler support. */ - bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) { if (!writer->is_rmw()) return true; @@ -1031,7 +1145,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con return true; for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) { - if (search==reader) + if (search == reader) return false; if (search->get_tid() == reader->get_tid() && search->happens_before(reader)) @@ -1064,24 +1178,36 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con */ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const { - if (!rf) { - /* read from future: need to settle this later */ - return false; /* incomplete */ - } + /* Only check for release sequences if there are no cycles */ + if (mo_graph->checkForCycles()) + return false; - ASSERT(rf->is_write()); + while (rf) { + ASSERT(rf->is_write()); + + if (rf->is_release()) + release_heads->push_back(rf); + if (!rf->is_rmw()) + break; /* End of RMW chain */ - if (rf->is_release()) - release_heads->push_back(rf); - if (rf->is_rmw()) { - /* We need a RMW action that is both an acquire and release to stop */ /** @todo Need to be smarter here... In the linux lock * example, this will run to the beginning of the program for * every acquire. */ + /** @todo The way to be smarter here is to keep going until 1 + * thread has a release preceded by an acquire and you've seen + * both. */ + + /* acq_rel RMW is a sufficient stopping condition */ if (rf->is_acquire() && rf->is_release()) return true; /* complete */ - return release_seq_head(rf->get_reads_from(), release_heads); + + rf = rf->get_reads_from(); + }; + if (!rf) { + /* read from future: need to settle this later */ + return false; /* incomplete */ } + if (rf->is_release()) return true; /* complete */ @@ -1118,10 +1244,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * the release seq? */ bool future_ordered = false; + ModelAction *last = get_last_action(int_to_id(i)); + if (last && (rf->happens_before(last) || + last->get_type() == THREAD_FINISH)) + future_ordered = true; + for (rit = list->rbegin(); rit != list->rend(); rit++) { const ModelAction *act = *rit; - if (!act->is_write()) - continue; /* Reach synchronization -> this thread is complete */ if (act->happens_before(release)) break; @@ -1130,6 +1259,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel continue; } + /* Only writes can break release sequences */ + if (!act->is_write()) + continue; + /* Check modification order */ if (mo_graph->checkReachable(rf, act)) { /* rf --mo--> act */ @@ -1174,10 +1307,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel complete = release_seq_head(rf, release_heads); if (!complete) { /* add act to 'lazy checking' list */ - action_list_t *list; - list = lazy_sync_with_release->get_safe_ptr(act->get_location()); - list->push_back(act); - (*lazy_sync_size)++; + pending_acq_rel_seq->push_back(act); } } @@ -1188,7 +1318,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel * modification order information is present at the time an action occurs. * * @param location The location/object that should be checked for release - * sequence resolutions + * sequence resolutions. A NULL value means to check all locations. * @param work_queue The work queue to which to add work items as they are * generated * @return True if any updates occurred (new synchronization, new mo_graph @@ -1196,34 +1326,40 @@ 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) { - action_list_t *list; - list = lazy_sync_with_release->getptr(location); - if (!list) - return false; - bool updated = false; - action_list_t::iterator it = list->begin(); - while (it != list->end()) { + std::vector::iterator it = pending_acq_rel_seq->begin(); + while (it != pending_acq_rel_seq->end()) { ModelAction *act = *it; + + /* Only resolve sequences on the given location, if provided */ + if (location && act->get_location() != location) { + it++; + continue; + } + const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; complete = release_seq_head(rf, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) { if (!act->has_synchronized_with(release_heads[i])) { - updated = true; - act->synchronize_with(release_heads[i]); + if (act->synchronize_with(release_heads[i])) + updated = true; + else + set_bad_synchronization(); } } 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)); /* propagate synchronization to later actions */ - action_list_t::reverse_iterator it = action_trace->rbegin(); - while ((*it) != act) { - ModelAction *propagate = *it; + action_list_t::reverse_iterator rit = action_trace->rbegin(); + for (; (*rit) != act; rit++) { + ModelAction *propagate = *rit; if (act->happens_before(propagate)) { propagate->synchronize_with(act); /* Re-check 'propagate' for mo_graph edges */ @@ -1231,10 +1367,9 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } } } - if (complete) { - it = list->erase(it); - (*lazy_sync_size)--; - } else + if (complete) + it = pending_acq_rel_seq->erase(it); + else it++; } @@ -1356,16 +1491,20 @@ bool ModelChecker::resolve_promises(ModelAction *write) Promise *promise = (*promises)[promise_index]; if (write->get_node()->get_promise(i)) { ModelAction *read = promise->get_action(); - read->read_from(write); if (read->is_rmw()) { mo_graph->addRMWEdge(write, read); } + read->read_from(write); //First fix up the modification order for actions that happened //before the read r_modification_order(read, write); //Next fix up the modification order for actions that happened //after the read. 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); resolved = true; } else @@ -1453,7 +1592,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */ - if (!curr->is_seqcst()|| (!act->is_seqcst() && (last_seq_cst==NULL||!act->happens_before(last_seq_cst))) || act == last_seq_cst) { + if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) { DEBUG("Adding action to may_read_from:\n"); if (DBG_ENABLED()) { act->print(); @@ -1499,6 +1638,34 @@ static void print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); } +#if SUPPORT_MOD_ORDER_DUMP +void ModelChecker::dumpGraph(char *filename) { + char buffer[200]; + sprintf(buffer, "%s.dot",filename); + FILE *file=fopen(buffer, "w"); + fprintf(file, "digraph %s {\n",filename); + mo_graph->dumpNodes(file); + ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads()); + + for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) { + 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()); + 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()); + } + + thread_array[action->get_tid()]=action; + } + fprintf(file,"}\n"); + model_free(thread_array); + fclose(file); +} +#endif + void ModelChecker::print_summary() { printf("\n"); @@ -1511,6 +1678,8 @@ void ModelChecker::print_summary() char buffername[100]; sprintf(buffername, "exec%04u", num_executions); mo_graph->dumpGraphToFile(buffername); + sprintf(buffername, "graph%04u", num_executions); + dumpGraph(buffername); #endif if (!isfinalfeasible()) @@ -1530,17 +1699,44 @@ void ModelChecker::add_thread(Thread *t) scheduler->add_thread(t); } +/** + * Removes a thread from the scheduler. + * @param the thread to remove. + */ 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) @@ -1560,35 +1756,36 @@ 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); priv->nextThread = check_current_action(priv->current_action); priv->current_action = NULL; + if (curr->is_blocked() || curr->is_complete()) scheduler->remove_thread(curr); } else { 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); /* 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);