From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 19 Sep 2012 07:35:54 +0000 (-0700)
Subject: fix
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=bd893aac350f125dc990f0ccd32b8e3cf133e2fb;hp=3bab2ac6bca956b302a62d2ee60e7d2b48e8258b;p=c11tester.git

fix
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Conflicts:
	model.cc
---

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/mutex.cc b/mutex.cc
new file mode 100644
index 00000000..b31b20a8
--- /dev/null
+++ b/mutex.cc
@@ -0,0 +1,25 @@
+#include "mutex.h"
+#include "model.h"
+
+
+namespace std {
+mutex::mutex() :
+	owner(0), islocked(false)
+{
+
+}
+	
+void mutex::lock() {
+  model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
+}
+	
+bool mutex::try_lock() {
+  model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
+  return thread_current()->get_return_value();
+}
+
+void mutex::unlock() {
+  model->switch_to_master(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this));
+}
+
+}
diff --git a/mutex.h b/mutex.h
new file mode 100644
index 00000000..1c6c3f36
--- /dev/null
+++ b/mutex.h
@@ -0,0 +1,18 @@
+#ifndef MUTEX_H
+#define MUTEX_H
+#include "threads.h"
+
+namespace std {
+	class mutex {
+	public:
+		mutex();
+		~mutex();
+		void lock();
+		bool try_lock();
+		void unlock();
+	private:
+		thread_id_t owner;
+		bool islocked;
+	};
+}
+#endif
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();