X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=nodestack.h;h=394552ca879f7056b0002acfe1ee2e5e348580f0;hp=3cffac9c9b2219905020262302f4c580f9f03784;hb=5ea8e3d5d861ed363e5ac5f3b20b8181dd197efb;hpb=5f5f526a141aa4727cb37920212623c8afffa1f6 diff --git a/nodestack.h b/nodestack.h index 3cffac9c..394552ca 100644 --- a/nodestack.h +++ b/nodestack.h @@ -12,6 +12,7 @@ #include "mymemory.h" #include "schedule.h" #include "promise.h" +#include "stl-model.h" class ModelAction; class Thread; @@ -29,6 +30,13 @@ typedef enum { 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 * @@ -57,7 +65,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. */ @@ -105,7 +118,7 @@ public: 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; @@ -115,11 +128,15 @@ private: 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; - 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; @@ -127,26 +144,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; + ModelVector future_values; int future_index; - std::vector< bool, ModelAlloc > resolve_promise; + ModelVector resolve_promise; int resolve_promise_idx; - std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; + 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