Small edits

diff --git a/model.cc b/model.cc
index 4061fe0c9079d2085cd2c60f8664d917f7636e9f..5292b24745a3eaa2c9ddd99c904dfd05718bc1b6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -332,7 +332,6 @@ void ModelChecker::startRunExecution(Thread *old) {
 
                thread_chosen = false;
                curr_thread_num = 1;
 
                thread_chosen = false;
                curr_thread_num = 1;

-

                Thread *thr = getNextThread(old);
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);
                Thread *thr = getNextThread(old);
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);


@@ -406,13 +405,6 @@ void ModelChecker::finishRunExecution(Thread *old)
        _Exit(0);
 }
 
        _Exit(0);
 }
 

-void ModelChecker::consumeAction()
-{
-       ModelAction *curr = chosen_thread->get_pending();
-       chosen_thread->set_pending(NULL);
-       chosen_thread = execution->take_step(curr);
-}
-

 /* Allow pending relaxed/release stores or thread actions to perform first */
 void ModelChecker::chooseThread(ModelAction *act, Thread *thr)
 {
 /* Allow pending relaxed/release stores or thread actions to perform first */
 void ModelChecker::chooseThread(ModelAction *act, Thread *thr)
 {


@@ -461,10 +453,6 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        if (old->is_waiting_on(old))
                assert_bug("Deadlock detected (thread %u)", curr_thread_num);
 
        if (old->is_waiting_on(old))
                assert_bug("Deadlock detected (thread %u)", curr_thread_num);
 

-       if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
-               scheduler->sleep(old);
-       }
-

        Thread* next = getNextThread(old);
        if (next != nullptr) {
                scheduler->set_current_thread(next);
        Thread* next = getNextThread(old);
        if (next != nullptr) {
                scheduler->set_current_thread(next);


@@ -502,7 +490,9 @@ bool ModelChecker::handleChosenThread(Thread *old)
        }
 
        // Consume the next action for a Thread
        }
 
        // Consume the next action for a Thread

-       consumeAction();
+       ModelAction *curr = chosen_thread->get_pending();
+       chosen_thread->set_pending(NULL);
+       chosen_thread = execution->take_step(curr);

 
        if (should_terminate_execution()) {
                finishRunExecution(old);
 
        if (should_terminate_execution()) {
                finishRunExecution(old);

diff --git a/model.h b/model.h
index 59ca72838adf40eb0649b33e54adeb4adf243869..7763c568fb6c7a468c86195389f1d2f1f66a7cd4 100644 (file)
--- a/model.h
+++ b/model.h
@@ -77,7 +77,6 @@ private:
 
        void startRunExecution(Thread *old);
        void finishRunExecution(Thread *old);
 
        void startRunExecution(Thread *old);
        void finishRunExecution(Thread *old);

-       void consumeAction();

        void chooseThread(ModelAction *act, Thread *thr);
        Thread * getNextThread(Thread *old);
        bool handleChosenThread(Thread *old);
        void chooseThread(ModelAction *act, Thread *thr);
        Thread * getNextThread(Thread *old);
        bool handleChosenThread(Thread *old);