nodestack.h

   1 /** @file nodestack.h
   2  *  @brief Stack of operations for use in backtracking.
   3 */
   4
   5 #ifndef __NODESTACK_H__
   6 #define __NODESTACK_H__
   7
   8 #include <list>
   9 #include <vector>
  10 #include <cstddef>
  11 #include <inttypes.h>
  12
  13 #include "mymemory.h"
  14 #include "modeltypes.h"
  15 #include "schedule.h"
  16
  17 class ModelAction;
  18 class Thread;
  19
  20 /**
  21  * A flag used for the promise counting/combination problem within a node,
  22  * denoting whether a particular Promise is
  23  * <ol><li>@b applicable: can be satisfied by this Node's ModelAction and</li>
  24  * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
  25  * configuration.</li></ol>
  26  */
  27 typedef enum {
  28         PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */
  29         PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */
  30         PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
  31 } promise_t;
  32
  33 struct future_value {
  34         uint64_t value;
  35         modelclock_t expiration;
  36 };
  37
  38 struct fairness_info {
  39         unsigned int enabled_count;
  40         unsigned int turns;
  41         bool priority;
  42 };
  43
  44
  45 /**
  46  * @brief A single node in a NodeStack
  47  *
  48  * Represents a single node in the NodeStack. Each Node is associated with up
  49  * to one action and up to one parent node. A node holds information
  50  * regarding the last action performed (the "associated action"), the thread
  51  * choices that have been explored (explored_children) and should be explored
  52  * (backtrack), and the actions that the last action may read from.
  53  */
  54 class Node {
  55 public:
  56         Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL);
  57         ~Node();
  58         /* return true = thread choice has already been explored */
  59         bool has_been_explored(thread_id_t tid);
  60         /* return true = backtrack set is empty */
  61         bool backtrack_empty();
  62
  63         void explore_child(ModelAction *act, enabled_type_t * is_enabled);
  64         /* return false = thread was already in backtrack */
  65         bool set_backtrack(thread_id_t id);
  66         thread_id_t get_next_backtrack();
  67         bool is_enabled(Thread *t);
  68         bool is_enabled(thread_id_t tid);
  69         ModelAction * get_action() { return action; }
  70         bool has_priority(thread_id_t tid);
  71         int get_num_threads() {return num_threads;}
  72         /** @return the parent Node to this Node; that is, the action that
  73          * occurred previously in the stack. */
  74         Node * get_parent() const { return parent; }
  75
  76         bool add_future_value(uint64_t value, modelclock_t expiration);
  77         uint64_t get_future_value();
  78         modelclock_t get_future_value_expiration();
  79         bool increment_future_value();
  80         bool future_value_empty();
  81
  82         void add_read_from(const ModelAction *act);
  83         const ModelAction * get_read_from();
  84         bool increment_read_from();
  85         bool read_from_empty();
  86         int get_read_from_size();
  87         const ModelAction * get_read_from_at(int i);
  88
  89         void set_promise(unsigned int i);
  90         bool get_promise(unsigned int i);
  91         bool increment_promise();
  92         bool promise_empty();
  93         enabled_type_t *get_enabled_array() {return enabled_array;}
  94
  95         void add_relseq_break(const ModelAction *write);
  96         const ModelAction * get_relseq_break();
  97         bool increment_relseq_break();
  98         bool relseq_break_empty();
  99
 100         void print();
 101         void print_may_read_from();
 102
 103         MEMALLOC
 104 private:
 105         void explore(thread_id_t tid);
 106
 107         ModelAction *action;
 108         Node *parent;
 109         int num_threads;
 110         std::vector< bool, ModelAlloc<bool> > explored_children;
 111         std::vector< bool, ModelAlloc<bool> > backtrack;
 112         std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness;
 113         int numBacktracks;
 114         enabled_type_t *enabled_array;
 115
 116         /** The set of ModelActions that this the action at this Node may read
 117          *  from. Only meaningful if this Node represents a 'read' action. */
 118         std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > may_read_from;
 119
 120         unsigned int read_from_index;
 121
 122         std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
 123         std::vector< promise_t, ModelAlloc<promise_t> > promises;
 124         int future_index;
 125
 126         std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > relseq_break_writes;
 127         int relseq_break_index;
 128 };
 129
 130 typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;
 131
 132 /**
 133  * @brief A stack of nodes
 134  *
 135  * Holds a Node linked-list that can be used for holding backtracking,
 136  * may-read-from, and replay information. It is used primarily as a
 137  * stack-like structure, in that backtracking points and replay nodes are
 138  * only removed from the top (most recent).
 139  */
 140 class NodeStack {
 141 public:
 142         NodeStack();
 143         ~NodeStack();
 144         ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled);
 145         Node * get_head();
 146         Node * get_next();
 147         void reset_execution();
 148         void pop_restofstack(int numAhead);
 149         int get_total_nodes() { return total_nodes; }
 150
 151         void print();
 152
 153         MEMALLOC
 154 private:
 155         node_list_t node_list;
 156         unsigned int iter;
 157
 158         int total_nodes;
 159 };
 160
 161 #endif /* __NODESTACK_H__ */