fix the case where no waiter is waiting

diff --git a/execution.cc b/execution.cc
index f6b59cd9bda059c194c473bf376564c0ee343b9d..8fdc9fbe59be737ed849582ac77b35c124d41665 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -753,6 +753,11 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                int wakeupthread = curr->get_node()->get_misc();
                action_list_t::iterator it = waiters->begin();
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                int wakeupthread = curr->get_node()->get_misc();
                action_list_t::iterator it = waiters->begin();

+
+               // WL
+               if (it == waiters->end())
+                       break;
+

                advance(it, wakeupthread);
                scheduler->wake(get_thread(*it));
                waiters->erase(it);
                advance(it, wakeupthread);
                scheduler->wake(get_thread(*it));
                waiters->erase(it);


@@ -2727,7 +2732,7 @@ static void print_list(const action_list_t *list)
        action_list_t::const_iterator it;
 
        model_print("------------------------------------------------------------------------------------\n");
        action_list_t::const_iterator it;
 
        model_print("------------------------------------------------------------------------------------\n");

-       model_print("#    t     Action type     MO       Location         Value               Rf  CV\n");
+       model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");

        model_print("------------------------------------------------------------------------------------\n");
 
        unsigned int hash = 0;
        model_print("------------------------------------------------------------------------------------\n");
 
        unsigned int hash = 0;