#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
/**
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)
{
}
}
-/** 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
{
#include "memoryorder.h"
#include "modeltypes.h"
+/* Forward declarations */
class ClockVector;
class Thread;
class Promise;
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
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:
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;
*
* 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
return false;
}
+/** @brief Begin a new sequence of graph additions which can be rolled back */
void CycleGraph::startChanges()
{
ASSERT(rollbackvector.empty());
/**
* @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
{
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();
/** @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;
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;
#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)
#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
};
/**
- * 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
}
/**
- * 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.
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
projects / model-checker.git / commitdiff