edits

diff --git a/model.cc b/model.cc
index a1204d0ab852352600edb95063476bd6f2976fa7..70ea4cd6534a9910ac176c1f497882e1ae6d3395 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -346,11 +346,13 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 
 void ModelChecker::continueRunExecution(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();
@@ -366,11 +368,13 @@ void ModelChecker::continueRunExecution(Thread *old)
 
 void ModelChecker::startRunExecution(ucontext_t *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();
@@ -402,7 +406,7 @@ Thread* ModelChecker::getNextThread()
                        scheduler->sleep(thr);
                }
 
-               chooseThread(act, thr);
+//             chooseThread(act, thr);
        }
        return nextThread;
 }
@@ -478,7 +482,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        if (act2 && execution->is_enabled(old) && !execution->check_action_enabled(act2)) {
                scheduler->sleep(old);
        }
-       chooseThread(act2, old);
+//     chooseThread(act2, old);
 
        curr_thread_num++;
        Thread* next = getNextThread();
@@ -536,7 +540,7 @@ void ModelChecker::handleChosenThread(ucontext_t *old)
                chosen_thread = get_next_thread();
        if (!chosen_thread || chosen_thread->is_model_thread())
                finishRunExecution(old);
-       if (chosen_thread->just_woken_up()) {
+/*     if (chosen_thread->just_woken_up()) {
                chosen_thread->set_wakeup_state(false);
                chosen_thread->set_pending(NULL);
                chosen_thread = NULL;
@@ -545,7 +549,9 @@ void ModelChecker::handleChosenThread(ucontext_t *old)
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } else {
+       } else*/
+
+       {
                /* Consume the next action for a Thread */
                consumeAction();
 
@@ -587,10 +593,13 @@ void ModelChecker::run()
        initstate(423121, random_state, sizeof(random_state));
        checkfree = params.checkthreshold;
        for(int exec = 0;exec < params.maxexecutions;exec++) {
-               chosen_thread = init_thread;
-               thread_chosen = false;
-               curr_thread_num = 1;
-               startRunExecution(&system_context);
+               do {
+                       chosen_thread = init_thread;
+                       thread_chosen = false;
+                       curr_thread_num = 1;
+                       startRunExecution(&system_context);
+               } while (!should_terminate_execution());
+
                finish_execution((exec+1) < params.maxexecutions);
                //restore random number generator state after rollback
                setstate(random_state);

diff --git a/threads.cc b/threads.cc
index 3d6b0863234273684de989ce7dd199e9f1931a72..fc5c84a160296f12f7b3c39db3a84c898bafee9f 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -60,7 +60,7 @@ Thread * thread_current(void)
 }
 
 void modelexit() {
-       model->switch_thread(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+       model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
 }
 
 void initMainThread() {