X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=44d739c9e9d752565fe76b67b4b49dce4cf778d9;hb=6bca1b36d0e9379014bea4d0b45db410b698b6f6;hp=0e952417b16c87a484712a94de4953bebc984d96;hpb=2ebb0b5a772c0bc5366c41c4980f3fd06f8081ae;p=c11tester.git diff --git a/nodestack.h b/nodestack.h index 0e952417..44d739c9 100644 --- a/nodestack.h +++ b/nodestack.h @@ -8,12 +8,42 @@ #include #include #include -#include "threads.h" +#include + #include "mymemory.h" +#include "modeltypes.h" +#include "schedule.h" class ModelAction; +class Thread; + +/** + * A flag used for the promise counting/combination problem within a node, + * denoting whether a particular Promise is + *
  1. @b applicable: can be satisfied by this Node's ModelAction and
    2. + *
  2. @b fulfilled: satisfied by this Node's ModelAction under the current + * configuration.
+ */ + +#define PROMISE_IGNORE 0 /**< This promise is inapplicable; ignore it */ +#define PROMISE_UNFULFILLED 1 /**< This promise is applicable but unfulfilled */ +#define PROMISE_FULFILLED 2 /**< This promise is applicable and fulfilled */ +#define PROMISE_MASK 0xf +#define PROMISE_RMW 0x10 + +typedef int promise_t; + +struct future_value { + uint64_t value; + modelclock_t expiration; +}; + +struct fairness_info { + unsigned int enabled_count; + unsigned int turns; + bool priority; +}; -typedef std::list< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t; /** * @brief A single node in a NodeStack @@ -26,26 +56,59 @@ typedef std::list< const ModelAction *, MyAlloc< const ModelAction * > > readfro */ class Node { public: - Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1); + Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 2, Node *prevfairness = NULL); ~Node(); /* return true = thread choice has already been explored */ - bool has_been_explored(thread_id_t tid); + bool has_been_explored(thread_id_t tid) const; /* return true = backtrack set is empty */ - bool backtrack_empty(); - void explore_child(ModelAction *act); + bool backtrack_empty() const; + + void explore_child(ModelAction *act, enabled_type_t * is_enabled); /* return false = thread was already in backtrack */ bool set_backtrack(thread_id_t id); thread_id_t get_next_backtrack(); - bool is_enabled(Thread *t); - ModelAction * get_action() { return action; } + bool is_enabled(Thread *t) const; + bool is_enabled(thread_id_t tid) const; + enabled_type_t enabled_status(thread_id_t tid) const; + ModelAction * get_action() const { return action; } + bool has_priority(thread_id_t tid) const; + int get_num_threads() const { return num_threads; } /** @return the parent Node to this Node; that is, the action that * occurred previously in the stack. */ Node * get_parent() const { return parent; } + bool add_future_value(uint64_t value, modelclock_t expiration); + uint64_t get_future_value() const; + modelclock_t get_future_value_expiration() const; + bool increment_future_value(); + bool future_value_empty() const; + void add_read_from(const ModelAction *act); + const ModelAction * get_read_from() const; + bool increment_read_from(); + bool read_from_empty() const; + int get_read_from_size() const; + const ModelAction * get_read_from_at(int i); + + void set_promise(unsigned int i, bool is_rmw); + bool get_promise(unsigned int i) const; + bool increment_promise(); + bool promise_empty() const; + enabled_type_t *get_enabled_array() {return enabled_array;} + + void set_misc_max(int i); + int get_misc() const; + bool increment_misc(); + bool misc_empty() const; + + void add_relseq_break(const ModelAction *write); + const ModelAction * get_relseq_break() const; + bool increment_relseq_break(); + bool relseq_break_empty() const; void print(); + void print_may_read_from(); MEMALLOC private: @@ -54,16 +117,30 @@ private: ModelAction *action; Node *parent; int num_threads; - std::vector< bool, MyAlloc > explored_children; - std::vector< bool, MyAlloc > backtrack; + std::vector< bool, ModelAlloc > explored_children; + std::vector< bool, ModelAlloc > backtrack; + std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness; int numBacktracks; + enabled_type_t *enabled_array; /** The set of ModelActions that this the action at this Node may read * from. Only meaningful if this Node represents a 'read' action. */ - readfrom_set_t may_read_from; + std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > may_read_from; + + unsigned int read_from_index; + + std::vector< struct future_value, ModelAlloc > future_values; + std::vector< promise_t, ModelAlloc > promises; + int future_index; + + std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; + int relseq_break_index; + + int misc_index; + int misc_max; }; -typedef std::list< Node *, MyAlloc< Node * > > node_list_t; +typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t; /** * @brief A stack of nodes @@ -77,19 +154,26 @@ class NodeStack { public: NodeStack(); ~NodeStack(); - ModelAction * explore_action(ModelAction *act); - Node * get_head(); - Node * get_next(); + ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled); + Node * get_head() const; + Node * get_next() const; void reset_execution(); - + void pop_restofstack(int numAhead); int get_total_nodes() { return total_nodes; } - void print(); + void print() const; MEMALLOC private: node_list_t node_list; - node_list_t::iterator iter; + + /** + * @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. + */ + int head_idx; int total_nodes; };