Merge branch 'norris'

diff --git a/cyclegraph.cc b/cyclegraph.cc
index f060a00e74362b6f9df99649ffd844f7e416d4b9..1eb1add33fc255e4f53e9044b3d3850b422668dd 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -2,15 +2,21 @@
 #include "action.h"
 
 /** Initializes a CycleGraph object. */
-CycleGraph::CycleGraph() {
-       hasCycles=false;
+CycleGraph::CycleGraph() :
+       hasCycles(false)
+{
 }
 
+/** CycleGraph destructor */
 CycleGraph::~CycleGraph() {
 }
 
-/** Returns the CycleNode for a given ModelAction. */
-CycleNode * CycleGraph::getNode(const ModelAction * action) {
+/**
+ * @brief Returns the CycleNode corresponding to a given ModelAction
+ * @param action The ModelAction to find a node for
+ * @return The CycleNode paired with this action
+ */
+CycleNode * CycleGraph::getNode(const ModelAction *action) {
        CycleNode *node=actionToNode.get(action);
        if (node==NULL) {
                node=new CycleNode(action);
@@ -20,8 +26,10 @@ CycleNode * CycleGraph::getNode(const ModelAction * action) {
 }
 
 /**
- * Adds an edge between two ModelActions.  The ModelAction to happens after the
- * ModelAction from.
+ * Adds an edge between two ModelActions. The ModelAction @a to is ordered
+ * after the ModelAction @a from.
+ * @param to The edge points to this ModelAction
+ * @param from The edge comes from this ModelAction
  */
 void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
        CycleNode *fromnode=getNode(from);
@@ -52,7 +60,7 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
  *  can occur in between the rmw and the from action.  Only one RMW
  *  action can read from a given write.
  */
-void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction * from) {
+void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction *from) {
        CycleNode *fromnode=getNode(from);
        CycleNode *rmwnode=getNode(rmw);
 
@@ -74,7 +82,12 @@ void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction * from) {
 }
 
 
-/** Checks whether the first CycleNode can reach the second one. */
+/**
+ * Checks whether one CycleNode can reach another.
+ * @param from The CycleNode from which to begin exploration
+ * @param to The CycleNode to reach
+ * @return True, @a from can reach @a to; otherwise, false
+ */
 bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
        std::vector<CycleNode *> queue;
        HashTable<CycleNode *, CycleNode *, uintptr_t, 4> discovered;
@@ -98,34 +111,46 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
        return false;
 }
 
-/** Returns whether a CycleGraph contains cycles. */
+/** @returns whether a CycleGraph contains cycles. */
 bool CycleGraph::checkForCycles() {
        return hasCycles;
 }
 
-/** Constructor for a CycleNode. */
-CycleNode::CycleNode(const ModelAction *modelaction) {
-       action=modelaction;
-       hasRMW=NULL;
+/**
+ * Constructor for a CycleNode.
+ * @param modelaction The ModelAction for this node
+ */
+CycleNode::CycleNode(const ModelAction *modelaction) :
+       action(modelaction),
+       hasRMW(NULL)
+{
 }
 
-/** Returns a vector of the edges from a CycleNode. */
+/** @returns a vector of the edges from a CycleNode. */
 std::vector<CycleNode *> * CycleNode::getEdges() {
        return &edges;
 }
 
-/** Adds an edge to a CycleNode. */
-void CycleNode::addEdge(CycleNode * node) {
+/**
+ * Adds an edge from this CycleNode to another CycleNode.
+ * @param node The node to which we add a directed edge
+ */
+void CycleNode::addEdge(CycleNode *node) {
        edges.push_back(node);
 }
 
-/** Get the RMW CycleNode that reads from the current CycleNode. */
-CycleNode* CycleNode::getRMW() {
+/** @returns the RMW CycleNode that reads from the current CycleNode */
+CycleNode * CycleNode::getRMW() {
        return hasRMW;
 }
 
-/** Set a RMW action node that reads from the current CycleNode. */
-bool CycleNode::setRMW(CycleNode * node) {
+/**
+ * Set a RMW action node that reads from the current CycleNode.
+ * @param node The RMW that reads from the current node
+ * @return True, if this node already was read by another RMW; false otherwise
+ * @see CycleGraph::addRMWEdge
+ */
+bool CycleNode::setRMW(CycleNode *node) {
        CycleNode * oldhasRMW=hasRMW;
        hasRMW=node;
        return (oldhasRMW!=NULL);

diff --git a/cyclegraph.h b/cyclegraph.h
index 5cf709324a863d51e4ec45956093600460495232..d0258d180f6e60546bc9619b1b3f56c86bda33de 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -23,11 +23,17 @@ class CycleGraph {
 
  private:
        CycleNode * getNode(const ModelAction *);
+
+       /** @brief A table for mapping ModelActions to CycleNodes */
        HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
+
        bool checkReachable(CycleNode *from, CycleNode *to);
+
+       /** @brief A flag: true if this graph contains cycles */
        bool hasCycles;
 };
 
+/** @brief A node within a CycleGraph; corresponds to one ModelAction */
 class CycleNode {
  public:
        CycleNode(const ModelAction *action);
@@ -37,8 +43,14 @@ class CycleNode {
        CycleNode* getRMW();
 
  private:
+       /** @brief The ModelAction that this node represents */
        const ModelAction *action;
+
+       /** @brief The edges leading out from this node */
        std::vector<CycleNode *> edges;
+
+       /** Pointer to a RMW node that reads from this node, or NULL, if none
+        * exists */
        CycleNode * hasRMW;
 };
 

diff --git a/hashtable.h b/hashtable.h
index 8427f6724318027bac7203ab570d66290900a384..8302000b03e9f9946eb064a8c5c61ca1d8f27b44 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -116,7 +116,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (*
 
        /** Reset the table to its initial state. */
        void reset() {
-               for(int i=0;i<capacity;i++) {
+               for(unsigned int i=0;i<capacity;i++) {
                        struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> * bin = table[i];
                        while(bin!=NULL) {
                                struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> * next=bin->next;
@@ -130,14 +130,10 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (*
 
        /** Put a key value pair into the table. */
        void put(_Key key, _Val val) {
-               if(size > threshold) {
-                       //Resize
-                       unsigned int newsize = capacity << 1;
-                       resize(newsize);
-               }
+               if (size > threshold)
+                       resize(capacity << 1);
 
                struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
-               size++;
                struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = ptr;
 
                while(search!=NULL) {
@@ -153,18 +149,24 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (*
                newptr->val=val;
                newptr->next=ptr;
                table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
+               size++;
        }
 
-       /** Put a key entry into the table. */
-       _Val * ensureptr(_Key key) {
-               if (size > threshold) {
-                       //Resize
-                       unsigned int newsize = capacity << 1;
-                       resize(newsize);
-               }
+       /**
+        * @brief Get a valid pointer to a value corresponding to a given key
+        *
+        * Ensure that key is present in the hash table, then return a pointer
+        * to its value bin. This may require either creating a new bin for
+        * this key (with a default-constructed value) or simply locating and
+        * returning a pointer to an existing value.
+        * @param key The key to check
+        * @return A pointer to the value in the table
+        */
+       _Val * get_safe_ptr(_Key key) {
+               if (size > threshold)
+                       resize(capacity << 1);
 
                struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
-               size++;
                struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = ptr;
 
                while(search!=NULL) {
@@ -178,6 +180,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (*
                newptr->key=key;
                newptr->next=ptr;
                table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
+               size++;
                return &newptr->val;
        }
 

diff --git a/model.cc b/model.cc
index 44c7e353d79b5f8cd87de1f50763c1b705b6224e..25f85d0ee4403ebb1b6ef00531cf872bbdd29892 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -200,7 +200,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
                        return NULL;
        }
        /* linear search: from most recent to oldest */
-       action_list_t *list = obj_map->ensureptr(act->get_location());
+       action_list_t *list = obj_map->get_safe_ptr(act->get_location());
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++) {
                ModelAction *prev = *rit;
@@ -384,7 +384,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) {
  * @param rf The action that curr reads from. Must be a write.
  */
 void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
-       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -414,7 +414,7 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
 /** Updates the cyclegraph with the constraints imposed from the
  *  current read. */
 void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) {
-       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -453,7 +453,7 @@ void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelActi
  * @param curr The current action. Must be a write.
  */
 void ModelChecker::w_modification_order(ModelAction * curr) {
-       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_write());
 
@@ -510,9 +510,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        action_trace->push_back(act);
 
-       obj_map->ensureptr(act->get_location())->push_back(act);
+       obj_map->get_safe_ptr(act->get_location())->push_back(act);
 
-       std::vector<action_list_t> *vec = obj_thrd_map->ensureptr(act->get_location());
+       std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
        if (tid >= (int)vec->size())
                vec->resize(next_thread_id);
        (*vec)[tid].push_back(act);
@@ -538,7 +538,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
  */
 ModelAction * ModelChecker::get_last_seq_cst(const void *location)
 {
-       action_list_t *list = obj_map->ensureptr(location);
+       action_list_t *list = obj_map->get_safe_ptr(location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
@@ -626,7 +626,7 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
  */
 void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
-       std::vector<action_list_t> *thrd_lists = obj_thrd_map->ensureptr(curr->get_location());
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());