model: add per-object action lists (obj_map)
authorBrian Norris <banorris@uci.edu>
Thu, 12 Jul 2012 22:33:14 +0000 (15:33 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 12 Jul 2012 22:36:49 +0000 (15:36 -0700)
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
model.h

index 9d07d41..85e1f84 100644 (file)
--- 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 (file)
--- 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;