d3120fc3f612518f5bca1b5b80aed3f813454147
[model-checker.git] / scanalysis.cc
1 #include "scanalysis.h"
2 #include "action.h"
3 #include "threads-model.h"
4 #include "clockvector.h"
5 #include "execution.h"
6
7 SCAnalysis::SCAnalysis(const ModelExecution *execution) :
8         execution(execution)
9 {
10         cvmap = new HashTable <const ModelAction *, ClockVector *, uintptr_t, 4>();
11         cycleset = new HashTable <const ModelAction *, const ModelAction *, uintptr_t, 4>();
12         threadlists = new SnapVector <action_list_t>(1);
13 }
14
15 SCAnalysis::~SCAnalysis() {
16         delete cvmap;
17         delete cycleset;
18         delete threadlists;
19 }
20
21 void SCAnalysis::print_list(action_list_t *list) {
22         action_list_t::iterator it;
23
24         model_print("---------------------------------------------------------------------\n");
25
26         unsigned int hash = 0;
27
28         for (it = list->begin(); it != list->end(); it++) {
29                 const ModelAction *act = *it;
30                 if (act->get_seq_number() > 0) {
31                         if (cycleset->contains(act))
32                                 model_print("CYC");
33                         act->print();
34                 }
35                 hash = hash ^ (hash << 3) ^ ((*it)->hash());
36         }
37         model_print("HASH %u\n", hash);
38         model_print("---------------------------------------------------------------------\n");
39 }
40
41 void SCAnalysis::analyze(action_list_t *actions) {
42         buildVectors(actions);
43         computeCV(actions);
44         action_list_t *list = generateSC(actions);
45         print_list(list);
46 }
47
48 bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2) {
49         if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
50                 cycleset->put(act, act);
51         }
52         return cv->merge(cv2);
53 }
54
55 ModelAction * SCAnalysis::getNextAction() {
56         ModelAction *act = NULL;
57         for (int i = 0; i <= maxthreads; i++) {
58                 action_list_t *threadlist = &(*threadlists)[i];
59                 if (threadlist->empty())
60                         continue;
61                 ModelAction *first = threadlist->front();
62                 if (act == NULL) {
63                         act = first;
64                         continue;
65                 }
66                 ClockVector *cv = cvmap->get(act);
67                 if (cv->synchronized_since(first)) {
68                         act = first;
69                 }
70         }
71         if (act == NULL)
72                 return act;
73         //print cycles in a nice way to avoid confusion
74         //make sure thread starts appear after the create
75         if (act->is_thread_start()) {
76                 ModelAction *createact = execution->get_thread(act)->get_creation();
77                 if (createact) {
78                         action_list_t *threadlist = &(*threadlists)[id_to_int(createact->get_tid())];
79                         if (!threadlist->empty()) {
80                                 ModelAction *first = threadlist->front();
81                                 if (first->get_seq_number() <= createact->get_seq_number())
82                                         act = first;
83                         }
84                 }
85         }
86
87         //make sure that joins appear after the thread is finished
88         if (act->is_thread_join()) {
89                 int jointhread = id_to_int(act->get_thread_operand()->get_id());
90                 action_list_t *threadlist = &(*threadlists)[jointhread];
91                 if (!threadlist->empty()) {
92                         act = threadlist->front();
93                 }
94         }
95
96         return act;
97 }
98
99 action_list_t * SCAnalysis::generateSC(action_list_t *list) {
100         action_list_t *sclist = new action_list_t();
101         while (true) {
102                 ModelAction *act = getNextAction();
103                 if (act == NULL)
104                         break;
105                 thread_id_t tid = act->get_tid();
106                 //remove action
107                 (*threadlists)[id_to_int(tid)].pop_front();
108                 //add ordering constraints from this choice
109                 if (updateConstraints(act)) {
110                         //propagate changes if we have them
111                         computeCV(list);
112                 }
113                 //add action to end
114                 sclist->push_back(act);
115         }
116         return sclist;
117 }
118
119 void SCAnalysis::buildVectors(action_list_t *list) {
120         maxthreads = 0;
121         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
122                 ModelAction *act = *it;
123                 int threadid = id_to_int(act->get_tid());
124                 if (threadid > maxthreads) {
125                         threadlists->resize(threadid + 1);
126                         maxthreads = threadid;
127                 }
128                 (*threadlists)[threadid].push_back(act);
129         }
130 }
131
132 bool SCAnalysis::updateConstraints(ModelAction *act) {
133         bool changed = false;
134         ClockVector *actcv = cvmap->get(act);
135         for (int i = 0; i <= maxthreads; i++) {
136                 thread_id_t tid = int_to_id(i);
137                 if (tid == act->get_tid())
138                         continue;
139
140                 action_list_t *list = &(*threadlists)[id_to_int(tid)];
141                 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
142                         ModelAction *write = *rit;
143                         if (!write->is_write())
144                                 continue;
145                         ClockVector *writecv = cvmap->get(write);
146                         if (writecv->synchronized_since(act))
147                                 break;
148                         if (write->get_location() == act->get_location()) {
149                                 //write is sc after act
150                                 merge(writecv, write, actcv);
151                                 changed = true;
152                                 break;
153                         }
154                 }
155         }
156         return changed;
157 }
158
159 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
160         bool changed = false;
161
162         /* Merge in the clock vector from the write */
163         const ModelAction *write = read->get_reads_from();
164         ClockVector *writecv = cvmap->get(write);
165         changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write));
166
167         for (int i = 0; i <= maxthreads; i++) {
168                 thread_id_t tid = int_to_id(i);
169                 if (tid == read->get_tid())
170                         continue;
171                 if (tid == write->get_tid())
172                         continue;
173                 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
174                 if (list == NULL)
175                         continue;
176                 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
177                         ModelAction *write2 = *rit;
178                         if (!write2->is_write())
179                                 continue;
180
181                         ClockVector *write2cv = cvmap->get(write2);
182                         if (write2cv == NULL)
183                                 continue;
184
185                         /* write -sc-> write2 &&
186                                  write -rf-> R =>
187                                  R -sc-> write2 */
188                         if (write2cv->synchronized_since(write)) {
189                                 changed |= merge(write2cv, write2, cv);
190                         }
191
192                         //looking for earliest write2 in iteration to satisfy this
193                         /* write2 -sc-> R &&
194                                  write -rf-> R =>
195                                  write2 -sc-> write */
196                         if (cv->synchronized_since(write2)) {
197                                 changed |= writecv == NULL || merge(writecv, write, write2cv);
198                                 break;
199                         }
200                 }
201         }
202         return changed;
203 }
204
205 void SCAnalysis::computeCV(action_list_t *list) {
206         bool changed = true;
207         bool firsttime = true;
208         ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
209         while (changed) {
210                 changed = changed&firsttime;
211                 firsttime = false;
212
213                 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
214                         ModelAction *act = *it;
215                         ModelAction *lastact = last_act[id_to_int(act->get_tid())];
216                         if (act->is_thread_start())
217                                 lastact = execution->get_thread(act)->get_creation();
218                         ClockVector *lastcv = (lastact != NULL) ? cvmap->get(lastact) : NULL;
219                         last_act[id_to_int(act->get_tid())] = act;
220                         ClockVector *cv = cvmap->get(act);
221                         if (cv == NULL) {
222                                 cv = new ClockVector(lastcv, act);
223                                 cvmap->put(act, cv);
224                         } else if (lastcv != NULL) {
225                                 merge(cv, act, lastcv);
226                         }
227                         if (act->is_thread_join()) {
228                                 Thread *joinedthr = act->get_thread_operand();
229                                 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
230                                 ClockVector *finishcv = cvmap->get(finish);
231                                 changed |= (finishcv == NULL) || merge(cv, act, finishcv);
232                         }
233                         if (act->is_read()) {
234                                 changed |= processRead(act, cv);
235                         }
236                 }
237                 /* Reset the last action array */
238                 if (changed) {
239                         bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
240                 }
241         }
242         model_free(last_act);
243 }