From 471e92c4bc5de8629d044a61eea5e1ff0670daad Mon Sep 17 00:00:00 2001 From: Brian Norris <banorris@uci.edu> Date: Thu, 12 Jul 2012 15:33:14 -0700 Subject: [PATCH] model: add per-object action lists (obj_map) This object list will map objects (i.e., memory locations) to traces of all actions performed on the respective objects. This will be used for some seq_cst and backtracking-conflict computations to reduce the space we have to search. --- model.cc | 4 ++++ model.h | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/model.cc b/model.cc index 9d07d416..85e1f849 100644 --- a/model.cc +++ b/model.cc @@ -27,6 +27,7 @@ ModelChecker::ModelChecker() nextThread(THREAD_ID_T_NONE), action_trace(new action_list_t()), thread_map(new std::map<int, Thread *>), + obj_map(new std::map<const void *, action_list_t>()), obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()), thrd_last_action(new std::vector<ModelAction *>(1)), node_stack(new NodeStack()), @@ -43,6 +44,7 @@ ModelChecker::~ModelChecker() delete thread_map; delete obj_thrd_map; + delete obj_map; delete action_trace; delete thrd_last_action; delete node_stack; @@ -297,6 +299,8 @@ void ModelChecker::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); action_trace->push_back(act); + (*obj_map)[act->get_location()].push_back(act); + std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()]; if (tid >= (int)vec->size()) vec->resize(next_thread_id); diff --git a/model.h b/model.h index 941601b6..5d74b844 100644 --- a/model.h +++ b/model.h @@ -89,6 +89,11 @@ private: ucontext_t *system_context; action_list_t *action_trace; std::map<int, Thread *> *thread_map; + + /** Per-object list of actions. Maps an object (i.e., memory location) + * to a trace of all actions performed on the object. */ + std::map<const void *, action_list_t> *obj_map; + std::map<void *, std::vector<action_list_t> > *obj_thrd_map; std::vector<ModelAction *> *thrd_last_action; NodeStack *node_stack; -- 2.34.1