From 160c85908774dfffc19dc1b02f4f845a14c056af Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 17 Sep 2012 22:15:35 -0700
Subject: [PATCH] start towards adding support for mutexes

---
 Makefile     |  2 +-
 action.h     |  5 ++++-
 model.cc     |  2 +-
 nodestack.cc | 16 ++++++++++++----
 nodestack.h  |  5 +++--
 5 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/Makefile b/Makefile
index 53b0331f..a732cb76 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ include common.mk
 OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \
 	  nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
 	  datarace.o impatomic.o cmodelint.o \
-	  snapshot.o malloc.o mymemory.o common.o
+	  snapshot.o malloc.o mymemory.o common.o mutex.o
 
 CPPFLAGS += -Iinclude -I. -rdynamic
 LDFLAGS = -ldl -lrt
diff --git a/action.h b/action.h
index 9fa7a91c..0e3f3d57 100644
--- a/action.h
+++ b/action.h
@@ -40,7 +40,10 @@ typedef enum action_type {
 	ATOMIC_RMWC,          /**< Convert an atomic RMW action into a READ */
 	ATOMIC_INIT,          /**< Initialization of an atomic object (e.g.,
 	                       *   atomic_init()) */
-	ATOMIC_FENCE
+	ATOMIC_FENCE,
+	ATOMIC_LOCK,
+	ATOMIC_TRYLOCK,
+	ATOMIC_UNLOCK
 } action_type_t;
 
 /* Forward declaration */
diff --git a/model.cc b/model.cc
index 954c07dd..ede3797b 100644
--- a/model.cc
+++ b/model.cc
@@ -358,7 +358,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		curr = tmp;
 		compute_promises(curr);
 	} else {
-		ModelAction *tmp = node_stack->explore_action(curr);
+		ModelAction *tmp = node_stack->explore_action(curr, NULL);
 		if (tmp) {
 			/* Discard duplicate ModelAction; use action from NodeStack */
 			/* First restore type and order in case of RMW operation */
diff --git a/nodestack.cc b/nodestack.cc
index 431baafb..69f0b5f5 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -17,7 +17,7 @@
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */
-Node::Node(ModelAction *act, Node *par, int nthreads)
+Node::Node(ModelAction *act, Node *par, int nthreads, bool *enabled)
 	: action(act),
 	parent(par),
 	num_threads(nthreads),
@@ -31,6 +31,12 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
 {
 	if (act)
 		act->set_node(this);
+	enabled_array=(bool *)MYMALLOC(sizeof(bool)*num_threads);
+	if (enabled)
+		memcpy(enabled_array, enabled, sizeof(bool)*num_threads);
+	else 
+		for(int i=0;i<num_threads;i++)
+			enabled_array[i]=false;
 }
 
 /** @brief Node desctructor */
@@ -38,6 +44,7 @@ Node::~Node()
 {
 	if (action)
 		delete action;
+	MYFREE(enabled_array);
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
@@ -212,7 +219,8 @@ thread_id_t Node::get_next_backtrack()
 
 bool Node::is_enabled(Thread *t)
 {
-	return id_to_int(t->get_id()) < num_threads;
+	int thread_id=id_to_int(t->get_id());
+	return thread_id < num_threads && enabled_array[thread_id];
 }
 
 /**
@@ -324,7 +332,7 @@ void NodeStack::print()
 	printf("............................................\n");
 }
 
-ModelAction * NodeStack::explore_action(ModelAction *act)
+ModelAction * NodeStack::explore_action(ModelAction *act, bool * enabled)
 {
 	DBG();
 
@@ -339,7 +347,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
 	/* Record action */
 	get_head()->explore_child(act);
-	node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
+	node_list.push_back(new Node(act, get_head(), model->get_num_threads(), enabled));
 	total_nodes++;
 	iter++;
 	return NULL;
diff --git a/nodestack.h b/nodestack.h
index 6c977949..6cd8cfd3 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -44,7 +44,7 @@ struct future_value {
  */
 class Node {
 public:
-	Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1);
+	Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, bool *enabled_array = NULL);
 	~Node();
 	/* return true = thread choice has already been explored */
 	bool has_been_explored(thread_id_t tid);
@@ -93,6 +93,7 @@ private:
 	std::vector< bool, MyAlloc<bool> > explored_children;
 	std::vector< bool, MyAlloc<bool> > backtrack;
 	int numBacktracks;
+	bool *enabled_array;
 
 	/** The set of ModelActions that this the action at this Node may read
 	 *  from. Only meaningful if this Node represents a 'read' action. */
@@ -119,7 +120,7 @@ class NodeStack {
 public:
 	NodeStack();
 	~NodeStack();
-	ModelAction * explore_action(ModelAction *act);
+	ModelAction * explore_action(ModelAction *act, bool * enabled);
 	Node * get_head();
 	Node * get_next();
 	void reset_execution();
-- 
2.34.1