X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.h;h=47c0272f95fa917e8710235fa0d56b02194a4d08;hp=47c72678aa13cffb9294e6a7d842860136e37baf;hb=7524803854c2de38c0311fe5037e3c17105ccfaa;hpb=9aae08ba6d60aa253039d2da1c3571fdde2ac159 diff --git a/nodestack.h b/nodestack.h index 47c7267..47c0272 100644 --- a/nodestack.h +++ b/nodestack.h @@ -5,7 +5,7 @@ #ifndef __NODESTACK_H__ #define __NODESTACK_H__ -#include +#include "stl_wrappers.h" #include #include @@ -16,28 +16,26 @@ 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 fairness_info { unsigned int enabled_count; unsigned int turns; bool priority; }; +typedef enum { + READ_FROM_PAST, + READ_FROM_PROMISE, + READ_FROM_FUTURE, + READ_FROM_NONE, +} read_from_type_t; + +#define YIELD_E 1 +#define YIELD_D 2 +#define YIELD_S 4 +#define YIELD_P 8 +#define YIELD_INDEX(tid1, tid2, num_threads) (tid1*num_threads+tid2) + + /** * @brief A single node in a NodeStack * @@ -56,6 +54,7 @@ public: /* return true = backtrack set is empty */ bool backtrack_empty() const; + 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); @@ -65,28 +64,42 @@ public: enabled_type_t enabled_status(thread_id_t tid) const; ModelAction * get_action() const { return action; } + void set_uninit_action(ModelAction *act) { uninit_action = act; } + ModelAction * get_uninit_action() const { return uninit_action; } + bool has_priority(thread_id_t tid) const; + void update_yield(Scheduler *); + bool has_priority_over(thread_id_t tid, thread_id_t tid2) 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(struct future_value& fv); - struct future_value get_future_value() const; - bool increment_future_value(); - bool future_value_empty() const; - - void add_read_from(const ModelAction *act); - const ModelAction * get_read_from() const; + read_from_type_t get_read_from_status(); bool increment_read_from(); bool read_from_empty() const; - int get_read_from_size() const; - const ModelAction * get_read_from_at(int i) const; + unsigned int read_from_size() const; - void set_promise(unsigned int i, bool is_rmw); + 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) const; bool increment_promise(); bool promise_empty() const; + void clear_promise_resolutions(); + enabled_type_t *get_enabled_array() {return enabled_array;} void set_misc_max(int i); @@ -100,13 +113,24 @@ public: bool relseq_break_empty() const; void print() const; - void print_may_read_from(); MEMALLOC private: void explore(thread_id_t tid); + int get_yield_data(int tid1, int tid2) const; + 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; + + /** @brief ATOMIC_UNINIT action which was created at this Node */ + ModelAction *uninit_action; + Node * const parent; const int num_threads; std::vector< bool, ModelAlloc > explored_children; @@ -115,24 +139,31 @@ private: 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; + /** + * 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; + int * yield_data; }; -typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t; +typedef model_vector< Node * > node_list_t; /** * @brief A stack of nodes