From: weiyu <weiyuluo1232@gmail.com>
Date: Mon, 24 Aug 2020 22:45:26 +0000 (-0700)
Subject: Bug fix for spsc-queue test
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=edf082882ea7a2d27d3a3322a84e42b040f186a4

Bug fix for spsc-queue test
---

edf082882ea7a2d27d3a3322a84e42b040f186a4
diff --cc model.cc
index 1e425b2e,078a1ce7..ea8f268f
--- a/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);
 +		return;
 +	}
- /*	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;
@@@ -564,9 -559,9 +564,7 @@@
  			finishRunExecution(old);
  		else
  			startRunExecution(old);	
- 	} */
 -	} else
--
--	{
++	} else {
  		/* Consume the next action for a Thread */
  		consumeAction();