From: Brian Norris Date: Tue, 18 Sep 2012 23:16:38 +0000 (-0700) Subject: model: refactor ModelChecker::initialize_curr_action X-Git-Tag: pldi2013~177^2^2~7 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=ed5684e598c27e458bde4976848d48a0cd247dbb model: refactor ModelChecker::initialize_curr_action Rewrite some logic for simplification. Just refactorization. --- diff --git a/model.cc b/model.cc index f2d4eb1..20d0880 100644 --- a/model.cc +++ b/model.cc @@ -335,39 +335,40 @@ bool ModelChecker::process_write(ModelAction *curr) ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) { + ModelAction *newcurr; + if (curr->is_rmwc() || curr->is_rmw()) { - ModelAction *tmp = process_rmw(curr); + newcurr = process_rmw(curr); + delete curr; + compute_promises(newcurr); + return newcurr; + } + + newcurr = node_stack->explore_action(curr); + if (newcurr) { + /* First restore type and order in case of RMW operation */ + if (curr->is_rmwr()) + newcurr->copy_typeandorder(curr); + + /* Discard duplicate ModelAction; use action from NodeStack */ delete curr; - curr = tmp; - compute_promises(curr); + + /* If we have diverged, we need to reset the clock vector. */ + if (diverge == NULL) + newcurr->create_cv(get_parent_action(newcurr->get_tid())); } else { - ModelAction *tmp = node_stack->explore_action(curr); - if (tmp) { - /* Discard duplicate ModelAction; use action from NodeStack */ - /* First restore type and order in case of RMW operation */ - if (curr->is_rmwr()) - tmp->copy_typeandorder(curr); - - /* If we have diverged, we need to reset the clock vector. */ - if (diverge == NULL) - tmp->create_cv(get_parent_action(tmp->get_tid())); - - delete curr; - curr = tmp; - } else { - /* - * Perform one-time actions when pushing new ModelAction onto - * NodeStack - */ - curr->create_cv(get_parent_action(curr->get_tid())); - /* Build may_read_from set */ - if (curr->is_read()) - build_reads_from_past(curr); - if (curr->is_write()) - compute_promises(curr); - } + newcurr = curr; + /* + * Perform one-time actions when pushing new ModelAction onto + * NodeStack + */ + curr->create_cv(get_parent_action(curr->get_tid())); + if (curr->is_read()) + build_reads_from_past(curr); + if (curr->is_write()) + compute_promises(curr); } - return curr; + return newcurr; } /**