From 22cfbcda627e74a3a8134bfcde03793e18c47681 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 14 Sep 2012 12:43:25 -0700 Subject: [PATCH] model: fixup happens_before/reflexivity, add 'curr' to lists earlier Some code under 'check_current_action' assumes that the current action is not added to the ModelChecker trace/list data structures yet. However, some features I need to add will require the current action to be in these data structures already. So there are a few spots I need to fixup so that the code can handle "happens_before" reflexivity properly. This commit moves the "add_action_to_lists()" call as well as fixes up reflexivity. --- model.cc | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/model.cc b/model.cc index 954c07d..acd2079 100644 --- a/model.cc +++ b/model.cc @@ -420,6 +420,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) break; } + /* Add current action to lists before work_queue loop */ + if (!second_part_of_rmw) + add_action_to_lists(curr); + work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); while (!work_queue.empty()) { @@ -451,10 +455,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) } } - /* Add action to list. */ - if (!second_part_of_rmw) - add_action_to_lists(curr); - check_curr_backtracking(curr); set_backtracking(curr); @@ -648,8 +648,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) { + /* + * Include at most one act per-thread that "happens + * before" curr. Don't consider reflexively. + */ + if (act->happens_before(curr) && act != curr) { if (act->is_write()) { if (rf != act && act != curr) { mo_graph->addEdge(act, rf); @@ -770,8 +773,12 @@ bool ModelChecker::w_modification_order(ModelAction *curr) for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) { + /* + * Include at most one act per-thread that "happens + * before" curr. Only consider reflexively if curr is + * RMW. + */ + if (act->happens_before(curr) && (act != curr || curr->is_rmw())) { /* * Note: if act is RMW, just add edge: * act --mo--> curr -- 2.34.1