Bug fix for spsc-queue test

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 078a1ce75849ebc48334958a7842b22dd6c958d1..ea8f268ff270fa8d59674570103699c1eb36eb03 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,9 +564,7 @@ void ModelChecker::handleChosenThread(ucontext_t *old)
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } else
-
-       {
+       } else {
                /* Consume the next action for a Thread */
                consumeAction();
 
@@ -604,7 +607,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);