X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.h;h=3cffac9c9b2219905020262302f4c580f9f03784;hp=8df67838c87c362518bdd3100bddcd4663254475;hb=5f5f526a141aa4727cb37920212623c8afffa1f6;hpb=e00292b5adf2b85eb1c6e2399159b5c28fde48eb diff --git a/nodestack.h b/nodestack.h index 8df6783..3cffac9 100644 --- a/nodestack.h +++ b/nodestack.h @@ -5,32 +5,16 @@ #ifndef __NODESTACK_H__ #define __NODESTACK_H__ -#include #include #include -#include "threads.h" +#include + #include "mymemory.h" -#include "clockvector.h" +#include "schedule.h" +#include "promise.h" class ModelAction; - -/** - * 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.
- */ -typedef enum { - PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */ - PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */ - PROMISE_FULFILLED /**< This promise is applicable and fulfilled */ -} promise_t; - -struct future_value { - uint64_t value; - modelclock_t expiration; -}; +class Thread; struct fairness_info { unsigned int enabled_count; @@ -38,6 +22,12 @@ struct fairness_info { bool priority; }; +typedef enum { + READ_FROM_PAST, + READ_FROM_PROMISE, + READ_FROM_FUTURE, + READ_FROM_NONE, +} read_from_type_t; /** * @brief A single node in a NodeStack @@ -50,69 +40,110 @@ struct fairness_info { */ class Node { public: - Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL); + Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness); ~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(); + bool backtrack_empty() const; - void explore_child(ModelAction *act, bool * is_enabled); + void clear_backtracking(); + 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); - bool is_enabled(thread_id_t tid); - ModelAction * get_action() { return action; } - bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;} - int get_num_threads() {return num_threads;} + 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(); - modelclock_t get_future_value_expiration(); - bool increment_future_value(); - bool future_value_empty(); - - void add_read_from(const ModelAction *act); - const ModelAction * get_read_from(); + read_from_type_t get_read_from_status(); bool increment_read_from(); - bool read_from_empty(); - int get_read_from_size(); - const ModelAction * get_read_from_at(int i); + bool read_from_empty() const; + unsigned int read_from_size() const; + + void print_read_from_past(); + void add_read_from_past(const ModelAction *act); + const ModelAction * get_read_from_past() const; + const ModelAction * get_read_from_past(int i) const; + int get_read_from_past_size() const; + + void add_read_from_promise(const ModelAction *reader); + Promise * get_read_from_promise() const; + Promise * get_read_from_promise(int i) const; + int get_read_from_promise_size() const; + + bool add_future_value(struct future_value fv); + struct future_value get_future_value() const; void set_promise(unsigned int i); - bool get_promise(unsigned int i); + bool get_promise(unsigned int i) const; bool increment_promise(); - bool promise_empty(); + bool promise_empty() const; + void clear_promise_resolutions(); + + enabled_type_t *get_enabled_array() {return enabled_array;} - void print(); - void print_may_read_from(); + 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() const; MEMALLOC private: void explore(thread_id_t tid); - ModelAction *action; - Node *parent; - int num_threads; + bool read_from_past_empty() const; + bool increment_read_from_past(); + bool read_from_promise_empty() const; + bool increment_read_from_promise(); + bool future_value_empty() const; + bool increment_future_value(); + read_from_type_t read_from_status; + + ModelAction * const action; + Node * const parent; + const 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; - bool *enabled_array; + 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; + /** + * The set of past 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 * > > read_from_past; + unsigned int read_from_past_idx; - unsigned int read_from_index; + std::vector< const ModelAction *, ModelAlloc > read_from_promises; + int read_from_promise_idx; std::vector< struct future_value, ModelAlloc > future_values; - std::vector< promise_t, ModelAlloc > promises; int future_index; + + std::vector< bool, ModelAlloc > resolve_promise; + int resolve_promise_idx; + + std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; + int relseq_break_index; + + int misc_index; + int misc_max; }; typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t; @@ -129,19 +160,26 @@ class NodeStack { public: NodeStack(); ~NodeStack(); - ModelAction * explore_action(ModelAction *act, bool * is_enabled); - 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; - unsigned int 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. It is negative when the list is empty. + */ + int head_idx; int total_nodes; };