X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=action.h;h=fbf566fb7a8f61497284c6ab1e826dd39b0f44e0;hp=4eb1f7ed19799943b3cf906e4f0a1a2017f1a95d;hb=7742256df627848c1c375f979f5369a45c92057b;hpb=9e899821b7500371dbe61975ccbc64e42e82ef83 diff --git a/action.h b/action.h index 4eb1f7ed..fbf566fb 100644 --- a/action.h +++ b/action.h @@ -34,6 +34,7 @@ using std::memory_order_seq_cst; * iteself does not indicate no value. */ #define VALUE_NONE 0xdeadbeef +#define WRITE_REFERENCED ((void *)0x1) /** * @brief The "location" at which a fence occurs @@ -52,25 +53,33 @@ typedef enum action_type { THREAD_YIELD, // < A thread yield action THREAD_JOIN, // < A thread join action THREAD_FINISH, // < A thread completion action + THREADONLY_FINISH, // < A thread completion action + THREAD_SLEEP, // < A sleep operation + PTHREAD_CREATE, // < A pthread creation action PTHREAD_JOIN, // < A pthread join action - ATOMIC_UNINIT, // < Represents an uninitialized atomic - ATOMIC_READ, // < An atomic read action + + NONATOMIC_WRITE, // < Represents a non-atomic store + ATOMIC_INIT, // < Initialization of an atomic object (e.g., atomic_init()) ATOMIC_WRITE, // < An atomic write action + ATOMIC_RMW, // < The write part of an atomic RMW action + ATOMIC_READ, // < An atomic read action ATOMIC_RMWR, // < The read part of an atomic RMW action ATOMIC_RMWRCAS, // < The read part of an atomic RMW action - ATOMIC_RMW, // < The write part of an atomic RMW action ATOMIC_RMWC, // < Convert an atomic RMW action into a READ - ATOMIC_INIT, // < Initialization of an atomic object (e.g., atomic_init()) + ATOMIC_FENCE, // < A fence action ATOMIC_LOCK, // < A lock action ATOMIC_TRYLOCK, // < A trylock 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 + ATOMIC_TIMEDWAIT, // < A timed wait action ATOMIC_ANNOTATION, // < An annotation action to pass information to a trace analysis - NOOP // no operation, which returns control to scheduler + READY_FREE, // < Write is ready to be freed + ATOMIC_NOP // < Placeholder } action_type_t; @@ -78,8 +87,8 @@ typedef enum action_type { * @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 + * multiple executions during backtracking. Except for non-atomic write + * ModelActions, each action is assigned a unique sequence * number. */ class ModelAction { @@ -87,12 +96,15 @@ public: ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL); ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size); ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value, int size); + ModelAction(action_type_t type, memory_order order, uint64_t value, uint64_t time); ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL); ~ModelAction(); void print() const; thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } + void set_type(action_type _type) { type = _type; } + void set_free() { type = READY_FREE; } memory_order get_mo() const { return order; } memory_order get_original_mo() const { return original_order; } void set_mo(memory_order order) { this->order = order; } @@ -104,6 +116,7 @@ public: uint64_t get_write_value() const; uint64_t get_return_value() const; ModelAction * get_reads_from() const { return reads_from; } + uint64_t get_time() const {return time;} cdsc::mutex * get_mutex() const; void set_read_from(ModelAction *act); @@ -116,22 +129,25 @@ public: void copy_from_new(ModelAction *newaction); void set_seq_number(modelclock_t num); + void reset_seq_number(); void set_try_lock(bool obtainedlock); bool is_thread_start() const; bool is_thread_join() const; bool is_mutex_op() const; bool is_lock() const; + bool is_sleep() const; bool is_trylock() const; bool is_unlock() const; bool is_wait() const; + bool is_create() 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_free() const; bool is_yield() const; bool could_be_write() const; bool is_rmwr() const; @@ -176,8 +192,10 @@ public: /* to accomodate pthread create and join */ Thread * thread_operand; void set_thread_operand(Thread *th) { thread_operand = th; } - void set_uninit_action(ModelAction *act) { uninitaction = act; } - ModelAction * get_uninit_action() { return uninitaction; } + + void setActionRef(sllnode *ref) { action_ref = ref; } + sllnode * getActionRef() { return action_ref; } + SNAPSHOTALLOC private: const char * get_type_str() const; @@ -197,12 +215,12 @@ private: */ ModelAction *reads_from; int size; + uint64_t time; //used for sleep }; /** @brief The last fence release from the same thread */ const ModelAction *last_fence_release; - ModelAction * uninitaction; - + /** * @brief The clock vector for this operation * @@ -212,7 +230,8 @@ private: */ ClockVector *cv; ClockVector *rf_cv; - + sllnode * action_ref; + /** @brief The value written (for write or RMW; undefined for read) */ uint64_t value; @@ -231,7 +250,7 @@ private: /** * @brief The sequence number of this action * - * Except for ATOMIC_UNINIT actions, this number should be unique and + * Except for non atomic write actions, this number should be unique and * should represent the action's position in the execution order. */ modelclock_t seq_number;