X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=2260431ab908973fe5b4233e9e15ceeb8be4ca2f;hp=e3d9203eea60ec53010d67bb87da20331cfbf642;hb=2de6c82d6d7e6af2267636ec55f7e81d2a799a78;hpb=a27eec056d90e248a071bea6912e5ab09dea8242 diff --git a/model.cc b/model.cc index e3d9203..2260431 100644 --- a/model.cc +++ b/model.cc @@ -34,7 +34,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - pending_acq_rel_seq(new std::vector()), + pending_rel_seqs(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -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; @@ -65,7 +65,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 +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; } @@ -207,8 +207,8 @@ 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()) print_summary(); @@ -236,7 +236,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; @@ -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: @@ -756,7 +760,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 +1114,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 @@ -1170,13 +1174,19 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @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 +1215,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 +1245,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) @@ -1277,14 +1290,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 +1323,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 +1350,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::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 +1364,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 +1391,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 +1512,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 +1530,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 +1571,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 +1587,69 @@ 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); + } + 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"