X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=f8482cbf7b9db9eb9689a213c5de18cf3b583ad9;hb=b6f06ab2c626eb6e0f044fa9c7d1b74fbc82a09d;hp=c1818ad5bfb8fb48c8b8e9221212119b2ca125ff;hpb=495dd308fe91920ea85719d8380d9cf28ee85274;p=cdsspec-compiler.git diff --git a/model.cc b/model.cc index c1818ad..f8482cb 100644 --- a/model.cc +++ b/model.cc @@ -32,10 +32,10 @@ ModelChecker::ModelChecker(struct model_params params) : obj_map(new HashTable()), lock_waiters_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), - promises(new std::vector()), - futurevalues(new std::vector()), - pending_rel_seqs(new std::vector()), - thrd_last_action(new std::vector(1)), + promises(new std::vector< Promise *, SnapshotAlloc >()), + futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc >()), + pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc >()), + thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc >(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), failed_promise(false), @@ -154,6 +154,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) earliest_diverge=diverge; Node *nextnode = next->get_node(); + Node *prevnode = nextnode->get_parent(); + scheduler->update_sleep_set(prevnode); + /* Reached divergence point */ if (nextnode->increment_promise()) { /* The next node will try to satisfy a different set of promises. */ @@ -173,13 +176,17 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) node_stack->pop_restofstack(2); } else { /* Make a different thread execute for next step */ - Node *node = nextnode->get_parent(); - tid = node->get_next_backtrack(); + scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid()))); + tid = prevnode->get_next_backtrack(); + /* Make sure the backtracked thread isn't sleeping. */ node_stack->pop_restofstack(1); if (diverge==earliest_diverge) { - earliest_diverge=node->get_action(); + earliest_diverge=prevnode->get_action(); } } + /* The correct sleep set is in the parent node. */ + execute_sleep_set(); + DEBUG("*** Divergence point ***\n"); diverge = NULL; @@ -191,6 +198,41 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) return thread_map->get(id_to_int(tid)); } +/** + * We need to know what the next actions of all threads in the sleep + * set will be. This method computes them and stores the actions at + * the corresponding thread object's pending action. + */ + +void ModelChecker::execute_sleep_set() { + for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { + thr->set_state(THREAD_RUNNING); + scheduler->next_thread(thr); + Thread::swap(&system_context, thr); + priv->current_action->set_sleep_flag(); + thr->set_pending(priv->current_action); + } + } + priv->current_action = NULL; +} + +void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { + for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { + ModelAction *pending_act=thr->get_pending(); + if (pending_act->could_synchronize_with(curr)) { + //Remove this thread from sleep set + scheduler->remove_sleep(thr); + } + } + } +} + /** * Queries the model-checker for more executions to explore and, if one * exists, resets the model-checker state to execute a new execution. @@ -278,7 +320,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) return NULL; } -/** This method find backtracking points where we should try to +/** This method finds backtracking points where we should try to * reorder the parameter ModelAction against. * * @param the ModelAction to find backtracking points for. @@ -303,9 +345,11 @@ void ModelChecker::set_backtracking(ModelAction *act) for(int i = low_tid; i < high_tid; i++) { thread_id_t tid = int_to_id(i); - if (!node->is_enabled(tid)) - continue; + /* Don't backtrack into a point where the thread is disabled or sleeping. */ + if (node->get_enabled_array()[i]!=THREAD_ENABLED) + continue; + /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; @@ -323,7 +367,6 @@ void ModelChecker::set_backtracking(ModelAction *act) if (unfair) continue; } - /* Cache the latest backtracking point */ if (!priv->next_backtrack || *prev > *priv->next_backtrack) priv->next_backtrack = prev; @@ -576,6 +619,16 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu ASSERT(release->same_thread(rf)); if (write == NULL) { + /** + * @todo Forcing a synchronization requires that we set + * modification order constraints. For instance, we can't allow + * a fixup sequence in which two separate read-acquire + * operations read from the same sequence, where the first one + * synchronizes and the other doesn't. Essentially, we can't + * allow any writes to insert themselves between 'release' and + * 'rf' + */ + /* Must synchronize */ if (!acquire->synchronize_with(release)) { set_bad_synchronization(); @@ -602,6 +655,10 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu mo_graph->addEdge(release, write); mo_graph->addEdge(write, rf); } + + /* See if we have realized a data race */ + if (checkDataRaces()) + set_assert(); } /** @@ -697,7 +754,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { Thread * ModelChecker::check_current_action(ModelAction *curr) { ASSERT(curr); - bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); if (!check_action_enabled(curr)) { @@ -708,8 +764,11 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(NULL); } + wake_up_sleeping_actions(curr); + ModelAction *newcurr = initialize_curr_action(curr); + /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw) add_action_to_lists(newcurr); @@ -721,7 +780,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); - while (!work_queue.empty()) { WorkQueueEntry work = work_queue.front(); work_queue.pop_front(); @@ -783,9 +841,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) } check_curr_backtracking(curr); - set_backtracking(curr); - return get_next_thread(curr); } @@ -1241,7 +1297,6 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * "returns" two pieces of data: a pass-by-reference vector of @a release_heads * and a boolean representing certainty. * - * @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 @@ -1334,6 +1389,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, th->is_complete()) future_ordered = true; + ASSERT(!th->is_model_thread() || future_ordered); + for (rit = list->rbegin(); rit != list->rend(); rit++) { const ModelAction *act = *rit; /* Reach synchronization -> this thread is complete */ @@ -1422,7 +1479,7 @@ 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_rel_seqs->begin(); + std::vector< struct release_seq *, SnapshotAlloc >::iterator it = pending_rel_seqs->begin(); while (it != pending_rel_seqs->end()) { struct release_seq *pending = *it; ModelAction *act = pending->acquire; @@ -1584,7 +1641,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; - std::vector threads_to_check; + std::vector< thread_id_t, ModelAlloc > threads_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; @@ -1790,7 +1847,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) act->print(); curr->print(); } - curr->get_node()->add_read_from(act); + + if (curr->get_sleep_flag()) { + if (sleep_can_read_from(curr, act)) + curr->get_node()->add_read_from(act); + } else + curr->get_node()->add_read_from(act); } /* Include at most one act per-thread that "happens before" curr */ @@ -1817,6 +1879,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) ASSERT(initialized); } +bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { + while(true) { + Node *prevnode=write->get_node()->get_parent(); + bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET; + if (write->is_release()&&thread_sleep) + return true; + if (!write->is_rmw()) + return false; + if (write->get_reads_from()==NULL) + return true; + write=write->get_reads_from(); + } +} + static void print_list(action_list_t *list) { action_list_t::iterator it; @@ -1971,6 +2047,26 @@ bool ModelChecker::take_step() { DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, next ? id_to_int(next->get_id()) : -1); + /* + * Launch end-of-execution release sequence fixups only when there are: + * + * (1) no more user threads to run (or when execution replay chooses + * the 'model_thread') + * (2) pending release sequences + * (3) pending assertions (i.e., data races) + * (4) no pending promises + */ + if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) && + isfinalfeasible() && !unrealizedraces.empty()) { + printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", + pending_rel_seqs->size()); + ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, + std::memory_order_seq_cst, NULL, VALUE_NONE, + model_thread); + set_current_action(fixup); + return true; + } + /* next == NULL -> don't take any more steps */ if (!next) return false;