Bug fix
authorweiyu <weiyuluo1232@gmail.com>
Mon, 24 Aug 2020 22:39:35 +0000 (15:39 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Mon, 24 Aug 2020 22:39:35 +0000 (15:39 -0700)
conditionvariable.cc
model.cc
model.h
mutex.cc

index 1d049f1..9d569e9 100644 (file)
@@ -14,15 +14,15 @@ condition_variable::~condition_variable() {
 }
 
 void condition_variable::notify_one() {
-       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this));
+       model->switch_thread(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this));
 }
 
 void condition_variable::notify_all() {
-       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this));
+       model->switch_thread(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this));
 }
 
 void condition_variable::wait(mutex& lock) {
-       model->switch_to_master(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock));
+       model->switch_thread(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock));
        //relock as a second action
        lock.lock();
 }
index 54f0185..1e425b2 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,7 +564,7 @@ void ModelChecker::handleChosenThread(ucontext_t *old)
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } else*/
+       } */
 
        {
                /* Consume the next action for a Thread */
@@ -604,7 +609,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);
diff --git a/model.h b/model.h
index b98e750..08f51b4 100644 (file)
--- a/model.h
+++ b/model.h
@@ -94,6 +94,7 @@ private:
        Thread * chosen_thread;
 
        bool thread_chosen;
+       bool break_execution;
 
        modelclock_t checkfree;
 
index 0776db8..27e4a08 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -19,17 +19,17 @@ mutex::mutex()
 
 void mutex::lock()
 {
-       model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
+       model->switch_thread(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this));
 }
 
 bool mutex::try_lock()
 {
-       return model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
+       return model->switch_thread(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
 }
 
 void mutex::unlock()
 {
-       model->switch_to_master(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this));
+       model->switch_thread(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this));
 }
 
 }