X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=4f2719f338c8afa9ba05d2f0835fd565bd6dfbd2;hp=2260431ab908973fe5b4233e9e15ceeb8be4ca2f;hb=b8b39c87557325a384faa45d0cae56a6f71f52b1;hpb=2de6c82d6d7e6af2267636ec55f7e81d2a799a78 diff --git a/model.cc b/model.cc index 2260431..4f2719f 100644 --- a/model.cc +++ b/model.cc @@ -47,6 +47,10 @@ ModelChecker::ModelChecker(struct model_params params) : 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; + + /* Initialize a model-checker thread, for special ModelActions */ + model_thread = new Thread(get_next_id()); + thread_map->put(id_to_int(model_thread->get_id()), model_thread); } /** @brief Destructor */ @@ -150,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. */ @@ -163,15 +170,24 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* The next node will try to read from a different future value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); + } else if (nextnode->increment_relseq_break()) { + /* The next node will try to resolve a release sequence differently */ + tid = next->get_tid(); + 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. */ + scheduler->remove_sleep(thread_map->get(id_to_int(tid))); 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; @@ -183,6 +199,40 @@ 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); + 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. @@ -270,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. @@ -295,9 +345,10 @@ 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; - + /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; @@ -315,7 +366,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; @@ -540,6 +590,76 @@ bool ModelChecker::process_thread_action(ModelAction *curr) return updated; } +/** + * @brief Process the current action for release sequence fixup activity + * + * Performs model-checker release sequence fixups for the current action, + * forcing a single pending release sequence to break (with a given, potential + * "loose" write) or to complete (i.e., synchronize). If a pending release + * sequence forms a complete release sequence, then we must perform the fixup + * synchronization, mo_graph additions, etc. + * + * @param curr The current action; must be a release sequence fixup action + * @param work_queue The work queue to which to add work items as they are + * generated + */ +void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue) +{ + const ModelAction *write = curr->get_node()->get_relseq_break(); + struct release_seq *sequence = pending_rel_seqs->back(); + pending_rel_seqs->pop_back(); + ASSERT(sequence); + ModelAction *acquire = sequence->acquire; + const ModelAction *rf = sequence->rf; + const ModelAction *release = sequence->release; + ASSERT(acquire); + ASSERT(release); + ASSERT(rf); + 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(); + return; + } + /* Re-check all pending release sequences */ + work_queue->push_back(CheckRelSeqWorkEntry(NULL)); + /* Re-check act for mo_graph edges */ + work_queue->push_back(MOEdgeWorkEntry(acquire)); + + /* propagate synchronization to later actions */ + action_list_t::reverse_iterator rit = action_trace->rbegin(); + for (; (*rit) != acquire; rit++) { + ModelAction *propagate = *rit; + if (acquire->happens_before(propagate)) { + propagate->synchronize_with(acquire); + /* Re-check 'propagate' for mo_graph edges */ + work_queue->push_back(MOEdgeWorkEntry(propagate)); + } + } + } else { + /* Break release sequence with new edges: + * release --mo--> write --mo--> rf */ + mo_graph->addEdge(release, write); + mo_graph->addEdge(write, rf); + } + + /* See if we have realized a data race */ + if (checkDataRaces()) + set_assert(); +} + /** * Initialize the current action by performing one or more of the following * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward @@ -591,6 +711,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) */ if (newcurr->is_write()) compute_promises(newcurr); + else if (newcurr->is_relseq_fixup()) + compute_relseq_breakwrites(newcurr); } return newcurr; } @@ -631,7 +753,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)) { @@ -642,8 +763,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); @@ -655,7 +779,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(); @@ -678,6 +801,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_mutex_op() && process_mutex(act)) update_all = true; + if (act->is_relseq_fixup()) + process_relseq_fixup(curr, &work_queue); + if (update_all) work_queue.push_back(CheckRelSeqWorkEntry(NULL)); else if (update) @@ -714,9 +840,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) } check_curr_backtracking(curr); - set_backtracking(curr); - return get_next_thread(curr); } @@ -740,7 +864,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { if ((!parnode->backtrack_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || - !currnode->promise_empty()) + !currnode->promise_empty() || + !currnode->relseq_break_empty()) && (!priv->next_backtrack || *curr > *priv->next_backtrack)) { priv->next_backtrack = curr; @@ -1258,10 +1383,14 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, bool future_ordered = false; ModelAction *last = get_last_action(int_to_id(i)); - if (last && (rf->happens_before(last) || - get_thread(int_to_id(i))->is_complete())) + Thread *th = get_thread(int_to_id(i)); + if ((last && rf->happens_before(last)) || + !scheduler->is_enabled(th) || + 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 */ @@ -1650,6 +1779,29 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) } } +/** + * Compute the set of writes that may break the current pending release + * sequence. This information is extracted from previou release sequence + * calculations. + * + * @param curr The current ModelAction. Must be a release sequence fixup + * action. + */ +void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) +{ + if (pending_rel_seqs->empty()) + return; + + struct release_seq *pending = pending_rel_seqs->back(); + for (unsigned int i = 0; i < pending->writes.size(); i++) { + const ModelAction *write = pending->writes[i]; + curr->get_node()->add_relseq_break(write); + } + + /* NULL means don't break the sequence; just synchronize */ + curr->get_node()->add_relseq_break(NULL); +} + /** * Build up an initial set of all past writes that this 'read' action may read * from. This set is determined by the clock vector's "happens before" @@ -1853,7 +2005,7 @@ bool ModelChecker::take_step() { if (has_asserted()) return false; - Thread *curr = thread_current(); + Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL; if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); @@ -1876,6 +2028,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;