From 008bdd4e5b8a010b19133ba952900b162a4c731b Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 25 Jun 2019 15:05:12 -0700 Subject: [PATCH] add a new class 'ModelHistory' --- classlist.h | 1 + cmodelint.cc | 29 +++++++++++++++++++++++++++-- history.cc | 36 ++++++++++++++++++++++++++++++++++++ history.h | 39 +++++++++++++++++++++++++++++++++++++++ model.cc | 2 ++ model.h | 3 +++ 6 files changed, 108 insertions(+), 2 deletions(-) create mode 100644 history.cc create mode 100644 history.h diff --git a/classlist.h b/classlist.h index 09aa09d1..641a1481 100644 --- a/classlist.h +++ b/classlist.h @@ -8,6 +8,7 @@ class CycleNode; class ModelAction; class ModelChecker; class ModelExecution; +class ModelHistory; class Node; class NodeStack; class Scheduler; diff --git a/cmodelint.cc b/cmodelint.cc index 184bb40e..5be511c8 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -1,6 +1,10 @@ #include +#include + #include "model.h" +#include "execution.h" #include "action.h" +#include "history.h" #include "cmodelint.h" #include "threads-model.h" @@ -360,11 +364,32 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { */ void cds_func_entry(const char * funcName) { + if (!model) return; + Thread * th = thread_current(); - printf("thread %d Enter function %s\n", th->get_id(), funcName); + uint32_t func_id; + + ModelHistory *history = model->get_history(); + if ( !history->getFuncMap()->contains(funcName) ) { + func_id = history->get_func_counter(); + history->incr_func_counter(); + + history->getFuncMap()->put(funcName, func_id); + } else { + func_id = history->getFuncMap()->get(funcName); + } + + history->enter_function(func_id, th->get_id()); } void cds_func_exit(const char * funcName) { + if (!model) return; + Thread * th = thread_current(); - printf("thread %d Exit from function %s\n", th->get_id(), funcName); + uint32_t func_id; + + ModelHistory *history = model->get_history(); + func_id = history->getFuncMap()->get(funcName); + + history->exit_function(func_id, th->get_id()); } diff --git a/history.cc b/history.cc new file mode 100644 index 00000000..ca52209d --- /dev/null +++ b/history.cc @@ -0,0 +1,36 @@ +#include +#include "history.h" +#include "action.h" + +ModelHistory::ModelHistory() : + func_id(1), /* function id starts with 1 */ + func_map(), + func_history(), + work_list() +{} + +void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) +{ + if ( !work_list.contains(tid) ) { + // This thread has not been pushed to work_list + SnapList * func_list = new SnapList(); + func_list->push_back(func_id); + work_list.put(tid, func_list); + } else { + SnapList * func_list = work_list.get(tid); + func_list->push_back(func_id); + } +} + +void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) +{ + SnapList * func_list = work_list.get(tid); + uint32_t last_func_id = func_list->back(); + + if (last_func_id == func_id) { + func_list->pop_back(); + } else { + model_print("trying to exit with a wrong function id\n"); + model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id); + } +} diff --git a/history.h b/history.h new file mode 100644 index 00000000..fff57126 --- /dev/null +++ b/history.h @@ -0,0 +1,39 @@ +#include "stl-model.h" +#include "common.h" +#include "hashtable.h" +#include "modeltypes.h" + +/* forward declaration */ +class ModelAction; + +typedef ModelList action_mlist_t; + +class ModelHistory { +public: + ModelHistory(); + + void enter_function(const uint32_t func_id, thread_id_t tid); + void exit_function(const uint32_t func_id, thread_id_t tid); + + uint32_t get_func_counter() { return func_id; } + void incr_func_counter() { func_id++; } + + HashTable * getFuncMap() { return &func_map; } + HashTable * getFuncHistory() { return &func_history; } + + void print(); + +private: + uint32_t func_id; + + /* map function names to integer ids */ + HashTable func_map; + + HashTable func_history; + + /* work_list stores a list of function ids for each thread + * SnapList is intended to be used as a stack storing + * the functions that thread i has entered and yet to exit from + */ + HashTable *, uintptr_t, 4> work_list; +}; diff --git a/model.cc b/model.cc index 84a60a51..3235f5c4 100644 --- a/model.cc +++ b/model.cc @@ -16,6 +16,7 @@ #include "output.h" #include "traceanalysis.h" #include "execution.h" +#include "history.h" #include "bugmessage.h" ModelChecker *model; @@ -28,6 +29,7 @@ ModelChecker::ModelChecker() : scheduler(new Scheduler()), node_stack(new NodeStack()), execution(new ModelExecution(this, scheduler, node_stack)), + history(new ModelHistory()), execution_number(1), trace_analyses(), inspect_plugin(NULL) diff --git a/model.h b/model.h index 2a505c3d..4d8558e2 100644 --- a/model.h +++ b/model.h @@ -46,6 +46,7 @@ public: ucontext_t * get_system_context() { return &system_context; } ModelExecution * get_execution() const { return execution; } + ModelHistory * get_history() const { return history; } int get_execution_number() const { return execution_number; } @@ -63,6 +64,7 @@ public: model_params params; void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } + MEMALLOC private: /** Flag indicates whether to restart the model checker. */ @@ -72,6 +74,7 @@ private: Scheduler * const scheduler; NodeStack * const node_stack; ModelExecution *execution; + ModelHistory *history; int execution_number; -- 2.34.1