From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 12 Oct 2012 06:56:12 +0000 (-0700)
Subject: forgot to add two files...
X-Git-Tag: pldi2013~51
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=55eb20c50ec656d385fb6e94c01aea55e9514917

forgot to add two files...
bug fixes...
---

diff --git a/action.cc b/action.cc
index 5705892..16f2327 100644
--- a/action.cc
+++ b/action.cc
@@ -187,6 +187,19 @@ bool ModelAction::is_seqcst() const
 
 bool ModelAction::same_var(const ModelAction *act) const
 {
+	if ( act->is_wait() || is_wait() ) {
+		if ( act->is_wait() && is_wait() ) {
+			if ( ((void *)value) == ((void *)act->value) )
+				return true;
+		} else if ( is_wait() ) {
+			if ( ((void *)value) == act->location )
+				return true;
+		} else if ( act->is_wait() ) {
+			if ( location == ((void *)act->value) )
+				return true;
+		}
+	}
+
 	return location == act->location;
 }
 
@@ -244,6 +257,27 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const
 	if (is_read() && is_acquire() && act->could_be_write() && act->is_release())
 		return true;
 
+	//lock just released...we can grab lock
+	if ((is_lock() ||is_trylock()) && (act->is_unlock()||act->is_wait()))
+		return true;
+
+	//lock just acquired...we can fail to grab lock
+	if (is_trylock() && act->is_success_lock())
+		return true;
+
+	//other thread stalling on lock...we can release lock
+	if (is_unlock() && (act->is_trylock()||act->is_lock()))
+		return true;
+
+	if (is_trylock() && (act->is_unlock()||act->is_wait()))
+		return true;
+
+	if ( is_notify() && act->is_wait() )
+		return true;
+
+	if ( is_wait() && act->is_notify() )
+		return true;
+
 	// Otherwise handle by reads_from relation
 	return false;
 }
@@ -398,6 +432,15 @@ void ModelAction::print() const
 	case ATOMIC_TRYLOCK:
 		type_str = "trylock";
 		break;
+	case ATOMIC_WAIT:
+		type_str = "wait";
+		break;
+	case ATOMIC_NOTIFY_ONE:
+		type_str = "notify one";
+		break;
+	case ATOMIC_NOTIFY_ALL:
+		type_str = "notify all";
+		break;
 	default:
 		type_str = "unknown type";
 	}
diff --git a/conditionvariable.cc b/conditionvariable.cc
new file mode 100644
index 0000000..5bd0beb
--- /dev/null
+++ b/conditionvariable.cc
@@ -0,0 +1,26 @@
+#include <mutex>
+#include "model.h"
+#include "conditionvariable.h"
+
+
+namespace std {
+
+condition_variable::condition_variable() {
+		
+}
+
+void condition_variable::notify_one() {
+	model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this));
+}
+
+void condition_variable::notify_all() {
+	model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this));
+}
+
+void condition_variable::wait(mutex& lock) {
+	model->switch_to_master(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock));
+	//relock as a second action
+	lock.lock();
+}
+}
+
diff --git a/conditionvariable.h b/conditionvariable.h
new file mode 100644
index 0000000..d1db7ff
--- /dev/null
+++ b/conditionvariable.h
@@ -0,0 +1,23 @@
+#ifndef CONDITIONVARIABLE_H
+#define CONDITIONVARIABLE_H
+
+namespace std {
+	class mutex;
+
+	struct condition_variable_state {
+		int reserved;
+	};
+
+	class condition_variable {
+	public:
+		condition_variable();
+		~condition_variable();
+		void notify_one();
+		void notify_all();
+		void wait(mutex& lock);
+		
+	private:
+		struct condition_variable_state state;
+	};
+}
+#endif
diff --git a/model.cc b/model.cc
index 101a5f0..2aaa1c2 100644
--- a/model.cc
+++ b/model.cc
@@ -498,8 +498,17 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  * @return True if synchronization was updated; false otherwise
  */
 bool ModelChecker::process_mutex(ModelAction *curr) {
-	std::mutex *mutex = (std::mutex *)curr->get_location();
-	struct std::mutex_state *state = mutex->get_state();
+	std::mutex *mutex=NULL;
+	struct std::mutex_state *state=NULL;
+
+	if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
+		mutex = (std::mutex *)curr->get_location();
+		state = mutex->get_state();
+	} else if(curr->is_wait()) {
+		mutex = (std::mutex *)curr->get_value();
+		state = mutex->get_state();
+	}
+
 	switch (curr->get_type()) {
 	case ATOMIC_TRYLOCK: {
 		bool success = !state->islocked;
@@ -1657,6 +1666,20 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 	if ((int)thrd_last_action->size() <= tid)
 		thrd_last_action->resize(get_num_threads());
 	(*thrd_last_action)[tid] = act;
+
+	if (act->is_wait()) {
+		void *mutex_loc=(void *) act->get_value();
+		obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+	
+		std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+		if (tid >= (int)vec->size())
+			vec->resize(priv->next_thread_id);
+		(*vec)[tid].push_back(act);
+
+		if ((int)thrd_last_action->size() <= tid)
+			thrd_last_action->resize(get_num_threads());
+		(*thrd_last_action)[tid] = act;
+	}
 }
 
 /**
@@ -1708,7 +1731,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
 	/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
 	for (rit = list->rbegin(); rit != list->rend(); rit++)
-		if ((*rit)->is_unlock())
+		if ((*rit)->is_unlock() || (*rit)->is_wait())
 			return *rit;
 	return NULL;
 }