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 9d07d416307f143a1f4fcf12692d4042e6dd2e04..85e1f849cc7a42f7c10139321b360414b818b102 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 941601b61fba027fe9b4a3dc366eef420aa561e1..5d74b8443543557b022b4fca51cf6cd64296c2e6 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;