push changes

diff --git a/action.cc b/action.cc
index f7ca249f965e6b351cd9763f382f9c792d586182..e5c9afe46f4cd81fff20555344b669c23c9b4bb1 100644 (file)
--- 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 b539aba6beba1339231a4f0c10cbf2e996a76f0e..aec05ffe4bc6a46c0bf00d2d252d8bfa2025613e 100644 (file)
--- 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 c81739902b94d01fd48aee8064228149a7595443..a0b6d6e4ac9829bb6184e41c6cc5bca8b064c03e 100644 (file)
--- 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))