Remove special cases for printing SC executions.
[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         /* Find the earliest in SC ordering */
55         for (int i = 0; i <= maxthreads; i++) {
56                 action_list_t *threadlist = &threadlists[i];
57                 if (threadlist->empty())
58                         continue;
59                 ModelAction *first = threadlist->front();
60                 if (act==NULL) {
61                         act=first;
62                         continue;
63                 }
64                 ClockVector *cv = cvmap.get(act);
65                 if (cv->synchronized_since(first)) {
66                         act = first;
67                 }
68         }
69         if (act == NULL)
70                 return act;
71
72
73         /* Find the model action with the earliest sequence number in case of a cycle.
74          */
75
76         for (int i = 0; i <= maxthreads; i++) {
77                 action_list_t *threadlist = &threadlists[i];
78                 if (threadlist->empty())
79                         continue;
80                 ModelAction *first = threadlist->front();
81                 ClockVector *cv = cvmap.get(act);
82                 ClockVector *cvfirst = cvmap.get(first);
83                 if (first->get_seq_number()<act->get_seq_number()&&
84                                 (cv->synchronized_since(first)||!cvfirst->synchronized_since(act))) {
85                         act=first;
86                 }
87         }
88
89         /* See if hb demands an earlier action. */
90         for (int i = 0; i <= maxthreads; i++) {
91                 action_list_t *threadlist = &threadlists[i];
92                 if (threadlist->empty())
93                         continue;
94                 ModelAction *first = threadlist->front();
95                 ClockVector *cv = act->get_cv();
96                 if (cv->synchronized_since(first)) {
97                         act = first;
98                 }
99         }
100         return act;
101 }
102
103 action_list_t * SCAnalysis::generateSC(action_list_t *list) {
104         action_list_t *sclist = new action_list_t();
105         while (true) {
106                 ModelAction *act = getNextAction();
107                 if (act == NULL)
108                         break;
109                 thread_id_t tid = act->get_tid();
110                 //remove action
111                 threadlists[id_to_int(tid)].pop_front();
112                 //add ordering constraints from this choice
113                 if (updateConstraints(act)) {
114                         //propagate changes if we have them
115                         computeCV(list);
116                 }
117                 //add action to end
118                 sclist->push_back(act);
119         }
120         return sclist;
121 }
122
123 void SCAnalysis::buildVectors(action_list_t *list) {
124         maxthreads = 0;
125         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
126                 ModelAction *act = *it;
127                 int threadid = id_to_int(act->get_tid());
128                 if (threadid > maxthreads) {
129                         threadlists.resize(threadid + 1);
130                         maxthreads = threadid;
131                 }
132                 threadlists[threadid].push_back(act);
133         }
134 }
135
136 bool SCAnalysis::updateConstraints(ModelAction *act) {
137         bool changed = false;
138         ClockVector *actcv = cvmap.get(act);
139         for (int i = 0; i <= maxthreads; i++) {
140                 thread_id_t tid = int_to_id(i);
141                 if (tid == act->get_tid())
142                         continue;
143
144                 action_list_t *list = &threadlists[id_to_int(tid)];
145                 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
146                         ModelAction *write = *rit;
147                         if (!write->is_write())
148                                 continue;
149                         ClockVector *writecv = cvmap.get(write);
150                         if (writecv->synchronized_since(act))
151                                 break;
152                         if (write->get_location() == act->get_location()) {
153                                 //write is sc after act
154                                 merge(writecv, write, actcv);
155                                 changed = true;
156                                 break;
157                         }
158                 }
159         }
160         return changed;
161 }
162
163 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
164         bool changed = false;
165
166         /* Merge in the clock vector from the write */
167         const ModelAction *write = read->get_reads_from();
168         ClockVector *writecv = cvmap.get(write);
169         changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write));
170
171         for (int i = 0; i <= maxthreads; i++) {
172                 thread_id_t tid = int_to_id(i);
173                 if (tid == read->get_tid())
174                         continue;
175                 if (tid == write->get_tid())
176                         continue;
177                 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
178                 if (list == NULL)
179                         continue;
180                 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
181                         ModelAction *write2 = *rit;
182                         if (!write2->is_write())
183                                 continue;
184
185                         ClockVector *write2cv = cvmap.get(write2);
186                         if (write2cv == NULL)
187                                 continue;
188
189                         /* write -sc-> write2 &&
190                                  write -rf-> R =>
191                                  R -sc-> write2 */
192                         if (write2cv->synchronized_since(write)) {
193                                 changed |= merge(write2cv, write2, cv);
194                         }
195
196                         //looking for earliest write2 in iteration to satisfy this
197                         /* write2 -sc-> R &&
198                                  write -rf-> R =>
199                                  write2 -sc-> write */
200                         if (cv->synchronized_since(write2)) {
201                                 changed |= writecv == NULL || merge(writecv, write, write2cv);
202                                 break;
203                         }
204                 }
205         }
206         return changed;
207 }
208
209 void SCAnalysis::computeCV(action_list_t *list) {
210         bool changed = true;
211         bool firsttime = true;
212         ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
213         while (changed) {
214                 changed = changed&firsttime;
215                 firsttime = false;
216
217                 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
218                         ModelAction *act = *it;
219                         ModelAction *lastact = last_act[id_to_int(act->get_tid())];
220                         if (act->is_thread_start())
221                                 lastact = execution->get_thread(act)->get_creation();
222                         ClockVector *lastcv = (lastact != NULL) ? cvmap.get(lastact) : NULL;
223                         last_act[id_to_int(act->get_tid())] = act;
224                         ClockVector *cv = cvmap.get(act);
225                         if (cv == NULL) {
226                                 cv = new ClockVector(lastcv, act);
227                                 cvmap.put(act, cv);
228                         } else if (lastcv != NULL) {
229                                 merge(cv, act, lastcv);
230                         }
231                         if (act->is_thread_join()) {
232                                 Thread *joinedthr = act->get_thread_operand();
233                                 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
234                                 ClockVector *finishcv = cvmap.get(finish);
235                                 changed |= (finishcv == NULL) || merge(cv, act, finishcv);
236                         }
237                         if (act->is_read()) {
238                                 changed |= processRead(act, cv);
239                         }
240                 }
241                 /* Reset the last action array */
242                 if (changed) {
243                         bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
244                 }
245         }
246         model_free(last_act);
247 }