From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 20 Sep 2012 00:38:24 +0000 (-0700)
Subject: push changes
X-Git-Tag: pldi2013~176
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d1930060e483b841f0a9c35c5041035dbdf6de4a

push changes
---

diff --git a/action.cc b/action.cc
index f7ca249..e5c9afe 100644
--- a/action.cc
+++ b/action.cc
@@ -217,7 +217,7 @@ void ModelAction::read_from(const ModelAction *act)
  * @param act The ModelAction to synchronize with
  */
 void ModelAction::synchronize_with(const ModelAction *act) {
-	ASSERT(*act < *this || type == THREAD_JOIN);
+	ASSERT(*act < *this || type == THREAD_JOIN || type == ATOMIC_LOCK );
 	model->check_promises(cv, act->cv);
 	cv->merge(act->cv);
 }
diff --git a/model.cc b/model.cc
index b539aba..aec05ff 100644
--- a/model.cc
+++ b/model.cc
@@ -332,8 +332,11 @@ void ModelChecker::process_mutex(ModelAction *curr) {
 	case ATOMIC_TRYLOCK: {
 		bool success=!state->islocked;
 		curr->set_try_lock(success);
-		if (!success)
+		if (!success) {
+			get_thread(curr)->set_return_value(0);
 			break;
+		}
+		get_thread(curr)->set_return_value(1);
 	}
 		//otherwise fall into the lock case
 	case ATOMIC_LOCK: {
@@ -344,7 +347,8 @@ void ModelChecker::process_mutex(ModelAction *curr) {
 		state->islocked=true;
 		ModelAction *unlock=get_last_unlock(curr);
 		//synchronize with the previous unlock statement
-		curr->synchronize_with(unlock);
+		if ( unlock != NULL )
+			curr->synchronize_with(unlock);
 		break;
 	}
 	case ATOMIC_UNLOCK: {
@@ -474,8 +478,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	if (!check_action_enabled(curr)) {
 		//we'll make the execution look like we chose to run this action
 		//much later...when a lock is actually available to relese
-		remove_thread(get_current_thread());
 		get_current_thread()->set_pending(curr);
+		remove_thread(get_current_thread());
 		return get_next_thread(NULL);
 	}
 
diff --git a/test/Makefile b/test/Makefile
index c817399..a0b6d6e 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -2,6 +2,8 @@ include ../common.mk
 
 CPPFLAGS += -I.. -I../include
 
+# Mac OSX options
+
 SRCS = $(wildcard *.c)
 OBJS = $(patsubst %.c,%.o,$(SRCS))