Add basic reads from support
[model-checker.git] / action.h
1 /** @file action.h
2  *  @brief Models actions taken by threads.
3  */
4
5 #ifndef __ACTION_H__
6 #define __ACTION_H__
7
8 #include <list>
9 #include <cstddef>
10
11 #include "threads.h"
12 #include "libatomic.h"
13 #include "mymemory.h"
14 #include "clockvector.h"
15
16 /** Note that this value can be legitimately used by a program, and
17                 hence by iteself does not indicate no value. */
18
19 #define VALUE_NONE 1234567890
20
21 /** @brief Represents an action type, identifying one of several types of
22  * ModelAction */
23 typedef enum action_type {
24         THREAD_CREATE,        /**< A thread creation action */
25         THREAD_START,         /**< First action in each thread */
26         THREAD_YIELD,         /**< A thread yield action */
27         THREAD_JOIN,          /**< A thread join action */
28         ATOMIC_READ,          /**< An atomic read action */
29         ATOMIC_WRITE,         /**< An atomic write action */
30         ATOMIC_RMW,           /**< An atomic read-modify-write action */
31         ATOMIC_INIT           /**< Initialization of an atomic object (e.g.,
32                                *   atomic_init()) */
33 } action_type_t;
34
35 /* Forward declaration */
36 class Node;
37 class ClockVector;
38
39 /**
40  * The ModelAction class encapsulates an atomic action.
41  */
42 class ModelAction {
43 public:
44         ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
45         ~ModelAction();
46         void print(void) const;
47
48         thread_id_t get_tid() const { return tid; }
49         action_type get_type() const { return type; }
50         memory_order get_mo() const { return order; }
51         void * get_location() const { return location; }
52         modelclock_t get_seq_number() const { return seq_number; }
53         uint64_t get_value() const { return value; }
54         const ModelAction * get_reads_from() const { return reads_from; }
55
56         Node * get_node() const { return node; }
57         void set_node(Node *n) { node = n; }
58
59         bool is_read() const;
60         bool is_write() const;
61         bool is_rmw() const;
62         bool is_initialization() const;
63         bool is_acquire() const;
64         bool is_release() const;
65         bool is_seqcst() const;
66         bool same_var(const ModelAction *act) const;
67         bool same_thread(const ModelAction *act) const;
68         bool is_synchronizing(const ModelAction *act) const;
69
70         void create_cv(const ModelAction *parent = NULL);
71         ClockVector * get_cv() const { return cv; }
72         void read_from(const ModelAction *act);
73
74         bool happens_before(const ModelAction *act) const;
75
76         inline bool operator <(const ModelAction& act) const {
77                 return get_seq_number() < act.get_seq_number();
78         }
79         inline bool operator >(const ModelAction& act) const {
80                 return get_seq_number() > act.get_seq_number();
81         }
82
83         MEMALLOC
84 private:
85
86         /** Type of action (read, write, thread create, thread yield, thread join) */
87         action_type type;
88
89         /** The memory order for this operation. */
90         memory_order order;
91
92         /** A pointer to the memory location for this action. */
93         void *location;
94
95         /** The thread id that performed this action. */
96         thread_id_t tid;
97
98         /** The value read or written (if RMW, then the value written). This
99          * should probably be something longer. */
100         uint64_t value;
101
102         /** The action that this action reads from. Only valid for reads */
103         const ModelAction *reads_from;
104
105         /** A back reference to a Node in NodeStack, if this ModelAction is
106          * saved on the NodeStack. */
107         Node *node;
108
109         modelclock_t seq_number;
110
111         /** The clock vector stored with this action; only needed if this
112          * action is a store release? */
113         ClockVector *cv;
114 };
115
116 typedef std::list<ModelAction *> action_list_t;
117
118 #endif /* __ACTION_H__ */