From: Brian Demsky <bdemsky@uci.edu>
Date: Sun, 30 Aug 2020 02:08:22 +0000 (-0700)
Subject: Simplify code
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=be8cc021ead92563f9ed55a922168d4a40da907f

Simplify code
---

diff --git a/action.cc b/action.cc
index af42a1f0..65e1447f 100644
--- a/action.cc
+++ b/action.cc
@@ -720,6 +720,9 @@ void ModelAction::print() const
 	model_print("%-4d %-2d   %-14s  %7s  %14p   %-#18" PRIx64,
 							seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());
 	if (is_read()) {
+		if (is_write()) {
+			model_print("(%" PRIx64 ")", get_write_value());
+		}
 		if (reads_from)
 			model_print("  %-3d", reads_from->get_seq_number());
 		else
diff --git a/model.cc b/model.cc
index 596e528d..4061fe0c 100644
--- a/model.cc
+++ b/model.cc
@@ -65,6 +65,7 @@ ModelChecker::ModelChecker() :
 	history(new ModelHistory()),
 	execution(new ModelExecution(this, scheduler)),
 	execution_number(1),
+	curr_thread_num(1),
 	trace_analyses(),
 	inspect_plugin(NULL)
 {
@@ -343,29 +344,7 @@ void ModelChecker::startRunExecution(Thread *old) {
 			return;
 		}
 
-		if (execution->has_asserted()) {
-			finishRunExecution(old);
-			return;
-		}
-		if (!chosen_thread)
-			chosen_thread = get_next_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);
-			chosen_thread = NULL;
-			// Allow this thread to stash the next pending action
-			continue;
-		}
-
-		/* Consume the next action for a Thread */
-		consumeAction();
-
-		if (should_terminate_execution()) {
-			finishRunExecution(old);
+		if (!handleChosenThread(old)) {
 			return;
 		}
 	}
@@ -403,6 +382,9 @@ void ModelChecker::finishRunExecution(Thread *old)
 {
 	scheduler->set_current_thread(NULL);
 
+	/** Reset curr_thread_num to initial value for next execution. */
+	curr_thread_num = 1;
+
 	/** If we have more executions, we won't make it past this call. */
 	finish_execution(execution_number < params.maxexecutions);
 
@@ -482,9 +464,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 	if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
 		scheduler->sleep(old);
 	}
-	chooseThread(act, old);
 
-	curr_thread_num++;
 	Thread* next = getNextThread(old);
 	if (next != nullptr) {
 		scheduler->set_current_thread(next);
@@ -492,31 +472,33 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 			perror("swap threads");
 			exit(EXIT_FAILURE);
 		}
-	} else
-		handleChosenThread(old);
-
+	} else {
+		if (handleChosenThread(old)) {
+			startRunExecution(old);
+		}
+	}
 	return old->get_return_value();
 }
 
-void ModelChecker::handleChosenThread(Thread *old)
+bool ModelChecker::handleChosenThread(Thread *old)
 {
 	if (execution->has_asserted()) {
 		finishRunExecution(old);
-		return;
+		return false;
 	}
-	if (!chosen_thread)
+	if (!chosen_thread) {
 		chosen_thread = get_next_thread();
+	}
 	if (!chosen_thread || chosen_thread->is_model_thread()) {
 		finishRunExecution(old);
-		return;
+		return false;
 	}
 	if (chosen_thread->just_woken_up()) {
 		chosen_thread->set_wakeup_state(false);
 		chosen_thread->set_pending(NULL);
 		chosen_thread = NULL;
 		// Allow this thread to stash the next pending action
-		startRunExecution(old);
-		return;
+		return true;
 	}
 
 	// Consume the next action for a Thread
@@ -524,9 +506,10 @@ void ModelChecker::handleChosenThread(Thread *old)
 
 	if (should_terminate_execution()) {
 		finishRunExecution(old);
-		return;
-	} else
-		startRunExecution(old);
+		return false;
+	} else {
+		return true;
+	}
 }
 
 void ModelChecker::startChecker() {
diff --git a/model.h b/model.h
index 12aeebcc..59ca7283 100644
--- a/model.h
+++ b/model.h
@@ -80,7 +80,7 @@ private:
 	void consumeAction();
 	void chooseThread(ModelAction *act, Thread *thr);
 	Thread * getNextThread(Thread *old);
-	void handleChosenThread(Thread *old);
+	bool handleChosenThread(Thread *old);
 
 	modelclock_t checkfree;