From: Brian Demsky <bdemsky@uci.edu>
Date: Tue, 18 Sep 2012 08:15:06 +0000 (-0700)
Subject: more changes towards locks
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=39489a1523a5109378d374632930499742762f32

more changes towards locks
---

diff --git a/action.cc b/action.cc
index 1e28264f..2d9186d2 100644
--- a/action.cc
+++ b/action.cc
@@ -27,6 +27,14 @@ ModelAction::~ModelAction()
 		delete cv;
 }
 
+bool ModelAction::is_success_lock() const {
+	return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
+}
+
+bool ModelAction::is_failed_trylock() const {
+	return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
+}
+
 bool ModelAction::is_read() const
 {
 	return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
diff --git a/action.h b/action.h
index 0e3f3d57..75386098 100644
--- a/action.h
+++ b/action.h
@@ -24,6 +24,8 @@ using std::memory_order_seq_cst;
 		hence by iteself does not indicate no value. */
 
 #define VALUE_NONE 1234567890
+#define VALUE_TRYSUCCESS 1
+#define VALUE_TRYFAILED 0
 
 /** @brief Represents an action type, identifying one of several types of
  * ModelAction */
@@ -70,6 +72,8 @@ public:
 	Node * get_node() const { return node; }
 	void set_node(Node *n) { node = n; }
 
+	bool is_success_lock() const;
+	bool is_failed_trylock() const;
 	bool is_read() const;
 	bool is_write() const;
 	bool is_rmwr() const;
diff --git a/model.cc b/model.cc
index ede3797b..00749228 100644
--- a/model.cc
+++ b/model.cc
@@ -33,6 +33,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
 	thrd_last_action(new std::vector<ModelAction *>(1)),
 	node_stack(new NodeStack()),
+	is_enabled(NULL),
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
 	too_many_reads(false),
@@ -52,6 +53,8 @@ ModelChecker::~ModelChecker()
 	for (int i = 0; i < get_num_threads(); i++)
 		delete thread_map->get(i);
 	delete thread_map;
+	if (is_enabled)
+		free(is_enabled);
 
 	delete obj_thrd_map;
 	delete obj_map;
@@ -86,7 +89,13 @@ void ModelChecker::reset_to_initial_state()
 /** @returns a thread ID for a new Thread */
 thread_id_t ModelChecker::get_next_id()
 {
-	return priv->next_thread_id++;
+	thread_id_t newid=priv->next_thread_id++;
+	bool * tmp=(bool *) malloc((newid+1)*sizeof(bool));
+	memcpy(tmp, is_enabled, newid*sizeof(bool));
+	tmp[newid]=true;
+	free(is_enabled);
+	is_enabled=tmp;
+	return newid;
 }
 
 /** @returns the number of user threads created during this execution */
@@ -197,21 +206,33 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
 	action_type type = act->get_type();
 
-	switch (type) {
-		case ATOMIC_READ:
-		case ATOMIC_WRITE:
-		case ATOMIC_RMW:
-			break;
-		default:
-			return NULL;
-	}
-	/* linear search: from most recent to oldest */
-	action_list_t *list = obj_map->get_safe_ptr(act->get_location());
-	action_list_t::reverse_iterator rit;
-	for (rit = list->rbegin(); rit != list->rend(); rit++) {
-		ModelAction *prev = *rit;
-		if (act->is_synchronizing(prev))
-			return prev;
+	if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==ATOMIC_RMW) {
+		/* linear search: from most recent to oldest */
+		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *prev = *rit;
+			if (act->is_synchronizing(prev))
+				return prev;
+		}
+	} else if (type==ATOMIC_LOCK||type==ATOMIC_TRYLOCK) {
+		/* linear search: from most recent to oldest */
+		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *prev = *rit;
+			if (prev->is_success_lock())
+				return prev;
+		}
+	} else if (type==ATOMIC_UNLOCK) {
+		/* linear search: from most recent to oldest */
+		action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *prev = *rit;
+			if (prev->is_failed_trylock())
+				return prev;
+		}
 	}
 	return NULL;
 }
diff --git a/model.h b/model.h
index 4fc32c6d..54f30268 100644
--- a/model.h
+++ b/model.h
@@ -177,6 +177,8 @@ private:
 	 * together for efficiency and maintainability. */
 	struct model_snapshot_members *priv;
 
+	bool * is_enabled;
+
 	/**
 	 * @brief The modification order graph
 	 *