From 236f53b4a7b4c07e9f60b662e059838f75b24171 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 21 Jun 2012 02:04:11 -0700 Subject: [PATCH] model: build up 'may_read_from' set Finally wire up the model-checker so that it builds the may_read_from set for every 'read' action. I think this is working OK, although I don't have much to really test it on yet. Also, improve comments to describe the process in check_current_action(). --- model.cc | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index e4d3016e..19d273de 100644 --- a/model.cc +++ b/model.cc @@ -240,11 +240,18 @@ void ModelChecker::check_current_action(void) tmp = node_stack->explore_action(curr); if (tmp) { - /* Discard duplicate ModelAction */ + /* Discard duplicate ModelAction; use action from NodeStack */ 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); } /* Assign 'creation' parent */ -- 2.34.1