improve documentation + Doxygen formatting
authorBrian Norris <banorris@uci.edu>
Thu, 11 Apr 2013 19:15:10 +0000 (12:15 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 11 Apr 2013 19:15:10 +0000 (12:15 -0700)
action.cc
action.h
cyclegraph.cc
cyclegraph.h
datarace.h
hashtable.h
model.cc
nodestack.h

index 08cacd8..bd98f5c 100644 (file)
--- a/action.cc
+++ b/action.cc
 
 #define ACTION_INITIAL_CLOCK 0
 
-/** A special value to represent a successful trylock */
+/** @brief A special value to represent a successful trylock */
 #define VALUE_TRYSUCCESS 1
 
-/** A special value to represent a failed trylock */
+/** @brief A special value to represent a failed trylock */
 #define VALUE_TRYFAILED 0
 
 /**
@@ -279,11 +279,17 @@ Thread * ModelAction::get_thread_operand() const
                return NULL;
 }
 
-/** 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.
+/**
+ * @brief Convert the read portion of an RMW
+ *
+ * Changes an existing read part of an RMW action into either:
+ *  -# a full RMW action in case of the completed write or
+ *  -# a READ action in case a failed action.
+ *
  * @todo  If the memory_order changes, we may potentially need to update our
  * clock vector.
+ *
+ * @param act The second half of the RMW (either RMWC or RMW)
  */
 void ModelAction::process_rmw(ModelAction *act)
 {
@@ -296,14 +302,18 @@ void ModelAction::process_rmw(ModelAction *act)
        }
 }
 
