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 <cstddef>
   9 #include <inttypes.h>
  10
  11 #include "mymemory.h"
  12 #include "schedule.h"
  13 #include "stl-model.h"
  14
  15 class ModelAction;
  16 class Thread;
  17
  18 struct fairness_info {
  19         unsigned int enabled_count;
  20         unsigned int turns;
  21         bool priority;
  22 };
  23
  24 /**
  25  * @brief Types of read-from relations
  26  *
  27  * Our "may-read-from" set is composed of multiple types of reads, and we have
  28  * to iterate through all of them in the backtracking search. This enumeration
  29  * helps to identify which type of read-from we are currently observing.
  30  */
  31 typedef enum {
  32         READ_FROM_PAST, /**< @brief Read from a prior, existing store */
  33         READ_FROM_NONE, /**< @brief A NULL state, which should not be reached */
  34 } read_from_type_t;
  35
  36 #define YIELD_E 1
  37 #define YIELD_D 2
  38 #define YIELD_S 4
  39 #define YIELD_P 8
  40 #define YIELD_INDEX(tid1, tid2, num_threads) (tid1*num_threads+tid2)
  41
  42
  43 /**
  44  * @brief A single node in a NodeStack
  45  *
  46  * Represents a single node in the NodeStack. Each Node is associated with up
  47  * to one action and up to one parent node. A node holds information
  48  * regarding the last action performed (the "associated action"), the thread
  49  * choices that have been explored (explored_children) and should be explored
  50  * (backtrack), and the actions that the last action may read from.
  51  */
  52 class Node {
  53 public:
  54         Node(const struct model_params *params, ModelAction *act, Node *par,
  55                         int nthreads, Node *prevfairness);
  56         ~Node();
  57         /* return true = thread choice has already been explored */
  58         bool has_been_explored(thread_id_t tid) const;
  59         /* return true = backtrack set is empty */
  60         bool backtrack_empty() const;
  61
  62         void clear_backtracking();
  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) const;
  68         bool is_enabled(thread_id_t tid) const;
  69         enabled_type_t enabled_status(thread_id_t tid) const;
  70
  71         ModelAction * get_action() const { return action; }
  72         void set_uninit_action(ModelAction *act) { uninit_action = act; }
  73         ModelAction * get_uninit_action() const { return uninit_action; }
  74
  75         bool has_priority(thread_id_t tid) const;
  76         void update_yield(Scheduler *);
  77         bool has_priority_over(thread_id_t tid, thread_id_t tid2) const;
  78         int get_num_threads() const { return num_threads; }
  79         /** @return the parent Node to this Node; that is, the action that
  80          * occurred previously in the stack. */
  81         Node * get_parent() const { return parent; }
  82
  83         read_from_type_t get_read_from_status();
  84         bool increment_read_from();
  85         bool read_from_empty() const;
  86         unsigned int read_from_size() const;
  87
  88         void print_read_from_past();
  89         void add_read_from_past(const ModelAction *act);
  90         const ModelAction * get_read_from_past() const;
  91         const ModelAction * get_read_from_past(int i) const;
  92         int get_read_from_past_size() const;
  93
  94         enabled_type_t *get_enabled_array() {return enabled_array;}
  95
  96         void set_misc_max(int i);
  97         int get_misc() const;
  98         bool increment_misc();
  99         bool misc_empty() const;
 100
 101         void add_relseq_break(const ModelAction *write);
 102         const ModelAction * get_relseq_break() const;
 103         bool increment_relseq_break();
 104         bool relseq_break_empty() const;
 105
 106         bool increment_behaviors();
 107
 108         void print() const;
 109
 110         MEMALLOC
 111 private:
 112         void explore(thread_id_t tid);
 113         int get_yield_data(int tid1, int tid2) const;
 114         bool read_from_past_empty() const;
 115         bool increment_read_from_past();
 116         bool future_value_empty() const;
 117         bool increment_future_value();
 118         read_from_type_t read_from_status;
 119         const struct model_params * get_params() const { return params; }
 120
 121         ModelAction * const action;
 122
 123         const struct model_params * const params;
 124
 125         /** @brief ATOMIC_UNINIT action which was created at this Node */
 126         ModelAction *uninit_action;
 127
 128         Node * const parent;
 129         const int num_threads;
 130         ModelVector<bool> explored_children;
 131         ModelVector<bool> backtrack;
 132         ModelVector<struct fairness_info> fairness;
 133         int numBacktracks;
 134         enabled_type_t *enabled_array;
 135
 136         /**
 137          * The set of past ModelActions that this the action at this Node may
 138          * read from. Only meaningful if this Node represents a 'read' action.
 139          */
 140         ModelVector<const ModelAction *> read_from_past;
 141         unsigned int read_from_past_idx;
 142
 143         ModelVector<const ModelAction *> relseq_break_writes;
 144         int relseq_break_index;
 145
 146         int misc_index;
 147         int misc_max;
 148         int * yield_data;
 149 };
 150
 151 typedef ModelVector<Node *> node_list_t;
 152
 153 /**
 154  * @brief A stack of nodes
 155  *
 156  * Holds a Node linked-list that can be used for holding backtracking,
 157  * may-read-from, and replay information. It is used primarily as a
 158  * stack-like structure, in that backtracking points and replay nodes are
 159  * only removed from the top (most recent).
 160  */
 161 class NodeStack {
 162 public:
 163         NodeStack();
 164         ~NodeStack();
 165
 166         void register_engine(const ModelExecution *exec);
 167
 168         ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled);
 169         Node * get_head() const;
 170         Node * get_next() const;
 171         void reset_execution();
 172         void pop_restofstack(int numAhead);
 173         void full_reset();
 174         int get_total_nodes() { return total_nodes; }
 175
 176         void print() const;
 177
 178         MEMALLOC
 179 private:
 180         node_list_t node_list;
 181
 182         const struct model_params * get_params() const;
 183
 184         /** @brief The model-checker execution object */
 185         const ModelExecution *execution;
 186
 187         /**
 188          * @brief the index position of the current head Node
 189          *
 190          * This index is relative to node_list. The index should point to the
 191          * current head Node. It is negative when the list is empty.
 192          */
 193         int head_idx;
 194
 195         int total_nodes;
 196 };
 197
 198 #endif /* __NODESTACK_H__ */