Bug fix for spsc-queue test
authorweiyu <weiyuluo1232@gmail.com>
Mon, 24 Aug 2020 22:45:26 +0000 (15:45 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Mon, 24 Aug 2020 22:45:26 +0000 (15:45 -0700)
1  2 
model.cc

diff --cc model.cc
+++ b/model.cc
@@@ -545,17 -544,13 +545,17 @@@ void ModelChecker::handleChosenThread(T
  
  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);
- /*    if (chosen_thread->just_woken_up()) {
 +              return;
 +      }
+       if (chosen_thread->just_woken_up()) {
                chosen_thread->set_wakeup_state(false);
                chosen_thread->set_pending(NULL);
                chosen_thread = NULL;
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } */
 -      } else
--
--      {
++      } else {
                /* Consume the next action for a Thread */
                consumeAction();