X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=38f40e5cd1ee55b47103883fa9677b6ad7ea7e6d;hb=7c77391dff9f4cf3166d47015494f0af276963f0;hp=fd9068586bc6f23f1371327ce0c337e837c15e9f;hpb=a3f3df022fdfd22dd6a8e877610b4b82281926fd;p=model-checker.git diff --git a/model.cc b/model.cc index fd90685..38f40e5 100644 --- a/model.cc +++ b/model.cc @@ -25,6 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) : num_executions(0), num_feasible_executions(0), diverge(NULL), + earliest_diverge(NULL), action_trace(new action_list_t()), thread_map(new HashTable()), obj_map(new HashTable()), @@ -38,7 +39,8 @@ ModelChecker::ModelChecker(struct model_params params) : 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)); @@ -80,6 +82,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); } @@ -136,6 +139,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()) { @@ -155,8 +161,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(); @@ -178,8 +188,16 @@ 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++; + } if (isfinalfeasible() || DBG_ENABLED()) print_summary(); @@ -334,7 +352,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); } @@ -412,7 +430,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; @@ -457,11 +475,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: { @@ -470,28 +488,20 @@ bool ModelChecker::process_thread_action(ModelAction *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); - synchronized = true; - } + Thread *blocking = (Thread *)curr->get_location(); + ModelAction *act = get_last_action(blocking->get_id()); + curr->synchronize_with(act); + 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); - synchronized = true; + scheduler->wake(get_thread(act)); } th->complete(); + updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { @@ -502,7 +512,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } - return synchronized; + return updated; } /** @@ -523,10 +533,14 @@ 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 */ @@ -539,26 +553,30 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *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; } /** - * 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. + * @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. + * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. */ @@ -571,6 +589,12 @@ 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; @@ -596,9 +620,9 @@ 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 is actually available to release */ + * much later, when a lock/join can succeed */ get_current_thread()->set_pending(curr); - remove_thread(get_current_thread()); + scheduler->sleep(get_current_thread()); return get_next_thread(NULL); } @@ -653,13 +677,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())); @@ -678,19 +704,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(curr); } -/** - * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH - * operation from the Thread it is joining with. Must be called after the - * completion of the Thread in question. - * @param join The THREAD_JOIN action - */ -void ModelChecker::do_complete_join(ModelAction *join) -{ - Thread *blocking = (Thread *)join->get_location(); - ModelAction *act = get_last_action(blocking->get_id()); - join->synchronize_with(act); -} - void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); @@ -739,10 +752,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. */ @@ -776,23 +791,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(); @@ -811,17 +824,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*/ @@ -944,10 +958,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; @@ -955,12 +969,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; } @@ -1111,6 +1138,10 @@ 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 { + /* Only check for release sequences if there are no cycles */ + if (mo_graph->checkForCycles()) + return false; + while (rf) { ASSERT(rf->is_write()); @@ -1272,12 +1303,16 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ 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)); @@ -1419,18 +1454,15 @@ bool ModelChecker::resolve_promises(ModelAction *write) if (read->is_rmw()) { mo_graph->addRMWEdge(write, read); } - - /* Only read (and check for release sequences) if this - * write (esp. RMW) doesn't create cycles */ - if (!mo_graph->checkForCycles()) - read->read_from(write); - + 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()); promises->erase(promises->begin() + promise_index); resolved = true; @@ -1565,6 +1597,33 @@ 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()); + 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"); @@ -1577,6 +1636,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()) @@ -1637,6 +1698,7 @@ bool ModelChecker::take_step() { priv->nextThread = check_current_action(priv->current_action); priv->current_action = NULL; + if (curr->is_blocked() || curr->is_complete()) scheduler->remove_thread(curr); } else {