X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=6739d2c85ee2ca51dd3963c471c811e12f0711b3;hb=ae1340cbd7d2f75d76a4199597f454290badcc8b;hp=ede2bcc840d8710ae00e3d021accadb6ef8e0698;hpb=523dbecc6fc18e58918a1f36860be5eb0ab42ce2;p=model-checker.git diff --git a/model.cc b/model.cc index ede2bcc..6739d2c 100644 --- a/model.cc +++ b/model.cc @@ -721,7 +721,6 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) r_status = r_modification_order(curr, reads_from); } - if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) { mo_graph->rollbackChanges(); priv->too_many_reads = false; @@ -736,9 +735,13 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } else if (!second_part_of_rmw) { /* Read from future value */ struct future_value fv = curr->get_node()->get_future_value(); + Promise *promise = new Promise(curr, fv); value = fv.value; - curr->set_read_from(NULL); - promises->push_back(new Promise(curr, fv)); + curr->set_read_from_promise(promise); + promises->push_back(promise); + mo_graph->startChanges(); + updated = r_modification_order(curr, promise); + mo_graph->commitChanges(); } get_thread(curr)->set_return_value(value); return updated; @@ -855,10 +858,22 @@ bool ModelChecker::process_mutex(ModelAction *curr) void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader) { /* Do more ambitious checks now that mo is more complete */ - if (mo_may_allow(writer, reader) && - reader->get_node()->add_future_value(writer, - writer->get_seq_number() + params.maxfuturedelay)) - set_latest_backtrack(reader); + if (mo_may_allow(writer, reader)) { + Node *node = reader->get_node(); + + /* Find an ancestor thread which exists at the time of the reader */ + Thread *write_thread = get_thread(writer); + while (id_to_int(write_thread->get_id()) >= node->get_num_threads()) + write_thread = write_thread->get_parent(); + + struct future_value fv = { + writer->get_value(), + writer->get_seq_number() + params.maxfuturedelay, + write_thread->get_id(), + }; + if (node->add_future_value(fv)) + set_latest_backtrack(reader); + } } /** @@ -955,6 +970,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr) case THREAD_CREATE: { Thread *th = curr->get_thread_operand(); th->set_creation(curr); + /* Promises can be satisfied by children */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(curr->get_tid())) + promise->add_thread(th->get_id()); + } break; } case THREAD_JOIN: { @@ -971,6 +992,13 @@ bool ModelChecker::process_thread_action(ModelAction *curr) scheduler->wake(get_thread(act)); } th->complete(); + /* Completed thread can't satisfy promises */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(th->get_id())) + if (promise->eliminate_thread(th->get_id())) + priv->failed_promise = true; + } updated = true; /* trigger rel-seq checks */ break; } @@ -1279,8 +1307,14 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) if (act->is_read()) { const ModelAction *rf = act->get_reads_from(); - if (rf != NULL && r_modification_order(act, rf)) - updated = true; + const Promise *promise = act->get_reads_from_promise(); + if (rf) { + if (r_modification_order(act, rf)) + updated = true; + } else if (promise) { + if (r_modification_order(act, promise)) + updated = true; + } } if (act->is_write()) { if (w_modification_order(act)) @@ -1347,8 +1381,6 @@ void ModelChecker::print_infeasibility(const char *prefix) const { char buf[100]; char *ptr = buf; - if (mo_graph->checkForRMWViolation()) - ptr += sprintf(ptr, "[RMW atomicity]"); if (mo_graph->checkForCycles()) ptr += sprintf(ptr, "[mo cycle]"); if (priv->failed_promise) @@ -1382,21 +1414,10 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const */ bool ModelChecker::is_infeasible() const { - return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW(); -} - -/** - * Check If the current partial trace is infeasible, while ignoring - * infeasibility related to 2 RMW's reading from the same store. It does not - * check end-of-execution feasibility. - * @see ModelChecker::is_infeasible - * @return whether the current partial trace is infeasible, ignoring multiple - * RMWs reading from the same store. - * */ -bool ModelChecker::is_infeasible_ignoreRMW() const -{ - return mo_graph->checkForCycles() || priv->failed_promise || - priv->too_many_reads || priv->bad_synchronization || + return mo_graph->checkForCycles() || + priv->failed_promise || + priv->too_many_reads || + priv->bad_synchronization || promises_expired(); } @@ -1509,7 +1530,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) * read. * * Basic idea is the following: Go through each other thread and find - * the lastest action that happened before our read. Two cases: + * the last action that happened before our read. Two cases: * * (1) The action is a write => that write must either occur before * the write we read from or be the write we read from. @@ -1518,10 +1539,11 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) * must occur before the write we read from or be the same write. * * @param curr The current action. Must be a read. - * @param rf The action that curr reads from. Must be a write. + * @param rf The ModelAction or Promise that curr reads from. Must be a write. * @return True if modification order edges were added; false otherwise */ -bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf) +template +bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) { std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; @@ -1549,26 +1571,23 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - if (act->is_write() && act != rf && act != curr) { + if (act->is_write() && !act->equals(rf) && act != curr) { /* C++, Section 29.3 statement 5 */ if (curr->is_seqcst() && last_sc_fence_thread_local && *act < *last_sc_fence_thread_local) { - mo_graph->addEdge(act, rf); - added = true; + added = mo_graph->addEdge(act, rf) || added; break; } /* C++, Section 29.3 statement 4 */ else if (act->is_seqcst() && last_sc_fence_local && *act < *last_sc_fence_local) { - mo_graph->addEdge(act, rf); - added = true; + added = mo_graph->addEdge(act, rf) || added; break; } /* C++, Section 29.3 statement 6 */ else if (last_sc_fence_thread_before && *act < *last_sc_fence_thread_before) { - mo_graph->addEdge(act, rf); - added = true; + added = mo_graph->addEdge(act, rf) || added; break; } } @@ -1579,9 +1598,8 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf */ if (act->happens_before(curr) && act != curr) { if (act->is_write()) { - if (rf != act) { - mo_graph->addEdge(act, rf); - added = true; + if (!act->equals(rf)) { + added = mo_graph->addEdge(act, rf) || added; } } else { const ModelAction *prevreadfrom = act->get_reads_from(); @@ -1589,9 +1607,8 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf if (prevreadfrom == NULL) continue; - if (rf != prevreadfrom) { - mo_graph->addEdge(prevreadfrom, rf); - added = true; + if (!prevreadfrom->equals(rf)) { + added = mo_graph->addEdge(prevreadfrom, rf) || added; } } break; @@ -1700,8 +1717,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) so we are initialized. */ ModelAction *last_seq_cst = get_last_seq_cst_write(curr); if (last_seq_cst != NULL) { - mo_graph->addEdge(last_seq_cst, curr); - added = true; + added = mo_graph->addEdge(last_seq_cst, curr) || added; } } @@ -1744,8 +1760,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) /* C++, Section 29.3 statement 7 */ if (last_sc_fence_thread_before && act->is_write() && *act < *last_sc_fence_thread_before) { - mo_graph->addEdge(act, curr); - added = true; + added = mo_graph->addEdge(act, curr) || added; break; } @@ -1761,14 +1776,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * readfrom(act) --mo--> act */ if (act->is_write()) - mo_graph->addEdge(act, curr); + added = mo_graph->addEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going if (act->get_reads_from() == NULL) continue; - mo_graph->addEdge(act->get_reads_from(), curr); + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } - added = true; break; } else if (act->is_read() && !act->could_synchronize_with(curr) && !act->same_thread(curr)) { @@ -1785,10 +1799,10 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (thin_air_constraint_may_allow(curr, act)) { - if (!is_infeasible() || - (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) { + if (!is_infeasible()) futurevalues->push_back(PendingFutureValue(curr, act)); - } + else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) + add_future_value(curr, act); } } } @@ -2327,7 +2341,7 @@ 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); + delete promise; promises->erase(promises->begin() + promise_index); actions_to_check.push_back(read); @@ -2462,7 +2476,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, } // Don't do any lookups twice for the same thread - if (promise->thread_is_eliminated(tid)) + if (!promise->thread_is_available(tid)) continue; if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) { @@ -2635,7 +2649,6 @@ void ModelChecker::dumpGraph(char *filename) const void ModelChecker::print_summary() const { #if SUPPORT_MOD_ORDER_DUMP - scheduler->print(); char buffername[100]; sprintf(buffername, "exec%04u", stats.num_total); mo_graph->dumpGraphToFile(buffername);