From: Brian Norris Date: Thu, 21 Jun 2012 07:54:01 +0000 (-0700) Subject: nodestack: add 'may_read_from' set X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8587e516d89ec5d8da43fc28b7d89fc4d65e343e;p=cdsspec-compiler.git nodestack: add 'may_read_from' set Each Node (at least, each Node that is a 'read') will be associated with a may_read_from set - the set of all possible ModelActions to read from. For now, this interface handles only actions that exist in the past. It won't properly retain information from future actions. --- diff --git a/nodestack.cc b/nodestack.cc index 65afd7c..87b3ee5 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -9,7 +9,8 @@ Node::Node(ModelAction *act, int nthreads) num_threads(nthreads), explored_children(num_threads), backtrack(num_threads), - numBacktracks(0) + numBacktracks(0), + may_read_from() { } @@ -99,6 +100,15 @@ bool Node::is_enabled(Thread *t) return id_to_int(t->get_id()) < num_threads; } +/** + * Add an action to the may_read_from set. + * @param act is the action to add + */ +void Node::add_read_from(ModelAction *act) +{ + may_read_from.insert(act); +} + void Node::explore(thread_id_t tid) { int i = id_to_int(tid); diff --git a/nodestack.h b/nodestack.h index a73ce44..74ac245 100644 --- a/nodestack.h +++ b/nodestack.h @@ -7,12 +7,15 @@ #include #include +#include #include #include "threads.h" #include "mymemory.h" class ModelAction; +typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction * > > action_set_t; + class Node { public: Node(ModelAction *act = NULL, int nthreads = 1); @@ -28,6 +31,8 @@ public: bool is_enabled(Thread *t); ModelAction * get_action() { return action; } + void add_read_from(ModelAction *act); + void print(); MEMALLOC @@ -39,6 +44,10 @@ private: std::vector< bool, MyAlloc > explored_children; std::vector< bool, MyAlloc > backtrack; int numBacktracks; + + /** The set of ModelActions that this the action at this Node may read + * from. Only meaningful if this Node represents a 'read' action. */ + action_set_t may_read_from; }; typedef std::list > node_list_t;