X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c9353db71c5bc15c77e802c32285f64f0c697681;hb=3ca736f95f5a2ade69700fb2c148f348a0a683f9;hp=1598fb9a276343ba3daf59f3beedad6d452115e7;hpb=eb3b6cccf71b9eeee035e2c98566dfa279e402ae;p=c11tester.git diff --git a/model.cc b/model.cc index 1598fb9a..c9353db7 100644 --- a/model.cc +++ b/model.cc @@ -139,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()) { @@ -158,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(); @@ -181,23 +188,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 +434,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 +479,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 +500,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 +511,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 +525,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } - return synchronized; + return updated; } /** @@ -540,6 +552,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 +626,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); } @@ -920,7 +934,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; } @@ -1045,14 +1063,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; } @@ -1069,8 +1095,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) && @@ -1314,6 +1344,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 +1497,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 @@ -1611,7 +1644,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());