From fa4c0d65d9c72d08d28e604a3eaa2fd82a9c6b20 Mon Sep 17 00:00:00 2001
From: root <root@dw-6.eecs.uci.edu>
Date: Thu, 27 Jun 2019 15:12:34 -0700
Subject: [PATCH] bug fixes
---
execution.cc | 2 +-
model.cc | 24 +++++++++++++-----------
threads-model.h | 2 +-
threads.cc | 5 -----
4 files changed, 15 insertions(+), 18 deletions(-)
diff --git a/execution.cc b/execution.cc
index 2c08711e..2e744251 100644
--- a/execution.cc
+++ b/execution.cc
@@ -64,7 +64,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack
thrd_last_fence_release(),
node_stack(node_stack),
priv(new struct model_snapshot_members ()),
- mo_graph(new CycleGraph()),
+ mo_graph(new CycleGraph()),
fuzzer(new Fuzzer())
{
/* Initialize a model-checker thread, for special ModelActions */
diff --git a/model.cc b/model.cc
index 7f38adc3..b4bbb70e 100644
--- a/model.cc
+++ b/model.cc
@@ -162,7 +162,7 @@ void ModelChecker::print_bugs() const
bugs->size(),
bugs->size() > 1 ? "s" : "");
for (unsigned int i = 0;i < bugs->size();i++)
- (*bugs)[i]->print();
+ (*bugs)[i] -> print();
}
/**
@@ -173,15 +173,15 @@ void ModelChecker::print_bugs() const
*/
void ModelChecker::record_stats()
{
- stats.num_total++;
+ stats.num_total ++;
if (!execution->isfeasibleprefix())
- stats.num_infeasible++;
+ stats.num_infeasible ++;
else if (execution->have_bug_reports())
- stats.num_buggy_executions++;
+ stats.num_buggy_executions ++;
else if (execution->is_complete_execution())
- stats.num_complete++;
+ stats.num_complete ++;
else {
- stats.num_redundant++;
+ stats.num_redundant ++;
/**
* @todo We can violate this ASSERT() when fairness/sleep sets
@@ -262,15 +262,15 @@ bool ModelChecker::next_execution()
return true;
}
// test code
- execution_number++;
+ execution_number ++;
reset_to_initial_state();
return false;
}
/** @brief Run trace analyses on complete trace */
void ModelChecker::run_trace_analyses() {
- for (unsigned int i = 0;i < trace_analyses.size();i++)
- trace_analyses[i]->analyze(execution->get_action_trace());
+ for (unsigned int i = 0;i < trace_analyses.size();i ++)
+ trace_analyses[i] -> analyze(execution->get_action_trace());
}
/**
@@ -373,7 +373,9 @@ void ModelChecker::do_restart()
}
void ModelChecker::startMainThread() {
- init_thread->setContext();
+ init_thread->set_state(THREAD_RUNNING);
+ scheduler->set_current_thread(init_thread);
+ thread_startup();
}
/** @brief Run ModelChecker for the user program */
@@ -383,7 +385,7 @@ void ModelChecker::run()
char random_state[256];
initstate(423121, random_state, sizeof(random_state));
- for(int exec = 0;exec < params.maxexecutions;exec++) {
+ for(int exec = 0;exec < params.maxexecutions;exec ++) {
Thread * t = init_thread;
do {
diff --git a/threads-model.h b/threads-model.h
index 513142b5..02f20b03 100644
--- a/threads-model.h
+++ b/threads-model.h
@@ -50,7 +50,6 @@ public:
static int swap(ucontext_t *ctxt, Thread *t);
static int swap(Thread *t, ucontext_t *ctxt);
- void setContext();
thread_state get_state() const { return state; }
void set_state(thread_state s);
thread_id_t get_id() const;
@@ -162,6 +161,7 @@ private:
};
Thread * thread_current();
+void thread_startup();
static inline thread_id_t thrd_to_id(thrd_t t)
{
diff --git a/threads.cc b/threads.cc
index 56942f5f..67f681ca 100644
--- a/threads.cc
+++ b/threads.cc
@@ -86,11 +86,6 @@ int Thread::create_context()
return 0;
}
-void Thread::setContext() {
- set_state(THREAD_RUNNING);
- setcontext(&context);
-}
-
/**
* Swaps the current context to another thread of execution. This form switches
* from a user Thread to a system context.
--
2.34.1