X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=4efd60292e24175f0aa3cfc7544a5eeab4904328;hb=edaaf79d36b5e9de06881591a42b799c5de0f59a;hp=b7e630b0ba4dc6d5b7957f48ab90f35e5ee933a6;hpb=51d58655a9a674d5e4b04f2dfcb5204a4342ef6d;p=c11tester.git diff --git a/nodestack.h b/nodestack.h index b7e630b0..4efd6029 100644 --- a/nodestack.h +++ b/nodestack.h @@ -1,6 +1,6 @@ /** @file nodestack.h * @brief Stack of operations for use in backtracking. -*/ + */ #ifndef __NODESTACK_H__ #define __NODESTACK_H__ @@ -11,34 +11,7 @@ #include "mymemory.h" #include "schedule.h" #include "stl-model.h" - -class ModelAction; -class Thread; - -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, /**< @brief Read from a prior, existing store */ - 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) - +#include "classlist.h" /** * @brief A single node in a NodeStack @@ -51,104 +24,23 @@ typedef enum { */ class Node { public: - Node(const struct model_params *params, ModelAction *act, Node *par, - int nthreads, Node *prevfairness); + 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 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) 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; } 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; } - - read_from_type_t get_read_from_status(); - bool increment_read_from(); - 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; - - 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; - - bool increment_behaviors(); - void print() const; - MEMALLOC + SNAPSHOTALLOC 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 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; - ModelVector explored_children; - ModelVector backtrack; - ModelVector fairness; - int numBacktracks; - enabled_type_t *enabled_array; - - /** - * The set of past ModelActions that this the action at this Node may - * read from. Only meaningful if this Node represents a 'read' action. - */ - ModelVector read_from_past; - unsigned int read_from_past_idx; - - ModelVector relseq_break_writes; - int relseq_break_index; - - int misc_index; - int misc_max; - int * yield_data; }; -typedef ModelVector node_list_t; +typedef SnapVector node_list_t; /** * @brief A stack of nodes @@ -164,21 +56,16 @@ public: ~NodeStack(); void register_engine(const ModelExecution *exec); - - ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled); + void add_action(ModelAction *act); Node * get_head() const; Node * get_next() const; void reset_execution(); - void pop_restofstack(int numAhead); void full_reset(); - int get_total_nodes() { return total_nodes; } - void print() const; - MEMALLOC + SNAPSHOTALLOC private: node_list_t node_list; - const struct model_params * get_params() const; /** @brief The model-checker execution object */ @@ -191,8 +78,6 @@ private: * current head Node. It is negative when the list is empty. */ int head_idx; - - int total_nodes; }; -#endif /* __NODESTACK_H__ */ +#endif /* __NODESTACK_H__ */