From: Brian Norris <banorris@uci.edu>
Date: Mon, 28 May 2012 19:42:54 +0000 (-0700)
Subject: model: log the last action in each thread
X-Git-Tag: pldi2013~392^2~11
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=b33a4fd70ac89ed0bf5e276421dd52ee04679c94;p=model-checker.git

model: log the last action in each thread

The last action in each thread is needed for some model-checking computations.
This could be expanded to a full-fledged per-thread list if needed...
---

diff --git a/model.cc b/model.cc
index 42f412f..8656d6b 100644
--- a/model.cc
+++ b/model.cc
@@ -26,6 +26,7 @@ ModelChecker::ModelChecker()
 	action_trace(new action_list_t()),
 	thread_map(new std::map<int, class Thread *>),
 	obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
+	thrd_last_action(new std::vector<ModelAction *>(1)),
 	node_stack(new NodeStack()),
 	next_backtrack(NULL)
 {
@@ -40,6 +41,7 @@ ModelChecker::~ModelChecker()
 
 	delete obj_thrd_map;
 	delete action_trace;
+	delete thrd_last_action;
 	delete node_stack;
 	delete scheduler;
 }
@@ -225,6 +227,16 @@ void ModelChecker::check_current_action(void)
 	if (id_to_int(curr->get_tid()) >= (int)vec->size())
 		vec->resize(next_thread_id);
 	(*vec)[id_to_int(curr->get_tid())].push_back(curr);
+
+	(*thrd_last_action)[id_to_int(curr->get_tid())] = curr;
+}
+
+ModelAction * ModelChecker::get_last_action(thread_id_t tid)
+{
+	int nthreads = get_num_threads();
+	if ((int)thrd_last_action->size() < nthreads)
+		thrd_last_action->resize(nthreads);
+	return (*thrd_last_action)[id_to_int(tid)];
 }
 
 void ModelChecker::print_summary(void)
diff --git a/model.h b/model.h
index a1ab45e..1f22ebf 100644
--- a/model.h
+++ b/model.h
@@ -56,6 +56,8 @@ private:
 	ModelAction * get_next_backtrack();
 	void reset_to_initial_state();
 
+	ModelAction * get_last_action(thread_id_t tid);
+
 	void print_list(action_list_t *list);
 
 	ModelAction *current_action;
@@ -66,6 +68,7 @@ private:
 	action_list_t *action_trace;
 	std::map<int, class Thread *> *thread_map;
 	std::map<void *, std::vector<action_list_t> > *obj_thrd_map;
+	std::vector<ModelAction *> *thrd_last_action;
 	class NodeStack *node_stack;
 	ModelAction *next_backtrack;
 };