action: add {get,set}_value(), assign default value
[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 #define VALUE_NONE -1
15
16 typedef enum action_type {
17         THREAD_CREATE,
18         THREAD_YIELD,
19         THREAD_JOIN,
20         ATOMIC_READ,
21         ATOMIC_WRITE,
22         ATOMIC_RMW
23 } action_type_t;
24
25 /* Forward declaration */
26 class Node;
27 class ClockVector;
28
29 /**
30  * The ModelAction class encapsulates an atomic action.
31  */
32 class ModelAction {
33 public:
34         ModelAction(action_type_t type, memory_order order, void *loc, int value = VALUE_NONE);
35         ~ModelAction();
36         void print(void) const;
37
38         thread_id_t get_tid() const { return tid; }
39         action_type get_type() const { return type; }
40         memory_order get_mo() const { return order; }
41         void * get_location() const { return location; }
42         int get_seq_number() const { return seq_number; }
43         int get_value() const { return value; }
44
45         Node * get_node() const { return node; }
46         void set_node(Node *n) { node = n; }
47         void set_value(int val) { value = val; }
48
49         bool is_read() const;
50         bool is_write() const;
51         bool is_rmw() const;
52         bool is_acquire() const;
53         bool is_release() const;
54         bool is_seqcst() const;
55         bool same_var(const ModelAction *act) const;
56         bool same_thread(const ModelAction *act) const;
57         bool is_synchronizing(const ModelAction *act) const;
58
59         void create_cv(ModelAction *parent = NULL);
60         ClockVector * get_cv() const { return cv; }
61         void read_from(ModelAction *act);
62
63         bool happens_before(ModelAction *act);
64
65         inline bool operator <(const ModelAction& act) const {
66                 return get_seq_number() < act.get_seq_number();
67         }
68         inline bool operator >(const ModelAction& act) const {
69                 return get_seq_number() > act.get_seq_number();
70         }
71
72         MEMALLOC
73 private:
74
75         /** Type of action (read, write, thread create, thread yield, thread join) */
76         action_type type;
77
78         /** The memory order for this operation. */
79         memory_order order;
80
81         /** A pointer to the memory location for this action. */
82         void *location;
83
84         /** The thread id that performed this action. */
85         thread_id_t tid;
86         
87         /** The value read or written (if RMW, then the value written). This
88          * should probably be something longer. */
89         int value;
90
91         /** A back reference to a Node in NodeStack, if this ModelAction is
92          * saved on the NodeStack. */
93         Node *node;
94         
95         int seq_number;
96
97         /** The clock vector stored with this action; only needed if this
98          * action is a store release? */
99         ClockVector *cv;
100 };
101
102 typedef std::list<class ModelAction *> action_list_t;
103
104 #endif /* __ACTION_H__ */