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 /**
  26  * @brief A single node in a NodeStack
  27  *
  28  * Represents a single node in the NodeStack. Each Node is associated with up
  29  * to one action and up to one parent node. A node holds information
  30  * regarding the last action performed (the "associated action"), the thread
  31  * choices that have been explored (explored_children) and should be explored
  32  * (backtrack), and the actions that the last action may read from.
  33  */
  34 class Node {
  35 public:
  36         Node(const struct model_params *params, ModelAction *act, Node *par,
  37                         int nthreads);
  38         ~Node();
  39
  40         bool is_enabled(Thread *t) const;
  41         bool is_enabled(thread_id_t tid) const;
  42         enabled_type_t enabled_status(thread_id_t tid) const;
  43
  44         ModelAction * get_action() const { return action; }
  45         void set_uninit_action(ModelAction *act) { uninit_action = act; }
  46         ModelAction * get_uninit_action() const { return uninit_action; }
  47
  48         bool has_priority(thread_id_t tid) const;
  49         void update_yield(Scheduler *);
  50         bool has_priority_over(thread_id_t tid, thread_id_t tid2) const;
  51         int get_num_threads() const { return num_threads; }
  52         /** @return the parent Node to this Node; that is, the action that
  53          * occurred previously in the stack. */
  54         Node * get_parent() const { return parent; }
  55
  56
  57
  58         void print() const;
  59
  60         MEMALLOC
  61 private:
  62         const struct model_params * get_params() const { return params; }
  63         ModelAction * const action;
  64         const struct model_params * const params;
  65
  66         /** @brief ATOMIC_UNINIT action which was created at this Node */
  67         ModelAction *uninit_action;
  68         Node * const parent;
  69         const int num_threads;
  70 };
  71
  72 typedef ModelVector<Node *> node_list_t;
  73
  74 /**
  75  * @brief A stack of nodes
  76  *
  77  * Holds a Node linked-list that can be used for holding backtracking,
  78  * may-read-from, and replay information. It is used primarily as a
  79  * stack-like structure, in that backtracking points and replay nodes are
  80  * only removed from the top (most recent).
  81  */
  82 class NodeStack {
  83 public:
  84         NodeStack();
  85         ~NodeStack();
  86
  87         void register_engine(const ModelExecution *exec);
  88
  89         ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled);
  90         Node * get_head() const;
  91         Node * get_next() const;
  92         void reset_execution();
  93         void full_reset();
  94         int get_total_nodes() { return total_nodes; }
  95
  96         void print() const;
  97
  98         MEMALLOC
  99 private:
 100         node_list_t node_list;
 101
 102         const struct model_params * get_params() const;
 103
 104         /** @brief The model-checker execution object */
 105         const ModelExecution *execution;
 106
 107         /**
 108          * @brief the index position of the current head Node
 109          *
 110          * This index is relative to node_list. The index should point to the
 111          * current head Node. It is negative when the list is empty.
 112          */
 113         int head_idx;
 114
 115         int total_nodes;
 116 };
 117
 118 #endif /* __NODESTACK_H__ */