From: Brian Norris <banorris@uci.edu>
Date: Thu, 12 Jul 2012 22:33:14 +0000 (-0700)
Subject: model: add per-object action lists (obj_map)
X-Git-Tag: pldi2013~360
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=471e92c4bc5de8629d044a61eea5e1ff0670daad

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.
---

diff --git a/model.cc b/model.cc
index 9d07d41..85e1f84 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 941601b..5d74b84 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;