-/** The is_synchronizing method should only explore interleavings if:
- *  (1) the operations are seq_cst and don't commute or
- *  (2) the reordering may establish or break a synchronization relation.
- *  Other memory operations will be dealt with by using the reads_from
- *  relation.
+/**
+ * @brief Check if this action should be backtracked with another, due to
+ * potential synchronization
+ *
+ * The is_synchronizing method should only explore interleavings if:
+ *  -# the operations are seq_cst and don't commute or
+ *  -# the reordering may establish or break a synchronization relation.
+ *
+ * Other memory operations will be dealt with by using the reads_from relation.
  *
- *  @param act is the action to consider exploring a reordering.
- *  @return tells whether we have to explore a reordering.
+ * @param act The action to consider exploring a reordering
+ * @return True, if we have to explore a reordering; otherwise false
  */
 bool ModelAction::could_synchronize_with(const ModelAction *act) const
 {
index 46e8273..dc56017 100644 (file)
--- a/action.h
+++ b/action.h
@@ -12,6 +12,7 @@
 #include "memoryorder.h"
 #include "modeltypes.h"
 
+/* Forward declarations */
 class ClockVector;
 class Thread;
 class Promise;
@@ -27,8 +28,13 @@ using std::memory_order_release;
 using std::memory_order_acq_rel;
 using std::memory_order_seq_cst;
 
-/** Note that this value can be legitimately used by a program, and
- *  hence by iteself does not indicate no value. */
+/**
+ * @brief A recognizable don't-care value for use in the ModelAction::value
+ * field
+ *
+ * Note that this value can be legitimately used by a program, and hence by
+ * iteself does not indicate no value.
+ */
 #define VALUE_NONE 0xdeadbeef
 
 /** @brief Represents an action type, identifying one of several types of
@@ -63,7 +69,12 @@ class Node;
 class ClockVector;
 
 /**
- * The ModelAction class encapsulates an atomic action.
+ * @brief Represents a single atomic action
+ *
+ * A ModelAction is always allocated as non-snapshotting, because it is used in
+ * multiple executions during backtracking. Except for fake uninitialized
+ * (ATOMIC_UNINIT) ModelActions, each action is assigned a unique sequence
+ * number.
  */
 class ModelAction {
 public:
@@ -162,38 +173,61 @@ public:
        MEMALLOC
 private:
 
-       /** Type of action (read, write, thread create, thread yield, thread join) */
+       /** @brief Type of action (read, write, RMW, fence, thread create, etc.) */
        action_type type;
 
-       /** The memory order for this operation. */
+       /** @brief The memory order for this operation. */
        memory_order order;
 
-       /** A pointer to the memory location for this action. */
+       /** @brief A pointer to the memory location for this action. */
        void *location;
 
-       /** The thread id that performed this action. */
+       /** @brief The thread id that performed this action. */
        thread_id_t tid;
 
-       /** The value written (for write or RMW; undefined for read) */
+       /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
 
-       /** The action that this action reads from. Only valid for reads */
+       /**
+        * @brief The store that this action reads from
+        *
+        * Only valid for reads
+        */
        const ModelAction *reads_from;
 
-       /** The promise that this action reads from. Only valid for reads */
+       /**
+        * @brief The promise that this action reads from
+        *
+        * Only valid for reads
+        */
        Promise *reads_from_promise;
 
-       /** The last fence release from the same thread */
+       /** @brief The last fence release from the same thread */
        const ModelAction *last_fence_release;
 
-       /** A back reference to a Node in NodeStack, if this ModelAction is
-        * saved on the NodeStack. */
+       /**
+        * @brief A back reference to a Node in NodeStack
+        *
+        * Only set if this ModelAction is saved on the NodeStack. (A
+        * ModelAction can be thrown away before it ever enters the NodeStack.)
+        */
        Node *node;
 
+       /**
+        * @brief The sequence number of this action
+        *
+        * Except for ATOMIC_UNINIT actions, this number should be unique and
+        * should represent the action's position in the execution order.
+        */
        modelclock_t seq_number;
 
-       /** The clock vector stored with this action; only needed if this
-        * action is a store release? */
+       /**
+        * @brief The clock vector for this operation
+        *
+        * Technically, this is only needed for potentially synchronizing
+        * (e.g., non-relaxed) operations, but it is very handy to have these
+        * vectors for all operations.
+        */
        ClockVector *cv;
 
        bool sleep_flag;
index 26ea215..77c0b68 100644 (file)
@@ -232,8 +232,8 @@ bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
  *
  * Handles special case of a RMW action, where the ModelAction rmw reads from
  * the ModelAction/Promise from. The key differences are:
- * (1) no write can occur in between the rmw and the from action.
- * (2) Only one RMW action can read from a given write.
+ *  -# No write can occur in between the @a rmw and @a from actions.
+ *  -# Only one RMW action can read from a given write.
  *
  * @param from The edge comes from this ModelAction/Promise
  * @param rmw The edge points to this ModelAction; this action must read from
@@ -472,6 +472,7 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) cons
        return false;
 }
 
