Add documentation
authorBrian Demsky <bdemsky@uci.edu>
Fri, 20 Jul 2012 21:01:03 +0000 (14:01 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 2 Aug 2012 17:12:48 +0000 (10:12 -0700)
[Split by Brian Norris]

action.cc
cmodelint.cc
cmodelint.h
cyclegraph.cc
cyclegraph.h
datarace.h
hashtable.h
nodestack.cc

index 1fb3b76..f0ad48f 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -100,6 +100,14 @@ void ModelAction::copy_typeandorder(ModelAction * act) {
        this->order=act->order;
 }
 
+/** This method changes an existing read part of an RMW action into either:
+ *  (1) a full RMW action in case of the completed write or
+ *  (2) a READ action in case a failed action.
+ */
+
+//TODO:  If the memory_order changes, we may potentially need to update our
+//clock vector.
+
 void ModelAction::process_rmw(ModelAction * act) {
        this->order=act->order;
        if (act->is_rmwc())
@@ -155,6 +163,8 @@ void ModelAction::create_cv(const ModelAction *parent)
                cv = new ClockVector(NULL, this);
 }
 
+
+/** Update the model action's read_from action */
 void ModelAction::read_from(const ModelAction *act)
 {
        ASSERT(cv);
index 4754a82..8919041 100644 (file)
@@ -1,28 +1,38 @@
 #include "model.h"
 #include "cmodelint.h"
 
+/** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
        model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
        return thread_current()->get_return_value();
 }
 
+/** Performs a write action.*/
 void model_write_action(void * obj, memory_order ord, uint64_t val) {
        model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
 }
 
+/** Performs an init action. */
 void model_init_action(void * obj, uint64_t val) {
        model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
 }
 
+/**
+ * Performs the read part of a RMW action. The next action must either be the
+ * write part of the RMW action or an explicit close out of the RMW action w/o
+ * a write.
+ */
 uint64_t model_rmwr_action(void *obj, memory_order ord) {
        model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
        return thread_current()->get_return_value();
 }
 
+/** Performs the write part of a RMW action. */
 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
        model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
 }
 
+/** Closes out a RMW action without doing a write. */
 void model_rmwc_action(void *obj, memory_order ord) {
        model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
 }
index 5e762f8..c23c061 100644 (file)
@@ -1,3 +1,7 @@
+/** @file cmodelint.h
+ *  @brief C interface to the model checker.
+ */
+
 #ifndef CMODELINT_H
 #define CMODELINT_H
 #include <inttypes.h>
index c0e8e2a..f060a00 100644 (file)
@@ -19,10 +19,10 @@ CycleNode * CycleGraph::getNode(const ModelAction * action) {
        return node;
 }
 
-/** Adds an edge between two ModelActions. */
-
-//the event to happens after the event from
-
+/**
+ * Adds an edge between two ModelActions.  The ModelAction to happens after the
+ * ModelAction from.
+ */
 void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
        CycleNode *fromnode=getNode(from);
        CycleNode *tonode=getNode(to);
@@ -47,8 +47,11 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
        }
 }
 
-//event rmw that reads from the node from
-
+/** Handles special case of a RMW action.  The ModelAction rmw reads
+ *  from the ModelAction from.  The key differences are: (1) no write
+ *  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) {
        CycleNode *fromnode=getNode(from);
        CycleNode *rmwnode=getNode(rmw);
@@ -116,10 +119,12 @@ void CycleNode::addEdge(CycleNode * node) {
        edges.push_back(node);
 }
 
+/** Get 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) {
        CycleNode * oldhasRMW=hasRMW;
        hasRMW=node;
index 3ed4e4a..5cf7093 100644 (file)
@@ -1,3 +1,7 @@
+/** @file cyclegraph.h @brief Data structure to track ordering
+ *  constraints on modification order.  The idea is to see whether a
+ *  total order exists that satisfies the ordering constriants.*/
+
 #ifndef CYCLEGRAPH_H
 #define CYCLEGRAPH_H
 
index ef1ef8c..33a5c26 100644 (file)
@@ -1,3 +1,7 @@
+/** @file datarace.h
+ *  @brief Data race detection code.
+ */
+
 #ifndef DATARACE_H
 #include "config.h"
 #include <stdint.h>
@@ -19,7 +23,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
 
 
 
-/** Encoding idea:
+/** Basic encoding idea:
  *      (void *) Either:
  *      (1) points to a full record or
  *
index b1cd327..c4cf290 100644 (file)
@@ -1,3 +1,7 @@
+/** @file hashtable.h
+ *  @brief Hashtable.  Standard chained bucket variety.
+ */
+
 #ifndef HASHTABLE_H
 #define HASHTABLE_H
 
@@ -36,6 +40,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
                free(table);
        }
 
+       /** Reset the table to its initial state. */
        void reset() {
                for(int i=0;i<capacity;i++) {
                        struct hashlistnode<_Key,_Val> * bin = table[i];
@@ -49,6 +54,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
                size=0;
        }
 
+       /** Put a key value pair into the table. */
        void put(_Key key, _Val val) {
                if(size > threshold) {
                        //Resize
@@ -75,6 +81,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
                table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
        }
 
+       /** Lookup the corresponding value for the given key. */
        _Val get(_Key key) {
                struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
 
@@ -87,6 +94,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
                return (_Val)0;
        }
 
+       /** Check whether the table contains a value for the given key. */
        bool contains(_Key key) {
                struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
 
@@ -99,6 +107,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
                return false;
        }
 
+       /** Resize the table. */
        void resize(unsigned int newsize) {
                struct hashlistnode<_Key,_Val> ** oldtable = table;
                struct hashlistnode<_Key,_Val> ** newtable;
index 1de5169..e8f377b 100644 (file)
@@ -77,6 +77,11 @@ bool Node::backtrack_empty()
        return (numBacktracks == 0);
 }
 
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
 bool Node::readsfrom_empty() {
        return ((read_from_index+1)>=may_read_from.size());
 }
@@ -148,6 +153,10 @@ const ModelAction * Node::get_read_from() {
        return may_read_from[read_from_index];
 }
 
+/**
+ * Increments the index into the readsfrom set to explore the next item.
+ * @return Returns false if we have explored all items.
+ */
 bool Node::increment_read_from() {
        read_from_index++;
        return (read_from_index<may_read_from.size());
@@ -225,7 +234,8 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
  * destructor for each. This function is provided an offset which determines
  * how many nodes (relative to the current replay state) to save before popping
  * the stack.
- * @param numAhead The number of nodes to skip forward before popping the stack.
+ * @param numAhead gives the number of Nodes (including this Node) to skip over
+ * before removing nodes.
  */
 void NodeStack::pop_restofstack(int numAhead)
 {