From 9e899821b7500371dbe61975ccbc64e42e82ef83 Mon Sep 17 00:00:00 2001 From: root Date: Wed, 3 Jul 2019 13:36:54 -0700 Subject: [PATCH] get rid of nodestack --- Makefile | 2 +- action.cc | 17 ++----- action.h | 18 ++----- classlist.h | 2 - execution.cc | 19 +++----- execution.h | 5 +- fuzzer.cc | 2 +- fuzzer.h | 2 +- model.cc | 7 +-- model.h | 1 - nodestack.cc | 131 --------------------------------------------------- nodestack.h | 83 -------------------------------- schedule.cc | 7 +-- schedule.h | 2 +- 14 files changed, 26 insertions(+), 272 deletions(-) delete mode 100644 nodestack.cc delete mode 100644 nodestack.h diff --git a/Makefile b/Makefile index 0d2af464..05afc05c 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ include common.mk OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ - nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ + clockvector.o main.o snapshot-interface.o cyclegraph.o \ datarace.o impatomic.o cmodelint.o \ snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \ context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \ diff --git a/action.cc b/action.cc index 8dcc9d51..0cd49cf1 100644 --- a/action.cc +++ b/action.cc @@ -8,7 +8,6 @@ #include "clockvector.h" #include "common.h" #include "threads-model.h" -#include "nodestack.h" #include "wildcard.h" #define ACTION_INITIAL_CLOCK 0 @@ -37,7 +36,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, position(NULL), reads_from(NULL), last_fence_release(NULL), - node(NULL), + uninitaction(NULL), cv(NULL), rf_cv(NULL), value(value), @@ -72,7 +71,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, position(NULL), reads_from(NULL), last_fence_release(NULL), - node(NULL), + uninitaction(NULL), cv(NULL), rf_cv(NULL), value(value), @@ -107,7 +106,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order position(position), reads_from(NULL), last_fence_release(NULL), - node(NULL), + uninitaction(NULL), cv(NULL), rf_cv(NULL), value(value), @@ -143,7 +142,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order position(position), reads_from(NULL), last_fence_release(NULL), - node(NULL), + uninitaction(NULL), cv(NULL), rf_cv(NULL), value(value), @@ -583,14 +582,6 @@ uint64_t ModelAction::get_return_value() const return value; } -/** @return The Node associated with this ModelAction */ -Node * ModelAction::get_node() const -{ - /* UNINIT actions do not have a Node */ - ASSERT(!is_uninitialized()); - return node; -} - /** * Update the model action's read_from action * @param act The action to read from; should be a write diff --git a/action.h b/action.h index 5e8b1b1c..4eb1f7ed 100644 --- a/action.h +++ b/action.h @@ -106,9 +106,6 @@ public: ModelAction * get_reads_from() const { return reads_from; } cdsc::mutex * get_mutex() const; - Node * get_node() const; - void set_node(Node *n) { node = n; } - void set_read_from(ModelAction *act); /** Store the most recent fence-release from the same thread @@ -179,6 +176,8 @@ public: /* to accomodate pthread create and join */ Thread * thread_operand; void set_thread_operand(Thread *th) { thread_operand = th; } + void set_uninit_action(ModelAction *act) { uninitaction = act; } + ModelAction * get_uninit_action() { return uninitaction; } SNAPSHOTALLOC private: const char * get_type_str() const; @@ -202,15 +201,8 @@ private: /** @brief The last fence release from the same thread */ const ModelAction *last_fence_release; - - /** - * @brief A back reference to a Node in NodeStack - * - * Only set if this ModelAction is saved on the NodeStack. (A - * ModelAction can be thrown away before it ever enters the NodeStack.) - */ - Node *node; - + ModelAction * uninitaction; + /** * @brief The clock vector for this operation * @@ -220,7 +212,7 @@ private: */ ClockVector *cv; ClockVector *rf_cv; - + /** @brief The value written (for write or RMW; undefined for read) */ uint64_t value; diff --git a/classlist.h b/classlist.h index 24c635fd..e6a5e4ec 100644 --- a/classlist.h +++ b/classlist.h @@ -9,8 +9,6 @@ class ModelAction; class ModelChecker; class ModelExecution; class ModelHistory; -class Node; -class NodeStack; class Scheduler; class Thread; class TraceAnalysis; diff --git a/execution.cc b/execution.cc index e3a0a855..d22f628d 100644 --- a/execution.cc +++ b/execution.cc @@ -6,7 +6,6 @@ #include "model.h" #include "execution.h" #include "action.h" -#include "nodestack.h" #include "schedule.h" #include "common.h" #include "clockvector.h" @@ -48,7 +47,7 @@ struct model_snapshot_members { }; /** @brief Constructor */ -ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) : +ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : model(m), params(NULL), scheduler(scheduler), @@ -62,7 +61,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack mutex_map(), thrd_last_action(1), thrd_last_fence_release(), - node_stack(node_stack), priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), fuzzer(new Fuzzer()) @@ -71,7 +69,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack model_thread = new Thread(get_next_id()); add_thread(model_thread); scheduler->register_engine(this); - node_stack->register_engine(this); } /** @brief Destructor */ @@ -522,8 +519,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr) /** * Initialize the current action by performing one or more of the following - * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward - * in the NodeStack, manipulating backtracking sets, allocating and + * actions, as appropriate: merging RMWR and RMWC/RMW actions, + * manipulating backtracking sets, allocating and * initializing clock vectors, and computing the promises to fulfill. * * @param curr The current action, as passed from the user context; may be @@ -543,7 +540,6 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) ModelAction *newcurr = *curr; newcurr->set_seq_number(get_next_seq_num()); - node_stack->add_action(newcurr); /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); @@ -1343,18 +1339,17 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu /** * @brief Get an action representing an uninitialized atomic * - * This function may create a new one or try to retrieve one from the NodeStack + * This function may create a new one. * * @param curr The current action, which prompts the creation of an UNINIT action * @return A pointer to the UNINIT ModelAction */ -ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const +ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const { - Node *node = curr->get_node(); - ModelAction *act = node->get_uninit_action(); + ModelAction *act = curr->get_uninit_action(); if (!act) { act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread); - node->set_uninit_action(act); + curr->set_uninit_action(act); } act->create_cv(NULL); return act; diff --git a/execution.h b/execution.h index c87a20fe..03b9faeb 100644 --- a/execution.h +++ b/execution.h @@ -32,7 +32,7 @@ struct PendingFutureValue { /** @brief The central structure for model-checking */ class ModelExecution { public: - ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack); + ModelExecution(ModelChecker *m, Scheduler *scheduler); ~ModelExecution(); struct model_params * get_params() const { return params; } @@ -125,7 +125,7 @@ private: bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector *priorset, bool *canprune); void w_modification_order(ModelAction *curr); ClockVector * get_hb_from_write(ModelAction *rf) const; - ModelAction * get_uninitialized_action(const ModelAction *curr) const; + ModelAction * get_uninitialized_action(ModelAction *curr) const; action_list_t action_trace; SnapVector thread_map; @@ -154,7 +154,6 @@ private: SnapVector thrd_last_action; SnapVector thrd_last_fence_release; - NodeStack * const node_stack; /** A special model-checker Thread; used for associating with * model-checker-related ModelAcitons */ diff --git a/fuzzer.cc b/fuzzer.cc index 9ad61c3c..5b174b15 100644 --- a/fuzzer.cc +++ b/fuzzer.cc @@ -8,7 +8,7 @@ int Fuzzer::selectWrite(ModelAction *read, SnapVector * rf_set) { return random_index; } -Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) { +Thread * Fuzzer::selectThread(int * threadlist, int numthreads) { int random_index = random() % numthreads; int thread = threadlist[random_index]; thread_id_t curr_tid = int_to_id(thread); diff --git a/fuzzer.h b/fuzzer.h index 6cf1efba..572190e1 100644 --- a/fuzzer.h +++ b/fuzzer.h @@ -8,7 +8,7 @@ class Fuzzer { public: Fuzzer() {} int selectWrite(ModelAction *read, SnapVector* rf_set); - Thread * selectThread(Node *n, int * threadlist, int numthreads); + Thread * selectThread(int * threadlist, int numthreads); Thread * selectNotify(action_list_t * waiters); MEMALLOC private: diff --git a/model.cc b/model.cc index 8454d0fb..3b4784d2 100644 --- a/model.cc +++ b/model.cc @@ -7,7 +7,6 @@ #include "model.h" #include "action.h" -#include "nodestack.h" #include "schedule.h" #include "snapshot-interface.h" #include "common.h" @@ -34,8 +33,7 @@ ModelChecker::ModelChecker() : params(), restart_flag(false), scheduler(new Scheduler()), - node_stack(new NodeStack()), - execution(new ModelExecution(this, scheduler, node_stack)), + execution(new ModelExecution(this, scheduler)), history(new ModelHistory()), execution_number(1), trace_analyses(), @@ -52,7 +50,6 @@ ModelChecker::ModelChecker() : /** @brief Destructor */ ModelChecker::~ModelChecker() { - delete node_stack; delete scheduler; } @@ -114,7 +111,7 @@ Thread * ModelChecker::get_next_thread() * Have we completed exploring the preselected path? Then let the * scheduler decide */ - return scheduler->select_next_thread(node_stack->get_head()); + return scheduler->select_next_thread(); } /** diff --git a/model.h b/model.h index 1269e76e..be9c86af 100644 --- a/model.h +++ b/model.h @@ -73,7 +73,6 @@ private: /** The scheduler to use: tracks the running/ready Threads */ Scheduler * const scheduler; - NodeStack * const node_stack; ModelExecution *execution; Thread * init_thread; ModelHistory *history; diff --git a/nodestack.cc b/nodestack.cc deleted file mode 100644 index 258c2758..00000000 --- a/nodestack.cc +++ /dev/null @@ -1,131 +0,0 @@ -#define __STDC_FORMAT_MACROS -#include -#include - -#include - -#include "nodestack.h" -#include "action.h" -#include "common.h" -#include "threads-model.h" -#include "modeltypes.h" -#include "execution.h" -#include "params.h" - -/** - * @brief Node constructor - * - * Constructs a single Node for use in a NodeStack. Each Node is associated - * with exactly one ModelAction (exception: the first Node should be created - * as an empty stub, to represent the first thread "choice") and up to one - * parent. - * - * @param act The ModelAction to associate with this Node. May be NULL. - * @param nthreads The number of threads which exist at this point in the - * execution trace. - */ -Node::Node(ModelAction *act) : - action(act), - uninit_action(NULL) -{ - ASSERT(act); - act->set_node(this); -} - -/** @brief Node desctructor */ -Node::~Node() -{ - delete action; - if (uninit_action) - delete uninit_action; -} - -/** Prints debugging info for the ModelAction associated with this Node */ -void Node::print() const -{ - action->print(); -} - -NodeStack::NodeStack() : - node_list(), - head_idx(-1) -{ -} - -NodeStack::~NodeStack() -{ - for (unsigned int i = 0;i < node_list.size();i++) - delete node_list[i]; -} - -/** - * @brief Register the model-checker object with this NodeStack - * @param exec The execution structure for the ModelChecker - */ -void NodeStack::register_engine(const ModelExecution *exec) -{ - this->execution = exec; -} - -const struct model_params * NodeStack::get_params() const -{ - return execution->get_params(); -} - -void NodeStack::print() const -{ - model_print("............................................\n"); - model_print("NodeStack printing node_list:\n"); - for (unsigned int it = 0;it < node_list.size();it++) { - if ((int)it == this->head_idx) - model_print("vvv following action is the current iterator vvv\n"); - node_list[it]->print(); - } - model_print("............................................\n"); -} - -/** Note: The is_enabled set contains what actions were enabled when - * act was chosen. */ -void NodeStack::add_action(ModelAction *act) -{ - DBG(); - - node_list.push_back(new Node(act)); - head_idx++; -} - - -/** Reset the node stack. */ -void NodeStack::full_reset() -{ - for (unsigned int i = 0;i < node_list.size();i++) - delete node_list[i]; - node_list.clear(); - reset_execution(); -} - -Node * NodeStack::get_head() const -{ - if (node_list.empty() || head_idx < 0) - return NULL; - return node_list[head_idx]; -} - -Node * NodeStack::get_next() const -{ - if (node_list.empty()) { - DEBUG("Empty\n"); - return NULL; - } - unsigned int it = head_idx + 1; - if (it == node_list.size()) { - DEBUG("At end\n"); - return NULL; - } - return node_list[it]; -} - -void NodeStack::reset_execution() -{ - head_idx = -1; -} diff --git a/nodestack.h b/nodestack.h deleted file mode 100644 index 4efd6029..00000000 --- a/nodestack.h +++ /dev/null @@ -1,83 +0,0 @@ -/** @file nodestack.h - * @brief Stack of operations for use in backtracking. - */ - -#ifndef __NODESTACK_H__ -#define __NODESTACK_H__ - -#include -#include - -#include "mymemory.h" -#include "schedule.h" -#include "stl-model.h" -#include "classlist.h" - -/** - * @brief A single node in a NodeStack - * - * Represents a single node in the NodeStack. Each Node is associated with up - * to one action and up to one parent node. A node holds information - * regarding the last action performed (the "associated action"), the thread - * choices that have been explored (explored_children) and should be explored - * (backtrack), and the actions that the last action may read from. - */ -class Node { -public: - Node(ModelAction *act); - ~Node(); - - ModelAction * get_action() const { return action; } - void set_uninit_action(ModelAction *act) { uninit_action = act; } - ModelAction * get_uninit_action() const { return uninit_action; } - void print() const; - - SNAPSHOTALLOC -private: - ModelAction * const action; - - /** @brief ATOMIC_UNINIT action which was created at this Node */ - ModelAction *uninit_action; -}; - -typedef SnapVector node_list_t; - -/** - * @brief A stack of nodes - * - * Holds a Node linked-list that can be used for holding backtracking, - * may-read-from, and replay information. It is used primarily as a - * stack-like structure, in that backtracking points and replay nodes are - * only removed from the top (most recent). - */ -class NodeStack { -public: - NodeStack(); - ~NodeStack(); - - void register_engine(const ModelExecution *exec); - void add_action(ModelAction *act); - Node * get_head() const; - Node * get_next() const; - void reset_execution(); - void full_reset(); - void print() const; - - SNAPSHOTALLOC -private: - node_list_t node_list; - const struct model_params * get_params() const; - - /** @brief The model-checker execution object */ - const ModelExecution *execution; - - /** - * @brief the index position of the current head Node - * - * This index is relative to node_list. The index should point to the - * current head Node. It is negative when the list is empty. - */ - int head_idx; -}; - -#endif /* __NODESTACK_H__ */ diff --git a/schedule.cc b/schedule.cc index 59a6e3a4..cb97d5bd 100644 --- a/schedule.cc +++ b/schedule.cc @@ -5,7 +5,6 @@ #include "schedule.h" #include "common.h" #include "model.h" -#include "nodestack.h" #include "execution.h" #include "fuzzer.h" @@ -197,12 +196,10 @@ void Scheduler::wake(Thread *t) /** * @brief Select a Thread to run via round-robin * - * @param n The current Node, holding priority information for the next thread - * selection * * @return The next Thread to run */ -Thread * Scheduler::select_next_thread(Node *n) +Thread * Scheduler::select_next_thread() { int avail_threads = 0; int thread_list[enabled_len]; @@ -214,7 +211,7 @@ Thread * Scheduler::select_next_thread(Node *n) if (avail_threads == 0) return NULL;// No threads availablex - Thread * thread = execution->getFuzzer()->selectThread(n, thread_list, avail_threads); + Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads); curr_thread_index = id_to_int(thread->get_id()); return thread; } diff --git a/schedule.h b/schedule.h index 49bd41f3..f9660232 100644 --- a/schedule.h +++ b/schedule.h @@ -28,7 +28,7 @@ public: void remove_thread(Thread *t); void sleep(Thread *t); void wake(Thread *t); - Thread * select_next_thread(Node *n); + Thread * select_next_thread(); void set_current_thread(Thread *t); Thread * get_current_thread() const; void print() const; -- 2.34.1