Bug fix

diff --git a/conditionvariable.cc b/conditionvariable.cc
index 1d049f1893c4bd66fb799ef0caba1eedd814f933..9d569e974406dc56831387c4f55e5321151d2739 100644 (file)
--- a/conditionvariable.cc
+++ b/conditionvariable.cc
@@ -14,15 +14,15 @@ condition_variable::~condition_variable() {
 }
 
 void condition_variable::notify_one() {
-       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this));
+       model->switch_thread(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));
+       model->switch_thread(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));
+       model->switch_thread(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock));
        //relock as a second action
        lock.lock();
 }

diff --git a/model.cc b/model.cc
index 54f01855adb2987e467e5556338edde4e1204a70..1e425b2ece627b877e5b33dd2d7bfde60d65b47e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -423,6 +423,7 @@ void ModelChecker::finishRunExecution(Thread *old)
 void ModelChecker::finishRunExecution(ucontext_t *old) 
 {
        scheduler->set_current_thread(NULL);
+       break_execution = true;
 }
 
 void ModelChecker::consumeAction()
@@ -544,12 +545,16 @@ void ModelChecker::handleChosenThread(Thread *old)
 
 void ModelChecker::handleChosenThread(ucontext_t *old)
 {
-       if (execution->has_asserted())
+       if (execution->has_asserted()) {
                finishRunExecution(old);
+               return;
+       }
        if (!chosen_thread)
                chosen_thread = get_next_thread();
-       if (!chosen_thread || chosen_thread->is_model_thread())
+       if (!chosen_thread || chosen_thread->is_model_thread()) {
                finishRunExecution(old);
+               return;
+       }
 /*     if (chosen_thread->just_woken_up()) {
                chosen_thread->set_wakeup_state(false);
                chosen_thread->set_pending(NULL);
@@ -559,7 +564,7 @@ void ModelChecker::handleChosenThread(ucontext_t *old)
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } else*/
+       } */
 
        {
                /* Consume the next action for a Thread */
@@ -604,7 +609,11 @@ void ModelChecker::run()
        checkfree = params.checkthreshold;
        for(int exec = 0;exec < params.maxexecutions;exec++) {
                chosen_thread = init_thread;
+               break_execution = false;
                do {
+                       if (break_execution)
+                               break;
+
                        thread_chosen = false;
                        curr_thread_num = 1;
                        startRunExecution(&system_context);

diff --git a/model.h b/model.h
index b98e7505a4bc21664384c930392b7b1a9b2b2c47..08f51b41752a8eced66f210b4a0c5477f82ff753 100644 (file)
--- a/model.h
+++ b/model.h
@@ -94,6 +94,7 @@ private:
        Thread * chosen_thread;
 
        bool thread_chosen;
+       bool break_execution;
 
        modelclock_t checkfree;
 

diff --git a/mutex.cc b/mutex.cc
index 0776db8eef5857b34c47bdbf3493194c9672097a..27e4a080a69de852f57295e46ad34f9e59e84464 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -19,17 +19,17 @@ mutex::mutex()
 
 void mutex::lock()
 {
-       model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
+       model->switch_thread(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
 }
 
 bool mutex::try_lock()
 {
-       return model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
+       return model->switch_thread(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
 }
 
 void mutex::unlock()
 {
-       model->switch_to_master(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this));
+       model->switch_thread(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this));
 }
 
 }