X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=action.h;h=abf55318cd3ba379ea198420fad4ce70bfc570ea;hp=c455ea780883b371d80caed2d25c95e3d16edf1b;hb=d775a7d6624fa14284c4a273d039bedd21a1f55c;hpb=c7cd65f78d1c7956a02ac1e1cbd833e3dd17a3f1 diff --git a/action.h b/action.h index c455ea78..abf55318 100644 --- a/action.h +++ b/action.h @@ -5,13 +5,20 @@ #ifndef __ACTION_H__ #define __ACTION_H__ -#include #include +#include -#include "threads.h" #include "mymemory.h" -#include "clockvector.h" #include "memoryorder.h" +#include "modeltypes.h" + +class ClockVector; +class Thread; +class Promise; + +namespace std { + class mutex; +} using std::memory_order; using std::memory_order_relaxed; @@ -21,12 +28,10 @@ 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. */ - -#define VALUE_NONE 1234567890 + * hence by iteself does not indicate no value. */ +#define VALUE_NONE 0xdeadbeef /** A special value to represent a successful trylock */ - #define VALUE_TRYSUCCESS 1 /** A special value to represent a failed trylock */ @@ -35,11 +40,14 @@ using std::memory_order_seq_cst; /** @brief Represents an action type, identifying one of several types of * ModelAction */ typedef enum action_type { + MODEL_FIXUP_RELSEQ, /**< Special ModelAction: finalize a release + * sequence */ 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 */ + 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 */ @@ -50,7 +58,10 @@ typedef enum action_type { ATOMIC_FENCE, /**< A fence action */ ATOMIC_LOCK, /**< A lock action */ ATOMIC_TRYLOCK, /**< A trylock action */ - ATOMIC_UNLOCK /**< An unlock action */ + ATOMIC_UNLOCK, /**< An unlock action */ + ATOMIC_NOTIFY_ONE, /**< A notify_one action */ + ATOMIC_NOTIFY_ALL, /**< A notify all action */ + ATOMIC_WAIT /**< A wait action */ } action_type_t; /* Forward declaration */ @@ -62,9 +73,9 @@ class ClockVector; */ class ModelAction { public: - ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE); + ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL); ~ModelAction(); - void print(void) const; + void print() const; thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } @@ -72,38 +83,65 @@ public: void * get_location() const { return location; } modelclock_t get_seq_number() const { return seq_number; } uint64_t get_value() const { return value; } + uint64_t get_reads_from_value() const; + uint64_t get_write_value() const; + uint64_t get_return_value() const; const ModelAction * get_reads_from() const { return reads_from; } + Promise * get_reads_from_promise() const { return reads_from_promise; } + std::mutex * get_mutex() const; - Node * get_node() const { return node; } + Node * get_node() const; void set_node(Node *n) { node = n; } + void set_read_from(const ModelAction *act); + void set_read_from_promise(Promise *promise); + + /** Store the most recent fence-release from the same thread + * @param fence The fence-release that occured prior to this */ + void set_last_fence_release(const ModelAction *fence) { last_fence_release = fence; } + /** @return The most recent fence-release from the same thread */ + const ModelAction * get_last_fence_release() const { return last_fence_release; } + void copy_from_new(ModelAction *newaction); + void set_seq_number(modelclock_t num); void set_try_lock(bool obtainedlock); + bool is_thread_start() const; + bool is_thread_join() const; + bool is_relseq_fixup() const; bool is_mutex_op() const; bool is_lock() const; bool is_trylock() const; bool is_unlock() const; + bool is_wait() const; + bool is_notify() const; + bool is_notify_one() const; bool is_success_lock() const; bool is_failed_trylock() const; + bool is_atomic_var() const; + bool is_uninitialized() const; bool is_read() const; bool is_write() const; + bool is_yield() const; + bool could_be_write() const; bool is_rmwr() const; bool is_rmwc() const; bool is_rmw() const; bool is_fence() const; bool is_initialization() const; + bool is_relaxed() const; bool is_acquire() const; bool is_release() const; bool is_seqcst() const; bool same_var(const ModelAction *act) const; bool same_thread(const ModelAction *act) const; bool is_conflicting_lock(const ModelAction *act) const; - bool is_synchronizing(const ModelAction *act) const; + bool could_synchronize_with(const ModelAction *act) const; + + Thread * get_thread_operand() const; void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } - void read_from(const ModelAction *act); - void synchronize_with(const ModelAction *act); + bool synchronize_with(const ModelAction *act); bool has_synchronized_with(const ModelAction *act) const; bool happens_before(const ModelAction *act) const; @@ -118,6 +156,15 @@ public: void process_rmw(ModelAction * act); void copy_typeandorder(ModelAction * act); + void set_sleep_flag() { sleep_flag=true; } + bool get_sleep_flag() { return sleep_flag; } + unsigned int hash() const; + + bool equals(const ModelAction *x) const { return this == x; } + bool equals(const Promise *x) const { return false; } + + bool may_read_from(const ModelAction *write) const; + bool may_read_from(const Promise *promise) const; MEMALLOC private: @@ -139,6 +186,12 @@ private: /** The action that this action reads from. Only valid for reads */ const ModelAction *reads_from; + /** The promise that this action reads from. Only valid for reads */ + Promise *reads_from_promise; + + /** 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. */ Node *node; @@ -148,8 +201,8 @@ private: /** The clock vector stored with this action; only needed if this * action is a store release? */ ClockVector *cv; -}; -typedef std::list action_list_t; + bool sleep_flag; +}; #endif /* __ACTION_H__ */