X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=0c201fd381aa239eeaa060d6e46f22aae9023579;hp=bfb63e48ddd5d0d9ac0bc096b3604d3e6d9e640d;hb=32b70968c21a1d21a41010f00c5f9a82a9fbdbd1;hpb=963f325c5b5df37487e17c3a05f4d15efabb8870 diff --git a/model.cc b/model.cc index bfb63e48..0c201fd3 100644 --- a/model.cc +++ b/model.cc @@ -259,7 +259,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* The next node will try to satisfy a different set of promises. */ tid = next->get_tid(); node_stack->pop_restofstack(2); - } else if (nextnode->increment_read_from()) { + } else if (nextnode->increment_read_from_past()) { /* The next node will read from a different value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); @@ -842,40 +842,36 @@ ModelAction * ModelChecker::get_next_backtrack() } /** - * Processes a read or rmw model action. + * Processes a read model action. * @param curr is the read model action to process. - * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw. * @return True if processing this read updates the mo_graph. */ -bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) +bool ModelChecker::process_read(ModelAction *curr) { uint64_t value = VALUE_NONE; bool updated = false; while (true) { - const ModelAction *reads_from = curr->get_node()->get_read_from(); - if (reads_from != NULL) { + const ModelAction *rf = curr->get_node()->get_read_from_past(); + if (rf != NULL) { mo_graph->startChanges(); - value = reads_from->get_value(); - bool r_status = false; + value = rf->get_value(); - if (!second_part_of_rmw) { - check_recency(curr, reads_from); - r_status = r_modification_order(curr, reads_from); - } + check_recency(curr, rf); + bool r_status = r_modification_order(curr, rf); - if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) { + if (is_infeasible() && (curr->get_node()->increment_read_from_past() || curr->get_node()->increment_future_value())) { mo_graph->rollbackChanges(); priv->too_many_reads = false; continue; } - read_from(curr, reads_from); + read_from(curr, rf); mo_graph->commitChanges(); mo_check_promises(curr, true); updated |= r_status; - } else if (!second_part_of_rmw) { + } else { /* Read from future value */ struct future_value fv = curr->get_node()->get_future_value(); Promise *promise = new Promise(curr, fv); @@ -1437,7 +1433,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) if (process_thread_action(curr)) update_all = true; - if (act->is_read() && process_read(act, second_part_of_rmw)) + if (act->is_read() && !second_part_of_rmw && process_read(act)) update = true; if (act->is_write() && process_write(act)) @@ -1505,7 +1501,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr) if ((parnode && !parnode->backtrack_empty()) || !currnode->misc_empty() || - !currnode->read_from_empty() || + !currnode->read_from_past_empty() || !currnode->future_value_empty() || !currnode->promise_empty() || !currnode->relseq_break_empty()) { @@ -1613,7 +1609,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { if (params.maxreads != 0) { - if (curr->get_node()->get_read_from_size() <= 1) + 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 @@ -1646,12 +1642,12 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) if (act->get_reads_from() != rf) return; - if (act->get_node()->get_read_from_size() <= 1) + if (act->get_node()->get_read_from_past_size() <= 1) return; } - for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) { + 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_at(i); + const ModelAction *write = curr->get_node()->get_read_from_past(i); /* Need a different write */ if (write == rf) @@ -1669,8 +1665,8 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) for (int loop = count; loop > 0; loop--, rit++) { ModelAction *act = *rit; bool foundvalue = false; - for (int j = 0; j < act->get_node()->get_read_from_size(); j++) { - if (act->get_node()->get_read_from_at(j) == write) { + 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; } @@ -1770,7 +1766,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) if (prevrf) { if (!prevrf->equals(rf)) added = mo_graph->addEdge(prevrf, rf) || added; - } else if (!prevrf->equals(rf)) { + } else if (!prevrf_promise->equals(rf)) { added = mo_graph->addEdge(prevrf_promise, rf) || added; } } @@ -2635,7 +2631,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr) mo_graph->startChanges(); r_modification_order(curr, act); if (!is_infeasible()) - curr->get_node()->add_read_from(act); + curr->get_node()->add_read_from_past(act); mo_graph->rollbackChanges(); } @@ -2662,7 +2658,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr) } /* We may find no valid may-read-from only if the execution is doomed */ - if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) { + if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) { priv->no_valid_reads = true; set_assert(); } @@ -2670,9 +2666,9 @@ void ModelChecker::build_may_read_from(ModelAction *curr) if (DBG_ENABLED()) { model_print("Reached read action:\n"); curr->print(); - model_print("Printing may_read_from\n"); - curr->get_node()->print_may_read_from(); - model_print("End printing may_read_from\n"); + model_print("Printing read_from_past\n"); + curr->get_node()->print_read_from_past(); + model_print("End printing read_from_past\n"); } }