X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=691ab832519d11dff2515dfe313884da05ef7382;hb=fbacb5f41ada96e7b539ccc41deccb1a7e1a1ba8;hp=1ecc48e395ffbe0a13b00b5dbeba02985de33ec2;hpb=72524dae1144e6fe437c8317f8f718e534ccfe0f;p=model-checker.git diff --git a/model.cc b/model.cc index 1ecc48e..691ab83 100644 --- a/model.cc +++ b/model.cc @@ -735,10 +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_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; @@ -1304,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)) @@ -1521,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. @@ -1530,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; @@ -1561,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; } } @@ -1591,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(); @@ -1601,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; @@ -1712,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; } } @@ -1756,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; } @@ -1773,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)) { @@ -1806,6 +1808,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr) } } + /* + * All compatible, thread-exclusive promises must be ordered after any + * concrete stores to the same thread, or else they can be merged with + * this store later + */ + for (unsigned int i = 0; i < promises->size(); i++) + if ((*promises)[i]->is_compatible_exclusive(curr)) + added = mo_graph->addEdge(curr, (*promises)[i]) || added; + return added; } @@ -2339,7 +2350,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); @@ -2647,7 +2658,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);