Remove duplicate functions

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index ac394d9a49ec9f164051c04328fe35af04e22d85..090743a49ff0ce6da1a1627acdd1367ebdc5c0ac 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -344,24 +344,33 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        return old->get_return_value();
 }
 
-void ModelChecker::continueExecution(Thread *old) 
+void ModelChecker::startRunExecution(Thread *old) 
 {
+
        if (params.traceminsize != 0 &&
                        execution->get_curr_seq_num() > checkfree) {
                checkfree += params.checkthreshold;
                execution->collectActions();
        }
+
        thread_chosen = false;
        curr_thread_num = 1;
        Thread *thr = getNextThread();
        if (thr != nullptr) {
                scheduler->set_current_thread(thr);
-               if (Thread::swap(old, thr) < 0) {
-                       perror("swap threads");
-                       exit(EXIT_FAILURE);
+               if (old) {
+                       if (Thread::swap(old, thr) < 0) {
+                               perror("swap threads");
+                               exit(EXIT_FAILURE);
+                       }
+               } else {
+                       if (Thread::swap(&system_context, thr) < 0) {
+                               perror("swap threads");
+                               exit(EXIT_FAILURE);
+                       }       
                }
        } else
-               handleChosenThread(old);        
+               handleChosenThread(old);
 }
 
 Thread* ModelChecker::getNextThread()
@@ -382,25 +391,38 @@ Thread* ModelChecker::getNextThread()
                        scheduler->sleep(thr);
                }
 
-               chooseThread(act, thr);
+       chooseThread(act, thr);
        }
        return nextThread;
 }
 
-void ModelChecker::finishExecution(Thread *old) 
+void ModelChecker::finishRunExecution(Thread *old) 
 {
        scheduler->set_current_thread(NULL);
-       if (Thread::swap(old, &system_context) < 0) {
-               perror("swap threads");
-               exit(EXIT_FAILURE);
+       if (old != NULL) {
+               if (Thread::swap(old, &system_context) < 0) {
+                       perror("swap threads");
+                       exit(EXIT_FAILURE);
+               }
        }
+       break_execution = true;
 }
 
 void ModelChecker::consumeAction()
 {
        ModelAction *curr = chosen_thread->get_pending();
-       chosen_thread->set_pending(NULL);
-       chosen_thread = execution->take_step(curr);
+       Thread * th = thread_current();
+       if (curr->get_type() == THREAD_FINISH && th != NULL)  {
+               // Thread finish must be consumed in the master context
+               scheduler->set_current_thread(NULL);
+               if (Thread::swap(th, &system_context) < 0) {
+                       perror("swap threads");
+                       exit(EXIT_FAILURE);
+               }
+       } else {
+               chosen_thread->set_pending(NULL);
+               chosen_thread = execution->take_step(curr);
+       }
 }
 
 void ModelChecker::chooseThread(ModelAction *act, Thread *thr)
@@ -448,58 +470,63 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        if (old->is_waiting_on(old))
                assert_bug("Deadlock detected (thread %u)", curr_thread_num);
 
-       ModelAction *act2 = old->get_pending();
-               
-       if (act2 && execution->is_enabled(old) && !execution->check_action_enabled(act2)) {
+       if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
                scheduler->sleep(old);
        }
-       chooseThread(act2, old);
+       chooseThread(act, old);
 
        curr_thread_num++;
        Thread* next = getNextThread();
        if (next != nullptr) 
                handleNewValidThread(old, next);
-       else
+       else {
+               old->set_state(THREAD_READY);   // Just to avoid the first ASSERT in ModelExecution::take_step 
                handleChosenThread(old);
+       }
 
        return old->get_return_value();
 }
 
 void ModelChecker::handleNewValidThread(Thread *old, Thread *next)
 {
-       scheduler->set_current_thread(next);    
+       scheduler->set_current_thread(next);
 
        if (Thread::swap(old, next) < 0) {
                perror("swap threads");
                exit(EXIT_FAILURE);
-       }               
+       }
 }
 
 void ModelChecker::handleChosenThread(Thread *old)
 {
-       if (execution->has_asserted())
-               finishExecution(old);
+       Thread * th = old ? old : thread_current();
+       if (execution->has_asserted()) {
+               finishRunExecution(th);
+               return;
+       }
        if (!chosen_thread)
                chosen_thread = get_next_thread();
-       if (!chosen_thread || chosen_thread->is_model_thread())
-               finishExecution(old);
+       if (!chosen_thread || chosen_thread->is_model_thread()) {
+               finishRunExecution(th);
+               return;
+       }
        if (chosen_thread->just_woken_up()) {
                chosen_thread->set_wakeup_state(false);
                chosen_thread->set_pending(NULL);
                chosen_thread = NULL;
                // Allow this thread to stash the next pending action
                if (should_terminate_execution())
-                       finishExecution(old);
+                       finishRunExecution(th);
                else
-                       continueExecution(old); 
+                       startRunExecution(th);
        } else {
                /* Consume the next action for a Thread */
                consumeAction();
 
                if (should_terminate_execution())
-                       finishExecution(old);
+                       finishRunExecution(th);
                else
-                       continueExecution(old);         
+                       startRunExecution(th);
        }
 }
 
@@ -534,16 +561,16 @@ void ModelChecker::run()
        checkfree = params.checkthreshold;
        for(int exec = 0;exec < params.maxexecutions;exec++) {
                chosen_thread = init_thread;
-               thread_chosen = false;
-               curr_thread_num = 1;
-               thread_id_t tid = int_to_id(1);
-               Thread *thr = get_thread(tid);
-               if (!thr->get_pending())
-                       switch_from_master(thr);
-               else {
-                       consumeAction();
-                       switch_from_master(thr);
-               }
+               break_execution = false;
+               do {
+                       if (break_execution)
+                               break;
+
+                       thread_chosen = false;
+                       curr_thread_num = 1;
+                       startRunExecution(NULL);
+               } while (!should_terminate_execution());
+
                finish_execution((exec+1) < params.maxexecutions);
                //restore random number generator state after rollback
                setstate(random_state);