From eec79bb1863a2d706aa89505afd5f8159e144030 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 21 Jun 2012 01:59:01 -0700 Subject: [PATCH] model: add build_reads_from_past() function Add function that will build up the initial set of all past writes that a 'read' action may read from. --- model.cc | 39 +++++++++++++++++++++++++++++++++++++++ model.h | 1 + 2 files changed, 40 insertions(+) diff --git a/model.cc b/model.cc index 077cc53..e4d3016 100644 --- a/model.cc +++ b/model.cc @@ -6,6 +6,7 @@ #include "schedule.h" #include "snapshot-interface.h" #include "common.h" +#include "clockvector.h" #define INITIAL_THREAD_ID 0 @@ -299,6 +300,44 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) return parent; } +/** + * Build up an initial set of all past writes that this 'read' action may read + * from. This set is determined by the clock vector's "happens before" + * relationship. + * @param curr is the current ModelAction that we are exploring; it must be a + * 'read' operation. + */ +void ModelChecker::build_reads_from_past(ModelAction *curr) +{ + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + + ASSERT(curr->is_read()); + + for (i = 0; i < thrd_lists->size(); i++) { + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + + /* Only consider 'write' actions */ + if (!act->is_write()) + continue; + + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); + } + curr->get_node()->add_read_from(act); + + /* Include at most one act that "happens before" curr */ + if (act->happens_before(curr)) + break; + } + } +} + void ModelChecker::print_summary(void) { printf("\n"); diff --git a/model.h b/model.h index 8d79eb5..ab961f8 100644 --- a/model.h +++ b/model.h @@ -78,6 +78,7 @@ private: void add_action_to_lists(ModelAction *act); ModelAction * get_last_action(thread_id_t tid); ModelAction * get_parent_action(thread_id_t tid); + void build_reads_from_past(ModelAction *curr); void print_list(action_list_t *list); -- 2.34.1