action: add create_cv() and read_from()
[model-checker.git] / action.cc
1 #include <stdio.h>
2
3 #include "model.h"
4 #include "action.h"
5 #include "clockvector.h"
6 #include "common.h"
7
8 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
9 {
10         Thread *t = thread_current();
11         ModelAction *act = this;
12
13         act->type = type;
14         act->order = order;
15         act->location = loc;
16         act->tid = t->get_id();
17         act->value = value;
18         act->seq_number = model->get_next_seq_num();
19
20         cv = NULL;
21 }
22
23 ModelAction::~ModelAction()
24 {
25         if (cv)
26                 delete cv;
27 }
28
29 bool ModelAction::is_read()
30 {
31         return type == ATOMIC_READ;
32 }
33
34 bool ModelAction::is_write()
35 {
36         return type == ATOMIC_WRITE;
37 }
38
39 bool ModelAction::is_acquire()
40 {
41         switch (order) {
42         case memory_order_acquire:
43         case memory_order_acq_rel:
44         case memory_order_seq_cst:
45                 return true;
46         default:
47                 return false;
48         }
49 }
50
51 bool ModelAction::is_release()
52 {
53         switch (order) {
54         case memory_order_release:
55         case memory_order_acq_rel:
56         case memory_order_seq_cst:
57                 return true;
58         default:
59                 return false;
60         }
61 }
62
63 bool ModelAction::same_var(ModelAction *act)
64 {
65         return location == act->location;
66 }
67
68 bool ModelAction::same_thread(ModelAction *act)
69 {
70         return tid == act->tid;
71 }
72
73 bool ModelAction::is_dependent(ModelAction *act)
74 {
75         if (!is_read() && !is_write())
76                 return false;
77         if (!act->is_read() && !act->is_write())
78                 return false;
79         if (same_var(act) && !same_thread(act) &&
80                         (is_write() || act->is_write()))
81                 return true;
82         return false;
83 }
84
85 void ModelAction::create_cv(ModelAction *parent)
86 {
87         ASSERT(cv == NULL);
88         if (parent)
89                 cv = new ClockVector(parent->cv, this);
90         else
91                 cv = new ClockVector();
92 }
93
94 void ModelAction::read_from(ModelAction *act)
95 {
96         ASSERT(cv);
97         if (act->is_release() && this->is_acquire())
98                 cv->merge(act->cv);
99         value = act->value;
100 }
101
102 void ModelAction::print(void)
103 {
104         const char *type_str;
105         switch (this->type) {
106         case THREAD_CREATE:
107                 type_str = "thread create";
108                 break;
109         case THREAD_YIELD:
110                 type_str = "thread yield";
111                 break;
112         case THREAD_JOIN:
113                 type_str = "thread join";
114                 break;
115         case ATOMIC_READ:
116                 type_str = "atomic read";
117                 break;
118         case ATOMIC_WRITE:
119                 type_str = "atomic write";
120                 break;
121         default:
122                 type_str = "unknown type";
123         }
124
125         printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
126                         seq_number, id_to_int(tid), type_str, order, location, value);
127 }