X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=f26100bad0e359459bf18263009028aa8a28f4e0;hb=2d0d4ac38e05905a6633b3f2d5112ccadd45c27f;hp=8a20c45cb2c03e53bdeaf53ee8e80a89b3882014;hpb=7bd9b5a1446863dc1a9de9683476f5a480dfba91;p=model-checker.git diff --git a/nodestack.h b/nodestack.h index 8a20c45..f26100b 100644 --- a/nodestack.h +++ b/nodestack.h @@ -5,46 +5,44 @@ #ifndef __NODESTACK_H__ #define __NODESTACK_H__ -#include #include #include #include "mymemory.h" #include "schedule.h" #include "promise.h" +#include "stl-model.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 fairness_info { unsigned int enabled_count; unsigned int turns; bool priority; }; +/** + * @brief Types of read-from relations + * + * Our "may-read-from" set is composed of multiple types of reads, and we have + * to iterate through all of them in the backtracking search. This enumeration + * helps to identify which type of read-from we are currently observing. + */ typedef enum { - READ_FROM_PAST, - READ_FROM_PROMISE, - READ_FROM_FUTURE, - READ_FROM_NONE, + READ_FROM_PAST, /**< @brief Read from a prior, existing store */ + READ_FROM_PROMISE, /**< @brief Read from an existing promised future value */ + READ_FROM_FUTURE, /**< @brief Read from a newly-asserted future value */ + READ_FROM_NONE, /**< @brief A NULL state, which should not be reached */ } 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,7 +54,8 @@ typedef enum { */ class Node { public: - Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness); + Node(const struct model_params *params, 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) const; @@ -73,7 +72,12 @@ 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. */ @@ -91,15 +95,19 @@ public: int get_read_from_past_size() const; void add_read_from_promise(const ModelAction *reader); - const Promise * get_read_from_promise() const; + 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 is_rmw); + 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); @@ -112,12 +120,14 @@ public: bool increment_relseq_break(); bool relseq_break_empty() const; + bool increment_behaviors(); + void print() const; 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; @@ -125,13 +135,20 @@ private: bool future_value_empty() const; bool increment_future_value(); read_from_type_t read_from_status; + const struct model_params * get_params() const { return params; } ModelAction * const action; + + const struct model_params * const params; + + /** @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; - std::vector< bool, ModelAlloc > backtrack; - std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness; + ModelVector explored_children; + ModelVector backtrack; + ModelVector fairness; int numBacktracks; enabled_type_t *enabled_array; @@ -139,24 +156,27 @@ private: * 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; + ModelVector read_from_past; unsigned int read_from_past_idx; - std::vector< const ModelAction *, ModelAlloc > read_from_promises; + ModelVector read_from_promises; int read_from_promise_idx; - std::vector< struct future_value, ModelAlloc > future_values; - std::vector< promise_t, ModelAlloc > promises; + ModelVector future_values; int future_index; - std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; + ModelVector resolve_promise; + int resolve_promise_idx; + + ModelVector 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 ModelVector node_list_t; /** * @brief A stack of nodes @@ -170,6 +190,9 @@ class NodeStack { public: NodeStack(); ~NodeStack(); + + void register_engine(const ModelExecution *exec); + ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled); Node * get_head() const; Node * get_next() const; @@ -183,6 +206,11 @@ public: 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 *