Simplify code

diff --git a/action.cc b/action.cc
index af42a1f06e952580b2f984c2f81c134b89748bf4..65e1447f1a755cae8416df96aa330addff0f4711 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -720,6 +720,9 @@ void ModelAction::print() const
        model_print("%-4d %-2d   %-14s  %7s  %14p   %-#18" PRIx64,
                                                        seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());
        if (is_read()) {
+               if (is_write()) {
+                       model_print("(%" PRIx64 ")", get_write_value());
+               }
                if (reads_from)
                        model_print("  %-3d", reads_from->get_seq_number());
                else

diff --git a/model.cc b/model.cc
index 596e528d84e75adcacdda1d3f6bd71345333100a..4061fe0c9079d2085cd2c60f8664d917f7636e9f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -65,6 +65,7 @@ ModelChecker::ModelChecker() :
        history(new ModelHistory()),
        execution(new ModelExecution(this, scheduler)),
        execution_number(1),
+       curr_thread_num(1),
        trace_analyses(),
        inspect_plugin(NULL)
 {
@@ -343,29 +344,7 @@ void ModelChecker::startRunExecution(Thread *old) {
                        return;
                }
 
-               if (execution->has_asserted()) {
-                       finishRunExecution(old);
-                       return;
-               }
-               if (!chosen_thread)
-                       chosen_thread = get_next_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);
-                       chosen_thread = NULL;
-                       // Allow this thread to stash the next pending action
-                       continue;
-               }
-
-               /* Consume the next action for a Thread */
-               consumeAction();
-
-               if (should_terminate_execution()) {
-                       finishRunExecution(old);
+               if (!handleChosenThread(old)) {
                        return;
                }
        }
@@ -403,6 +382,9 @@ void ModelChecker::finishRunExecution(Thread *old)
 {
        scheduler->set_current_thread(NULL);
 
+       /** Reset curr_thread_num to initial value for next execution. */
+       curr_thread_num = 1;
+
        /** If we have more executions, we won't make it past this call. */
        finish_execution(execution_number < params.maxexecutions);
 
@@ -482,9 +464,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
                scheduler->sleep(old);
        }
-       chooseThread(act, old);
 
-       curr_thread_num++;
        Thread* next = getNextThread(old);
        if (next != nullptr) {
                scheduler->set_current_thread(next);
@@ -492,31 +472,33 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
                        perror("swap threads");
                        exit(EXIT_FAILURE);
                }
-       } else
-               handleChosenThread(old);
-
+       } else {
+               if (handleChosenThread(old)) {
+                       startRunExecution(old);
+               }
+       }
        return old->get_return_value();
 }
 
-void ModelChecker::handleChosenThread(Thread *old)
+bool ModelChecker::handleChosenThread(Thread *old)
 {
        if (execution->has_asserted()) {
                finishRunExecution(old);
-               return;
+               return false;
        }
-       if (!chosen_thread)
+       if (!chosen_thread) {
                chosen_thread = get_next_thread();
+       }
        if (!chosen_thread || chosen_thread->is_model_thread()) {
                finishRunExecution(old);
-               return;
+               return false;
        }
        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
-               startRunExecution(old);
-               return;
+               return true;
        }
 
        // Consume the next action for a Thread
@@ -524,9 +506,10 @@ void ModelChecker::handleChosenThread(Thread *old)
 
        if (should_terminate_execution()) {
                finishRunExecution(old);
-               return;
-       } else
-               startRunExecution(old);
+               return false;
+       } else {
+               return true;
+       }
 }
 
 void ModelChecker::startChecker() {

diff --git a/model.h b/model.h
index 12aeebcce1df645950ce702d07c14f459da15de6..59ca72838adf40eb0649b33e54adeb4adf243869 100644 (file)
--- a/model.h
+++ b/model.h
@@ -80,7 +80,7 @@ private:
        void consumeAction();
        void chooseThread(ModelAction *act, Thread *thr);
        Thread * getNextThread(Thread *old);
-       void handleChosenThread(Thread *old);
+       bool handleChosenThread(Thread *old);
 
        modelclock_t checkfree;