X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=c0cc93eb0a80523eefc48f2fe7ec3c8119d8619c;hp=21b2b77b16c83cced2f13730e8f0ac2e59bcc577;hb=4546308ab989c074f83d8607e16f13ffbcff494a;hpb=e44b9753a9b616cba58c2fb0583b876e3d4006ae diff --git a/model.cc b/model.cc index 21b2b77..c0cc93e 100644 --- a/model.cc +++ b/model.cc @@ -12,7 +12,7 @@ #include "promise.h" #include "datarace.h" #include "mutex.h" -#include "threads.h" +#include "threads-model.h" #define INITIAL_THREAD_ID 0 @@ -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_acq_rel_seq(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), @@ -47,12 +47,16 @@ 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 */ ModelChecker::~ModelChecker() { - for (int i = 0; i < get_num_threads(); i++) + for (unsigned int i = 0; i < get_num_threads(); i++) delete thread_map->get(i); delete thread_map; @@ -65,7 +69,7 @@ ModelChecker::~ModelChecker() delete (*promises)[i]; delete promises; - delete pending_acq_rel_seq; + delete pending_rel_seqs; delete thrd_last_action; delete node_stack; @@ -95,7 +99,7 @@ thread_id_t ModelChecker::get_next_id() } /** @return the number of user threads created during this execution */ -int ModelChecker::get_num_threads() +unsigned int ModelChecker::get_num_threads() { return priv->next_thread_id; } @@ -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,23 @@ 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. */ 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 +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. @@ -199,7 +249,7 @@ bool ModelChecker::next_execution() if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) - earliest_diverge->print(false); + earliest_diverge->print(); else printf("(Not set)\n"); @@ -207,10 +257,11 @@ bool ModelChecker::next_execution() num_feasible_executions++; } - DEBUG("Number of acquires waiting on pending release sequences: %lu\n", - pending_acq_rel_seq->size()); + DEBUG("Number of acquires waiting on pending release sequences: %zu\n", + pending_rel_seqs->size()); - if (isfinalfeasible() || DBG_ENABLED()) + + if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) print_summary(); if ((diverge = get_next_backtrack()) == NULL) @@ -236,7 +287,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (act->is_synchronizing(prev)) + if (prev->could_synchronize_with(act)) return prev; } break; @@ -270,7 +321,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 +346,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; @@ -315,7 +368,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; @@ -377,6 +429,8 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) curr->read_from(reads_from); mo_graph->commitChanges(); + mo_check_promises(curr->get_tid(), reads_from); + updated |= r_status; } else if (!second_part_of_rmw) { /* Read from future value */ @@ -466,7 +520,9 @@ bool ModelChecker::process_write(ModelAction *curr) if (promises->size() == 0) { 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) && + //Do more ambitious checks now that mo is more complete + if (mo_may_allow(pfv.writer, pfv.act)&& + pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) && (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) priv->next_backtrack = pfv.act; } @@ -474,6 +530,8 @@ bool ModelChecker::process_write(ModelAction *curr) } mo_graph->commitChanges(); + mo_check_promises(curr->get_tid(), curr); + get_thread(curr)->set_return_value(VALUE_NONE); return updated_mod_order || updated_promises; } @@ -500,33 +558,24 @@ 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); - updated = true; /* trigger rel-seq checks */ - } + 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); - updated = true; /* trigger rel-seq checks */ + scheduler->wake(get_thread(act)); } th->complete(); updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { - check_promises(NULL, curr->get_cv()); + check_promises(curr->get_tid(), NULL, curr->get_cv()); break; } default: @@ -536,6 +585,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 @@ -587,14 +706,19 @@ 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; } /** - * 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. */ @@ -607,6 +731,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; @@ -627,19 +757,21 @@ 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)) { /* 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); scheduler->sleep(get_current_thread()); 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); @@ -651,7 +783,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(); @@ -674,6 +805,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) @@ -710,25 +844,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) } check_curr_backtracking(curr); - set_backtracking(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(); @@ -736,7 +855,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; @@ -756,7 +876,7 @@ 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 && pending_acq_rel_seq->size() == 0; + return promises->size() == 0 && pending_rel_seqs->size() == 0; } /** @return whether the current partial trace is feasible. */ @@ -1110,7 +1230,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) } added = true; break; - } else if (act->is_read() && !act->is_synchronizing(curr) && + } else if (act->is_read() && !act->could_synchronize_with(curr) && !act->same_thread(curr)) { /* We have an action that: (1) did not happen before us @@ -1118,12 +1238,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr) (3) cannot synchronize with us (4) is in a different thread => - that read could potentially read from our write. + that read could potentially read from our write. Note that + these checks are overly conservative at this point, we'll + do more checks before actually removing the + pendingfuturevalue. + */ 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())) { - struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act}; + struct PendingFutureValue pfv = {curr,act}; futurevalues->push_back(pfv); } } @@ -1155,6 +1279,33 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con return true; } +/** 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::mo_may_allow(const ModelAction * writer, const ModelAction *reader) { + std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); + + //Get write that follows reader action + action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())]; + action_list_t::reverse_iterator rit; + ModelAction *first_write_after_read=NULL; + + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + if (act==reader) + break; + if (act->is_write()) + first_write_after_read=act; + } + + if (first_write_after_read==NULL) + return true; + + return !mo_graph->checkReachable(first_write_after_read, writer); +} + + + /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. * The ModelAction under consideration is expected to be taking part in @@ -1167,16 +1318,21 @@ 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 + * @param release_heads A pass-by-reference style return parameter. After * execution of this function, release_heads will contain the heads of all the - * relevant release sequences, if any exists + * relevant release sequences, if any exists with certainty + * @param pending A pass-by-reference style return parameter which is only used + * when returning false (i.e., uncertain). Returns most information regarding + * an uncertain release sequence, including any write operations that might + * break the sequence. * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const +bool ModelChecker::release_seq_heads(const ModelAction *rf, + rel_heads_list_t *release_heads, + struct release_seq *pending) const { /* Only check for release sequences if there are no cycles */ if (mo_graph->checkForCycles()) @@ -1205,6 +1361,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re }; if (!rf) { /* read from future: need to settle this later */ + pending->rf = NULL; return false; /* incomplete */ } @@ -1234,6 +1391,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re ASSERT(rf->same_thread(release)); + pending->writes.clear(); + bool certain = true; for (unsigned int i = 0; i < thrd_lists->size(); i++) { if (id_to_int(rf->get_tid()) == (int)i) @@ -1245,10 +1404,14 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re 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 */ @@ -1277,14 +1440,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re /* release --mo-> act --mo--> rf */ return true; /* complete */ } + /* act may break release sequence */ + pending->writes.push_back(act); certain = false; } if (!future_ordered) - return false; /* This thread is uncertain */ + certain = false; /* This thread is uncertain */ } - if (certain) + if (certain) { release_heads->push_back(release); + pending->writes.clear(); + } else { + pending->release = release; + pending->rf = rf; + } return certain; } @@ -1303,11 +1473,14 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); - bool complete; - complete = release_seq_heads(rf, release_heads); - if (!complete) { + struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq)); + sequence->acquire = act; + + if (!release_seq_heads(rf, release_heads, sequence)) { /* add act to 'lazy checking' list */ - pending_acq_rel_seq->push_back(act); + pending_rel_seqs->push_back(sequence); + } else { + snapshot_free(sequence); } } @@ -1327,9 +1500,10 @@ 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_acq_rel_seq->begin(); - while (it != pending_acq_rel_seq->end()) { - ModelAction *act = *it; + 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; /* Only resolve sequences on the given location, if provided */ if (location && act->get_location() != location) { @@ -1340,7 +1514,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; - complete = release_seq_heads(rf, &release_heads); + complete = release_seq_heads(rf, &release_heads, pending); for (unsigned int i = 0; i < release_heads.size(); i++) { if (!act->has_synchronized_with(release_heads[i])) { if (act->synchronize_with(release_heads[i])) @@ -1367,10 +1541,12 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } } } - if (complete) - it = pending_acq_rel_seq->erase(it); - else + if (complete) { + it = pending_rel_seqs->erase(it); + snapshot_free(pending); + } else { it++; + } } // If we resolved promises or data races, see if we have realized a data race. @@ -1486,6 +1662,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; + 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]; @@ -1503,13 +1680,22 @@ bool ModelChecker::resolve_promises(ModelAction *write) 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); + threads_to_check.push_back(read->get_tid()); + resolved = true; } else promise_index++; } + + //Check whether reading these writes has made threads unable to + //resolve promises + + for(unsigned int i=0;iget_action(); if (!act->happens_before(curr) && act->is_read() && - !act->is_synchronizing(curr) && + !act->could_synchronize_with(curr) && !act->same_thread(curr) && promise->get_value() == curr->get_value()) { curr->get_node()->set_promise(i); @@ -1535,16 +1721,14 @@ void ModelChecker::compute_promises(ModelAction *curr) } /** Checks promises in response to change in ClockVector Threads. */ -void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) +void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv) { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; const ModelAction *act = promise->get_action(); if ((old_cv == NULL || !old_cv->synchronized_since(act)) && merge_cv->synchronized_since(act)) { - //This thread is no longer able to send values back to satisfy the promise - int num_synchronized_threads = promise->increment_threads(); - if (num_synchronized_threads == get_num_threads()) { + if (promise->increment_threads(tid)) { //Promise has failed failed_promise = true; return; @@ -1553,6 +1737,97 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) } } +/** Checks promises in response to addition to modification order for threads. + * Definitions: + * pthread is the thread that performed the read that created the promise + * + * pread is the read that created the promise + * + * pwrite is either the first write to same location as pread by + * pthread that is sequenced after pread or the value read by the + * first read to the same lcoation as pread by pthread that is + * sequenced after pread.. + * + * 1. If tid=pthread, then we check what other threads are reachable + * through the mode order starting with pwrite. Those threads cannot + * perform a write that will resolve the promise due to modification + * order constraints. + * + * 2. If the tid is not pthread, we check whether pwrite can reach the + * action write through the modification order. If so, that thread + * cannot perform a future write that will resolve the promise due to + * modificatin order constraints. + * + * @parem tid The thread that either read from the model action + * write, or actually did the model action write. + * + * @parem write The ModelAction representing the relevant write. + */ + +void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) { + void * location = write->get_location(); + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + const ModelAction *act = promise->get_action(); + + //Is this promise on the same location? + if ( act->get_location() != location ) + continue; + + //same thread as the promise + if ( act->get_tid()==tid ) { + + //do we have a pwrite for the promise, if not, set it + if (promise->get_write() == NULL ) { + promise->set_write(write); + //The pwrite cannot happen before the promise + if (write->happens_before(act) && (write != act)) { + failed_promise = true; + return; + } + } + if (mo_graph->checkPromise(write, promise)) { + failed_promise = true; + return; + } + } + + //Don't do any lookups twice for the same thread + if (promise->has_sync_thread(tid)) + continue; + + if (mo_graph->checkReachable(promise->get_write(), write)) { + if (promise->increment_threads(tid)) { + failed_promise = true; + return; + } + } + } +} + +/** + * 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" @@ -1598,7 +1873,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() && ! curr->is_seqcst()) { + 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 */ @@ -1625,16 +1905,34 @@ 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; printf("---------------------------------------------------------------------\n"); printf("Trace:\n"); - + unsigned int hash=0; + for (it = list->begin(); it != list->end(); it++) { (*it)->print(); + hash=hash^(hash<<3)^((*it)->hash()); } + printf("HASH %u\n", hash); printf("---------------------------------------------------------------------\n"); } @@ -1756,7 +2054,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); @@ -1776,9 +2074,35 @@ bool ModelChecker::take_step() { if (!isfeasible()) return false; + if (params.bound != 0) { + if (priv->used_sequence_numbers > params.bound) { + return false; + } + } + 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;