using std::memory_order_acquire;
using std::memory_order_release;
using std::memory_order_acq_rel;
using std::memory_order_seq_cst;
using std::memory_order_acquire;
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.
+ */
-/** A special value to represent a successful trylock */
-
-#define VALUE_TRYSUCCESS 1
-
-/** A special value to represent a failed trylock */
-#define VALUE_TRYFAILED 0
+/**
+ * @brief The "location" at which a fence occurs
+ *
+ * We need a non-zero memory location to associate with fences, since our hash
+ * tables don't handle NULL-pointer keys. HACK: Hopefully this doesn't collide
+ * with any legitimate memory locations.
+ */
+#define FENCE_LOCATION ((void *)0x7)
/** @brief Represents an action type, identifying one of several types of
* ModelAction */
typedef enum action_type {
/** @brief Represents an action type, identifying one of several types of
* ModelAction */
typedef enum action_type {
THREAD_CREATE, /**< A thread creation action */
THREAD_START, /**< First action in each thread */
THREAD_YIELD, /**< A thread yield action */
THREAD_JOIN, /**< A thread join action */
THREAD_FINISH, /**< A thread completion action */
THREAD_CREATE, /**< A thread creation action */
THREAD_START, /**< First action in each thread */
THREAD_YIELD, /**< A thread yield action */
THREAD_JOIN, /**< A thread join action */
THREAD_FINISH, /**< A thread completion action */
+ PTHREAD_CREATE, /**< A pthread creation action */
+ PTHREAD_JOIN, /**< A pthread join action */
+
+ ATOMIC_UNINIT, /**< Represents an uninitialized atomic */
ATOMIC_READ, /**< An atomic read action */
ATOMIC_WRITE, /**< An atomic write action */
ATOMIC_RMWR, /**< The read part of an atomic RMW action */
ATOMIC_READ, /**< An atomic read action */
ATOMIC_WRITE, /**< An atomic write action */
ATOMIC_RMWR, /**< The read part of an atomic RMW action */
ATOMIC_UNLOCK, /**< An unlock action */
ATOMIC_NOTIFY_ONE, /**< A notify_one action */
ATOMIC_NOTIFY_ALL, /**< A notify all action */
ATOMIC_UNLOCK, /**< An unlock action */
ATOMIC_NOTIFY_ONE, /**< A notify_one action */
ATOMIC_NOTIFY_ALL, /**< A notify all action */
- * 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.
thread_id_t get_tid() const { return tid; }
action_type get_type() const { return type; }
memory_order get_mo() const { return order; }
thread_id_t get_tid() const { return tid; }
action_type get_type() const { return type; }
memory_order get_mo() const { return order; }
void * get_location() const { return location; }
modelclock_t get_seq_number() const { return seq_number; }
uint64_t get_value() const { return value; }
void * get_location() const { return location; }
modelclock_t get_seq_number() const { return seq_number; }
uint64_t get_value() const { return value; }
void copy_from_new(ModelAction *newaction);
void set_seq_number(modelclock_t num);
void set_try_lock(bool obtainedlock);
void copy_from_new(ModelAction *newaction);
void set_seq_number(modelclock_t num);
void set_try_lock(bool obtainedlock);
bool is_notify_one() const;
bool is_success_lock() const;
bool is_failed_trylock() const;
bool is_notify_one() const;
bool is_success_lock() const;
bool is_failed_trylock() const;
bool is_conflicting_lock(const ModelAction *act) const;
bool could_synchronize_with(const ModelAction *act) const;
bool is_conflicting_lock(const ModelAction *act) const;
bool could_synchronize_with(const ModelAction *act) const;
void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
bool synchronize_with(const ModelAction *act);
void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
bool synchronize_with(const ModelAction *act);
- /** Type of action (read, write, thread create, thread yield, thread join) */
+ const char * get_type_str() const;
+ const char * get_mo_str() const;
+
+ /** @brief Type of action (read, write, RMW, fence, thread create, etc.) */
- /** A pointer to the memory location for this action. */
+ /** @brief The original memory order parameter for this operation. */
+ memory_order original_order;
+
+ /** @brief A pointer to the memory location for this action. */
- /** 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.)
+ */
- /** 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.
+ */