From 61d1e3ae29b690f69cf77c5a6f836fb36507a694 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 27 Feb 2013 16:36:24 -0800 Subject: [PATCH] model: don't call process_read() for 2nd half of RMW/RMWC We don't need to call process_read() for the second half of an RMW or RMWC ModelAction. Anyway, it does next-to-nothing when 'second_part_of_rmw' is true. --- model.cc | 18 +++++++----------- model.h | 2 +- 2 files changed, 8 insertions(+), 12 deletions(-) diff --git a/model.cc b/model.cc index 152e36ec..417cbc1c 100644 --- a/model.cc +++ b/model.cc @@ -842,12 +842,11 @@ 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; @@ -857,14 +856,11 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) mo_graph->startChanges(); value = reads_from->get_value(); - bool r_status = false; - if (!second_part_of_rmw) { - check_recency(curr, reads_from); - r_status = r_modification_order(curr, reads_from); - } + check_recency(curr, reads_from); + bool 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())) { + if (is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) { mo_graph->rollbackChanges(); priv->too_many_reads = false; continue; @@ -875,7 +871,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) 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)) diff --git a/model.h b/model.h index 783f7a66..9e0b34ba 100644 --- a/model.h +++ b/model.h @@ -155,7 +155,7 @@ private: bool next_execution(); ModelAction * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); - bool process_read(ModelAction *curr, bool second_part_of_rmw); + bool process_read(ModelAction *curr); bool process_write(ModelAction *curr); bool process_fence(ModelAction *curr); bool process_mutex(ModelAction *curr); -- 2.34.1