X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=action.h;h=ae4afb29d27f928cbe63a34d79629a6d6310b28b;hb=f3ef22bef8d339c7d45b7d7232cdcf183a0b7776;hp=cca56390567a0b66b265d371656417b60a34e748;hpb=3e0ad5e987371d52c9377a12cff4c4dec2b6fd81;p=c11tester.git diff --git a/action.h b/action.h index cca56390..ae4afb29 100644 --- a/action.h +++ b/action.h @@ -1,11 +1,16 @@ +/** @file action.h + * @brief Models actions taken by threads. + */ + #ifndef __ACTION_H__ #define __ACTION_H__ #include +#include #include "threads.h" #include "libatomic.h" - +#include "mymemory.h" #define VALUE_NONE -1 typedef enum action_type { @@ -13,41 +18,83 @@ typedef enum action_type { THREAD_YIELD, THREAD_JOIN, ATOMIC_READ, - ATOMIC_WRITE + ATOMIC_WRITE, + ATOMIC_RMW } action_type_t; -/* Forward declaration (tree.h) */ -class TreeNode; +/* Forward declaration */ +class Node; +class ClockVector; +/** + * The ModelAction class encapsulates an atomic action. + */ class ModelAction { public: ModelAction(action_type_t type, memory_order order, void *loc, int value); + ~ModelAction(); void print(void); - thread_id_t get_tid() { return tid; } - action_type get_type() { return type; } - memory_order get_mo() { return order; } - void * get_location() { return location; } - int get_seq_number() { return seq_number; } - - TreeNode * get_node() { return node; } - void set_node(TreeNode *n) { node = n; } - - bool is_read(); - bool is_write(); - bool is_acquire(); - bool is_release(); - bool same_var(ModelAction *act); - bool same_thread(ModelAction *act); - bool is_dependent(ModelAction *act); + 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; } + int get_seq_number() const { return seq_number; } + + Node * get_node() const { return node; } + void set_node(Node *n) { node = n; } + + bool is_read() const; + bool is_write() const; + bool is_rmw() 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_synchronizing(const ModelAction *act) const; + + void create_cv(ModelAction *parent = NULL); + ClockVector * get_cv() const { return cv; } + void read_from(ModelAction *act); + + bool happens_before(ModelAction *act); + + inline bool operator <(const ModelAction& act) const { + return get_seq_number() < act.get_seq_number(); + } + inline bool operator >(const ModelAction& act) const { + return get_seq_number() > act.get_seq_number(); + } + + MEMALLOC private: + + /** Type of action (read, write, thread create, thread yield, thread join) */ action_type type; + + /** The memory order for this operation. */ memory_order order; + + /** A pointer to the memory location for this action. */ void *location; + + /** The thread id that performed this action. */ thread_id_t tid; + + /** The value read or written (if RMW, then the value written). This + * should probably be something longer. */ int value; - TreeNode *node; + + /** A back reference to a Node in NodeStack, if this ModelAction is + * saved on the NodeStack. */ + Node *node; + int seq_number; + + /** The clock vector stored with this action; only needed if this + * action is a store release? */ + ClockVector *cv; }; typedef std::list action_list_t;