From be8cc021ead92563f9ed55a922168d4a40da907f Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 29 Aug 2020 19:08:22 -0700
Subject: [PATCH] Simplify code
---
action.cc | 3 +++
model.cc | 57 +++++++++++++++++++------------------------------------
model.h | 2 +-
3 files changed, 24 insertions(+), 38 deletions(-)
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;
--
2.34.1