X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b0ca05ea3c9009734d1196fad234b2aceaa8b001;hb=745b71256a4b96ddf4843c7f66b11d0cb3daa3cb;hp=4ae69665e4b84e3b04c2e852a120e85271c9c3c0;hpb=20c377062e4cfe1c12d517c059822229bacc8c20;p=model-checker.git diff --git a/model.cc b/model.cc index 4ae6966..b0ca05e 100644 --- a/model.cc +++ b/model.cc @@ -854,17 +854,19 @@ bool ModelChecker::process_read(ModelAction *curr) { Node *node = curr->get_node(); uint64_t value = VALUE_NONE; - bool updated = false; while (true) { + bool updated = false; switch (node->get_read_from_status()) { case READ_FROM_PAST: { const ModelAction *rf = node->get_read_from_past(); ASSERT(rf); mo_graph->startChanges(); - value = rf->get_value(); - check_recency(curr, rf); - bool r_status = r_modification_order(curr, rf); + + ASSERT(!is_infeasible()); + if (!check_recency(curr, rf)) + priv->too_many_reads = true; + updated = r_modification_order(curr, rf); if (is_infeasible() && node->increment_read_from()) { mo_graph->rollbackChanges(); @@ -872,11 +874,11 @@ bool ModelChecker::process_read(ModelAction *curr) continue; } + value = rf->get_value(); read_from(curr, rf); mo_graph->commitChanges(); mo_check_promises(curr, true); - updated |= r_status; break; } case READ_FROM_PROMISE: { @@ -1640,6 +1642,33 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { return lastread; } +template +bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const +{ + /* Need a different write/promise */ + if (other_rf->equals(rf)) + return false; + + /* Only look for "newer" writes/promises */ + if (!mo_graph->checkReachable(rf, other_rf)) + return false; + + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())]; + action_list_t::reverse_iterator rit = list->rbegin(); + ASSERT((*rit) == curr); + /* Skip past curr */ + rit++; + + /* Does this write/promise work for everyone? */ + for (int i = 0; i < params.maxreads; i++, rit++) { + ModelAction *act = *rit; + if (!act->may_read_from(other_rf)) + return false; + } + return true; +} + /** * Checks whether a thread has read from the same write for too many times * without seeing the effects of a later write. @@ -1650,86 +1679,57 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { * 3) that other write must have been in the reads_from set for maxreads times. * * If so, we decide that the execution is no longer feasible. + * + * @param curr The current action. Must be a read. + * @param rf The store from which we might read. + * @return True if the read should succeed; false otherwise */ -void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) +bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const { if (!params.maxreads) - return; + return true; //NOTE: Next check is just optimization, not really necessary.... - if (curr->get_node()->get_read_from_past_size() <= 1) - return; - /* Must make sure that execution is currently feasible... We could - * accidentally clear by rolling back */ - if (is_infeasible()) - return; + if (curr->get_node()->get_read_from_past_size() + + curr->get_node()->get_read_from_promise_size() <= 1) + return true; + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); - - //NOTE: this check seems left over from previous approach that added action to list late in the game...should be safe to remove - /* Skip checks */ - if ((int)thrd_lists->size() <= tid) - return; + ASSERT(tid < (int)thrd_lists->size()); action_list_t *list = &(*thrd_lists)[tid]; - action_list_t::reverse_iterator rit = list->rbegin(); + ASSERT((*rit) == curr); /* Skip past curr */ - for (; (*rit) != curr; rit++) - ; - /* go past curr now */ rit++; action_list_t::reverse_iterator ritcopy = rit; /* See if we have enough reads from the same value */ for (int count = 0; count < params.maxreads; ritcopy++, count++) { if (ritcopy == list->rend()) - return; + return true; ModelAction *act = *ritcopy; if (!act->is_read()) - return; - if (act->get_reads_from() != rf) - return; - if (act->get_node()->get_read_from_past_size() <= 1) - return; + return true; + if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf)) + return true; + if (act->get_reads_from() && !act->get_reads_from()->equals(rf)) + return true; + if (act->get_node()->get_read_from_past_size() + + act->get_node()->get_read_from_promise_size() <= 1) + return true; } for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) { - /* Get write */ const ModelAction *write = curr->get_node()->get_read_from_past(i); - - /* Need a different write */ - if (write == rf) - continue; - - //NOTE: SHOULD MAKE SURE write is MOd after rf - - /* Test to see whether this is a feasible write to read from */ - /** NOTE: all members of read-from set should be - * feasible, so we no longer check it here **/ - - ritcopy = rit; - - bool feasiblewrite = true; - /* now we need to see if this write works for everyone */ - - for (int loop = params.maxreads; loop > 0; loop--, ritcopy++) { - ModelAction *act = *ritcopy; - bool foundvalue = false; - for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) { - if (act->get_node()->get_read_from_past(j) == write) { - foundvalue = true; - break; - } - } - if (!foundvalue) { - feasiblewrite = false; - break; - } - } - if (feasiblewrite) { - priv->too_many_reads = true; - return; - } + if (should_read_instead(curr, rf, write)) + return false; /* liveness failure */ + } + for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) { + const Promise *promise = curr->get_node()->get_read_from_promise(i); + if (should_read_instead(curr, rf, promise)) + return false; /* liveness failure */ } + return true; } /**