From 25f190b7c3700b5bafe37ea57617ca0af91534d6 Mon Sep 17 00:00:00 2001 From: weiyu Date: Wed, 26 Jun 2019 17:13:07 -0700 Subject: [PATCH] change func_atomics and work_list to vectors --- execution.cc | 9 +++--- history.cc | 81 ++++++++++++++++++++++++++++++++++++++++++++-------- history.h | 39 +++++++++++++++++-------- 3 files changed, 101 insertions(+), 28 deletions(-) diff --git a/execution.cc b/execution.cc index d75499f1..af98c2f3 100644 --- a/execution.cc +++ b/execution.cc @@ -14,6 +14,7 @@ #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" +#include "history.h" #include "fuzzer.h" #define INITIAL_THREAD_ID 0 @@ -64,7 +65,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 */ @@ -388,10 +389,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) */ void ModelExecution::process_write(ModelAction *curr) { - w_modification_order(curr); - - get_thread(curr)->set_return_value(VALUE_NONE); } @@ -1631,6 +1629,9 @@ Thread * ModelExecution::take_step(ModelAction *curr) curr = check_current_action(curr); ASSERT(curr); + // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() ); + model->get_history()->add_func_atomic( curr, curr_thrd->get_id() ); + if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd); diff --git a/history.cc b/history.cc index ca52209d..f757a5d7 100644 --- a/history.cc +++ b/history.cc @@ -2,29 +2,41 @@ #include "history.h" #include "action.h" +HistoryNode::HistoryNode(ModelAction *act) : + action(act) +{ + ASSERT(act); + this->position = act->get_position(); +} + +/** @brief Constructor */ ModelHistory::ModelHistory() : - func_id(1), /* function id starts with 1 */ + func_counter(0), /* function id starts with 0 */ func_map(), - func_history(), - work_list() + func_atomics(), + work_list(2) /* we have at least two threads */ {} 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); +// model_print("entering function: %d\n", func_id); + + uint32_t id = id_to_int(tid); + if ( work_list.size() <= id ) + work_list.resize( id + 1 ); + + func_id_list_t * func_list = work_list[id]; + if (func_list == NULL) { + func_list = new func_id_list_t(); + work_list[id] = func_list; } + + 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); + func_id_list_t * func_list = work_list[ id_to_int(tid) ]; uint32_t last_func_id = func_list->back(); if (last_func_id == func_id) { @@ -33,4 +45,49 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) 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); } + +// model_print("exiting function: %d\n", func_id); +} + +void ModelHistory::add_func_atomic(ModelAction *act, thread_id_t tid) { + /* return if thread i has not entered any function or has exited + from all functions */ + uint32_t id = id_to_int(tid); + if ( work_list.size() <= id ) + return; + else if (work_list[id] == NULL) + return; + + /* get the function id that thread i is currently in */ + func_id_list_t * func_list = work_list[id]; + uint32_t func_id = func_list->back(); + + if ( func_atomics.size() <= func_id ) + func_atomics.resize( func_id + 1 ); + + action_mlist_t * atomic_list = func_atomics[func_id]; + if (atomic_list == NULL) { + atomic_list = new action_mlist_t(); + func_atomics[func_id] = atomic_list; + } + + atomic_list->push_back(act); + + model_print("func id: %d, added atomic acts: %d\n", func_id, act->get_type()); +} + +void ModelHistory::print() { + for (uint32_t i = 0; i < func_atomics.size(); i++ ) { + action_mlist_t * atomic_list = func_atomics[i]; + + if (atomic_list == NULL) + continue; + + model_print("function with id: %d has following actions\n", i); + action_mlist_t::iterator it; + for (it = atomic_list->begin(); it != atomic_list->end(); it++) { + const ModelAction *act = *it; + act->print(); + } + } } diff --git a/history.h b/history.h index fff57126..03a89852 100644 --- a/history.h +++ b/history.h @@ -1,39 +1,54 @@ #include "stl-model.h" #include "common.h" #include "hashtable.h" -#include "modeltypes.h" +#include "threads-model.h" /* forward declaration */ class ModelAction; -typedef ModelList action_mlist_t; +typedef ModelList action_mlist_t; +typedef SnapList func_id_list_t; + +class HistoryNode { +public: + HistoryNode(ModelAction *act); + ~HistoryNode(); + + ModelAction * get_action() const { return action; } + const char * get_position() const { return position; } +private: + ModelAction * const action; + const char * position; +}; class ModelHistory { public: ModelHistory(); - + ~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++; } + uint32_t get_func_counter() { return func_counter; } + void incr_func_counter() { func_counter++; } + + void add_func_atomic(ModelAction *act, thread_id_t tid); HashTable * getFuncMap() { return &func_map; } - HashTable * getFuncHistory() { return &func_history; } + ModelVector< action_mlist_t * > * getFuncAtomics() { return &func_atomics; } void print(); - private: - uint32_t func_id; + uint32_t func_counter; /* map function names to integer ids */ HashTable func_map; - HashTable func_history; + ModelVector< action_mlist_t * > func_atomics; - /* work_list stores a list of function ids for each thread - * SnapList is intended to be used as a stack storing + /* Work_list stores a list of function ids for each thread. + * Each element in work_list 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; + SnapVector< func_id_list_t * > work_list; }; -- 2.34.1