X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=fa356d0e9ae666db61bb993423b7b915df2c815b;hb=6904559239add5bbb227337ebb113b59c0534633;hp=44d739c9e9d752565fe76b67b4b49dce4cf778d9;hpb=24032577ab44f5adb4f072d022f70d0b0162ab90;p=c11tester.git diff --git a/nodestack.h b/nodestack.h index 44d739c9..fa356d0e 100644 --- a/nodestack.h +++ b/nodestack.h @@ -1,49 +1,17 @@ /** @file nodestack.h * @brief Stack of operations for use in backtracking. -*/ + */ #ifndef __NODESTACK_H__ #define __NODESTACK_H__ -#include -#include #include #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; -}; - +#include "stl-model.h" +#include "classlist.h" /** * @brief A single node in a NodeStack @@ -56,91 +24,23 @@ struct fairness_info { */ class Node { public: - Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 2, Node *prevfairness = NULL); + Node(ModelAction *act); ~Node(); - /* return true = thread choice has already been explored */ - bool has_been_explored(thread_id_t tid) const; - /* return true = backtrack set is empty */ - 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) 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(); + void set_uninit_action(ModelAction *act) { uninit_action = act; } + ModelAction * get_uninit_action() const { return uninit_action; } + void print() const; MEMALLOC private: - void explore(thread_id_t tid); - - ModelAction *action; - Node *parent; - int num_threads; - 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. */ - std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > may_read_from; + ModelAction * const action; - 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; + /** @brief ATOMIC_UNINIT action which was created at this Node */ + ModelAction *uninit_action; }; -typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t; +typedef ModelVector node_list_t; /** * @brief A stack of nodes @@ -154,28 +54,30 @@ class NodeStack { public: NodeStack(); ~NodeStack(); - ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled); + + void register_engine(const ModelExecution *exec); + ModelAction * explore_action(ModelAction *act); Node * get_head() const; Node * get_next() const; void reset_execution(); - void pop_restofstack(int numAhead); - int get_total_nodes() { return total_nodes; } - + void full_reset(); void print() const; MEMALLOC 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. + * current head Node. It is negative when the list is empty. */ int head_idx; - - int total_nodes; }; -#endif /* __NODESTACK_H__ */ +#endif /* __NODESTACK_H__ */