From: Brian Norris Date: Thu, 11 Apr 2013 19:15:10 +0000 (-0700) Subject: improve documentation + Doxygen formatting X-Git-Tag: oopsla2013~88 X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=4fa31aac91303266f4c87a6cd5d60cbab34135db improve documentation + Doxygen formatting --- diff --git a/action.cc b/action.cc index 08cacd8..bd98f5c 100644 --- a/action.cc +++ b/action.cc @@ -11,10 +11,10 @@ #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 { diff --git a/action.h b/action.h index 46e8273..dc56017 100644 --- 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; diff --git a/cyclegraph.cc b/cyclegraph.cc index 26ea215..77c0b68 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -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 a 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(); diff --git a/cyclegraph.h b/cyclegraph.h index 1a3e0eb..7e7d180 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -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 rollbackvector; diff --git a/datarace.h b/datarace.h index 7c24b6d..6c92203 100644 --- a/datarace.h +++ b/datarace.h @@ -49,15 +49,9 @@ void assert_race(struct DataRace *race); extern SnapVector 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) diff --git a/hashtable.h b/hashtable.h index 5b0086f..c09b3ff 100644 --- a/hashtable.h +++ b/hashtable.h @@ -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 diff --git a/model.cc b/model.cc index 29b88c1..5941cf2 100644 --- 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. diff --git a/nodestack.h b/nodestack.h index 8573e9f..e260f08 100644 --- a/nodestack.h +++ b/nodestack.h @@ -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