X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b916d8cf3e2c3d169c11e361715c46407ace3cd5;hb=38b76fe373e538f275cb3a864a6e919664dc9bda;hp=326358ea79c8b80ed0a356854cef43288c0ec304;hpb=cf4cc8a444d3c85367b9aa15b91b2829220e2edf;p=model-checker.git diff --git a/model.cc b/model.cc index 326358e..b916d8c 100644 --- a/model.cc +++ b/model.cc @@ -52,7 +52,7 @@ ModelChecker::ModelChecker(struct model_params params) : /** @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; @@ -95,7 +95,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; } @@ -199,7 +199,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"); @@ -377,6 +377,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 */ @@ -474,6 +476,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; } @@ -526,7 +530,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } case THREAD_START: { - check_promises(NULL, curr->get_cv()); + check_promises(curr->get_tid(), NULL, curr->get_cv()); break; } default: @@ -1176,7 +1180,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const +bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const { /* Only check for release sequences if there are no cycles */ if (mo_graph->checkForCycles()) @@ -1298,14 +1302,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * @param act The 'acquire' action that may read from a release sequence * @param release_heads A pass-by-reference return parameter. Will be filled * with the head(s) of the release sequence(s), if they exists with certainty. - * @see ModelChecker::release_seq_head + * @see ModelChecker::release_seq_heads */ 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_head(rf, release_heads); - if (!complete) { + + if (!release_seq_heads(rf, release_heads)) { /* add act to 'lazy checking' list */ pending_acq_rel_seq->push_back(act); } @@ -1340,7 +1343,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_head(rf, &release_heads); + complete = release_seq_heads(rf, &release_heads); 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])) @@ -1486,6 +1489,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; + std::vector threads_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; @@ -1503,13 +1507,18 @@ 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++; } + for(unsigned int i=0;isize(); 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 +1560,40 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) } } +/** Checks promises in response to change in ClockVector Threads. */ +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; + + if ( act->get_tid()==tid) { + if (promise->get_write() == NULL ) { + promise->set_write(write); + } + 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; + } + } + } +} + /** * 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"