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://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=edf082882ea7a2d27d3a3322a84e42b040f186a4;hp=-c

Bug fix for spsc-queue test
---

edf082882ea7a2d27d3a3322a84e42b040f186a4
diff --combined model.cc
index 1e425b2e,078a1ce7..ea8f268f
--- a/model.cc
+++ b/model.cc
@@@ -346,13 -346,13 +346,13 @@@ uint64_t ModelChecker::switch_to_master
  
  void ModelChecker::continueRunExecution(Thread *old) 
  {
- /*
+ 
  	if (params.traceminsize != 0 &&
  			execution->get_curr_seq_num() > checkfree) {
  		checkfree += params.checkthreshold;
  		execution->collectActions();
  	}
- */
+ 
  	thread_chosen = false;
  	curr_thread_num = 1;
  	Thread *thr = getNextThread();
@@@ -368,13 -368,13 +368,13 @@@
  
  void ModelChecker::startRunExecution(ucontext_t *old) 
  {
- /*
+ 
  	if (params.traceminsize != 0 &&
  			execution->get_curr_seq_num() > checkfree) {
  		checkfree += params.checkthreshold;
  		execution->collectActions();
  	}
- */
+ 
  	thread_chosen = false;
  	curr_thread_num = 1;
  	Thread *thr = getNextThread();
@@@ -406,7 -406,7 +406,7 @@@ Thread* ModelChecker::getNextThread(
  			scheduler->sleep(thr);
  		}
  
- //		chooseThread(act, thr);
+ 	chooseThread(act, thr);
  	}
  	return nextThread;
  }
@@@ -423,7 -423,6 +423,7 @@@ void ModelChecker::finishRunExecution(T
  void ModelChecker::finishRunExecution(ucontext_t *old) 
  {
  	scheduler->set_current_thread(NULL);
 +	break_execution = true;
  }
  
  void ModelChecker::consumeAction()
@@@ -491,7 -490,7 +491,7 @@@ uint64_t ModelChecker::switch_thread(Mo
  	if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
  		scheduler->sleep(old);
  	}
- //	chooseThread(act, old);
+ 	chooseThread(act, old);
  
  	curr_thread_num++;
  	Thread* next = getNextThread();
@@@ -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();
  
@@@ -609,11 -604,7 +607,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);