+/** @brief Begin a new sequence of graph additions which can be rolled back */
 void CycleGraph::startChanges()
 {
        ASSERT(rollbackvector.empty());
@@ -531,7 +532,7 @@ CycleNode::CycleNode(const Promise *promise) :
 
 /**
  * @param i The index of the edge to return
- * @returns The CycleNode edge indexed by i
+ * @returns The CycleNode edge indexed by i
  */
 CycleNode * CycleNode::getEdge(unsigned int i) const
 {
@@ -544,11 +545,16 @@ unsigned int CycleNode::getNumEdges() const
        return edges.size();
 }
 
+/**
+ * @param i The index of the back edge to return
+ * @returns The CycleNode back-edge indexed by i
+ */
 CycleNode * CycleNode::getBackEdge(unsigned int i) const
 {
        return back_edges[i];
 }
 
+/** @returns The number of edges entering this CycleNode */
 unsigned int CycleNode::getNumBackEdges() const
 {
        return back_edges.size();
index 1a3e0eb..7e7d180 100644 (file)
@@ -82,6 +82,7 @@ class CycleGraph {
 
        /** @brief A flag: true if this graph contains cycles */
        bool hasCycles;
+       /** @brief The previous value of CycleGraph::hasCycles, for rollback */
        bool oldCycles;
 
        SnapVector<CycleNode *> rollbackvector;
index 7c24b6d..6c92203 100644 (file)
@@ -49,15 +49,9 @@ void assert_race(struct DataRace *race);
 
 extern SnapVector<struct DataRace *> unrealizedraces;
 
-/** Basic encoding idea:
- *      (void *) Either:
- *      (1) points to a full record or
- *
- * (2) encodes the information in a 64 bit word.  Encoding is as
- * follows: lowest bit set to 1, next 8 bits are read thread id, next
- * 23 bits are read clock vector, next 8 bites are write thread id,
- * next 23 bits are write clock vector.  */
-
+/**
+ * @brief A record of information for detecting data races
+ */
 struct RaceRecord {
        modelclock_t *readClock;
        thread_id_t *thread;
@@ -81,6 +75,17 @@ struct RaceRecord {
 #define WRITEMASK READMASK
 #define WRITEVECTOR(x) (((x)>>40)&WRITEMASK)
 
+/**
+ * The basic encoding idea is that (void *) either:
+ *  -# points to a full record (RaceRecord) or
+ *  -# encodes the information in a 64 bit word. Encoding is as
+ *     follows:
+ *     - lowest bit set to 1
+ *     - next 8 bits are read thread id
+ *     - next 23 bits are read clock vector
+ *     - next 8 bits are write thread id
+ *     - next 23 bits are write clock vector
+ */
 #define ENCODEOP(rdthread, rdtime, wrthread, wrtime) (0x1ULL | ((rdthread)<<1) | ((rdtime) << 9) | (((uint64_t)wrthread)<<32) | (((uint64_t)wrtime)<<40))
 
 #define MAXTHREADID (THREADMASK-1)
index 5b0086f..c09b3ff 100644 (file)
@@ -12,8 +12,9 @@
 #include "common.h"
 
 /**
- * Hashtable linked node class, for chained storage of hash table conflicts. By
- * default it is snapshotting, but you can pass in your own allocation
+ * @brief HashTable linked node class, for chained storage of hash table conflicts
+ *
+ * By default it is snapshotting, but you can pass in your own allocation
  * functions.
  *
  * @tparam _Key    Type name for the key
@@ -33,8 +34,10 @@ struct hashlistnode {
 };
 
 /**
- * Hashtable class. By default it is snapshotting, but you can pass in your own
- * allocation functions.
+ * @brief A simple, custom hash table
+ *
+ * By default it is snapshotting, but you can pass in your own allocation
+ * functions.
  *
  * @tparam _Key    Type name for the key
  * @tparam _Val    Type name for the values to be stored
index 29b88c1..5941cf2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1796,16 +1796,15 @@ bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
 }
 
 /**
- * Updates the mo_graph with the constraints imposed from the current
+ * @brief Updates the mo_graph with the constraints imposed from the current
  * read.
  *
  * Basic idea is the following: Go through each other thread and find
  * the last action that happened before our read.  Two cases:
  *
- * (1) The action is a write => that write must either occur before
+ * -# The action is a write: that write must either occur before
  * the write we read from or be the write we read from.
- *
- * (2) The action is a read => the write that that action read from
+ * -# The action is a read: the write that that action read from
  * must occur before the write we read from or be the same write.
  *
  * @param curr The current action. Must be a read.
index 8573e9f..e260f08 100644 (file)
@@ -22,11 +22,18 @@ struct fairness_info {
        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,
-       READ_FROM_PROMISE,
-       READ_FROM_FUTURE,
-       READ_FROM_NONE,
+       READ_FROM_PAST, /**< @brief Read from a prior, existing store */
+       READ_FROM_PROMISE, /**< @brief Read from an existing promised future value */
+       READ_FROM_FUTURE, /**< @brief Read from a newly-asserted future value */
+       READ_FROM_NONE, /**< @brief A NULL state, which should not be reached */
 } read_from_type_t;
 
 #define YIELD_E 1