From fa4c0d65d9c72d08d28e604a3eaa2fd82a9c6b20 Mon Sep 17 00:00:00 2001 From: root Date: Thu, 27 Jun 2019 15:12:34 -0700 Subject: [PATCH 1/1] 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