get rid of nodestack
authorroot <root@dw-6.eecs.uci.edu>
Wed, 3 Jul 2019 20:36:54 +0000 (13:36 -0700)
committerroot <root@dw-6.eecs.uci.edu>
Wed, 3 Jul 2019 20:36:54 +0000 (13:36 -0700)
14 files changed:
Makefile
action.cc
action.h
classlist.h
execution.cc
execution.h
fuzzer.cc
fuzzer.h
model.cc
model.h
nodestack.cc [deleted file]
nodestack.h [deleted file]
schedule.cc
schedule.h

index 0d2af46..05afc05 100644 (file)
--- 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 \
index 8dcc9d5..0cd49cf 100644 (file)
--- 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
index 5e8b1b1..4eb1f7e 100644 (file)
--- 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;
 
index 24c635f..e6a5e4e 100644 (file)
@@ -9,8 +9,6 @@ class ModelAction;
 class ModelChecker;
 class ModelExecution;
 class ModelHistory;
-class Node;
-class NodeStack;
 class Scheduler;
 class Thread;
 class TraceAnalysis;
index e3a0a85..d22f628 100644 (file)
@@ -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<ModelAction *> *  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;
index c87a20f..03b9fae 100644 (file)
@@ -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<const ModelAction *> *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 *> thread_map;
@@ -154,7 +154,6 @@ private:
 
        SnapVector<ModelAction *> thrd_last_action;
        SnapVector<ModelAction *> thrd_last_fence_release;
-       NodeStack * const node_stack;
 
        /** A special model-checker Thread; used for associating with
         *  model-checker-related ModelAcitons */
index 9ad61c3..5b174b1 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -8,7 +8,7 @@ int Fuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * 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);
index 6cf1efb..572190e 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -8,7 +8,7 @@ class Fuzzer {
 public:
        Fuzzer() {}
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
-       Thread * selectThread(Node *n, int * threadlist, int numthreads);
+       Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
        MEMALLOC
 private:
index 8454d0f..3b4784d 100644 (file)
--- 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 1269e76..be9c86a 100644 (file)
--- 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 (file)
index 258c275..0000000
+++ /dev/null
@@ -1,131 +0,0 @@
-#define __STDC_FORMAT_MACROS
-#include <inttypes.h>
-#include <cstdlib>
-
-#include <string.h>
-
-#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 (file)
index 4efd602..0000000
+++ /dev/null
@@ -1,83 +0,0 @@
-/** @file nodestack.h
- *  @brief Stack of operations for use in backtracking.
- */
-
-#ifndef __NODESTACK_H__
-#define __NODESTACK_H__
-
-#include <cstddef>
-#include <inttypes.h>
-
-#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 *> 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__ */
index 59a6e3a..cb97d5b 100644 (file)
@@ -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;
 }
index 49bd41f..f966023 100644 (file)
@@ -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;