push changes

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 6732c265e9534a426a0aed9391303a2754faeda6..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: {
@@ -419,6 +423,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                        newcurr->copy_typeandorder(curr);
 
                ASSERT(curr->get_location()==newcurr->get_location());
+
                /* Discard duplicate ModelAction; use action from NodeStack */
                delete curr;
 
@@ -473,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);
        }
 
@@ -489,6 +494,15 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                build_reads_from_past(curr);
        curr = newcurr;
 
+       /* Add the action to lists before any other model-checking tasks */
+       if (!second_part_of_rmw)
+               add_action_to_lists(newcurr);
+
+       /* Build may_read_from set for newly-created actions */
+       if (curr == newcurr && curr->is_read())
+               build_reads_from_past(curr);
+       curr = newcurr;
+
        /* Thread specific actions */
        switch (curr->get_type()) {
        case THREAD_CREATE: {