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