1 #include "scanalysis.h"
3 #include "threads-model.h"
4 #include "clockvector.h"
7 SCAnalysis::SCAnalysis(const ModelExecution *execution) :
17 SCAnalysis::~SCAnalysis() {
20 void SCAnalysis::print_list(action_list_t *list) {
21 model_print("---------------------------------------------------------------------\n");
23 model_print("Not SC\n");
24 unsigned int hash = 0;
26 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
27 const ModelAction *act = *it;
28 if (act->get_seq_number() > 0) {
29 if (badrfset.contains(act))
32 if (badrfset.contains(act)) {
33 model_print("Desired Rf: %u \n",badrfset.get(act)->get_seq_number());
36 hash = hash ^ (hash << 3) ^ ((*it)->hash());
38 model_print("HASH %u\n", hash);
39 model_print("---------------------------------------------------------------------\n");
42 void SCAnalysis::analyze(action_list_t *actions) {
43 action_list_t *list = generateSC(actions);
48 void SCAnalysis::check_rf(action_list_t *list) {
49 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
50 const ModelAction *act = *it;
52 if (act->get_reads_from()!=lastwrmap.get(act->get_location()))
53 badrfset.put(act,lastwrmap.get(act->get_location()));
56 lastwrmap.put(act->get_location(), act);
60 bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) {
61 ClockVector * cv2=cvmap.get(act2);
64 if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
66 //refuse to introduce cycles into clock vectors
70 return cv->merge(cv2);
73 int SCAnalysis::getNextActions(ModelAction ** array) {
76 for (int t = 0; t <= maxthreads; t++) {
77 action_list_t *tlt = &threadlists[t];
80 ModelAction *act = tlt->front();
81 ClockVector *cv = cvmap.get(act);
83 /* Find the earliest in SC ordering */
84 for (int i = 0; i <= maxthreads; i++) {
87 action_list_t *threadlist = &threadlists[i];
88 if (threadlist->empty())
90 ModelAction *first = threadlist->front();
91 if (cv->synchronized_since(first)) {
102 for (int t = 0; t <= maxthreads; t++) {
103 action_list_t *tlt = &threadlists[t];
106 ModelAction *act = tlt->front();
107 ClockVector *cv = act->get_cv();
109 /* Find the earliest in SC ordering */
110 for (int i = 0; i <= maxthreads; i++) {
113 action_list_t *threadlist = &threadlists[i];
114 if (threadlist->empty())
116 ModelAction *first = threadlist->front();
117 if (cv->synchronized_since(first)) {
127 ASSERT(count==0 || cyclic);
132 ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) {
137 /* Choose first non-write action */
138 ModelAction *nonwrite=NULL;
139 for(int i=0;i<count;i++) {
140 if (!array[i]->is_write())
141 if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number())
144 if (nonwrite != NULL)
147 /* Look for non-conflicting action */
148 ModelAction *nonconflict=NULL;
149 for(int a=0;a<count;a++) {
150 ModelAction *act=array[a];
151 for (int i = 0; i <= maxthreads && act != NULL; i++) {
152 thread_id_t tid = int_to_id(i);
153 if (tid == act->get_tid())
156 action_list_t *list = &threadlists[id_to_int(tid)];
157 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
158 ModelAction *write = *rit;
159 if (!write->is_write())
161 ClockVector *writecv = cvmap.get(write);
162 if (writecv->synchronized_since(act))
164 if (write->get_location() == act->get_location()) {
165 //write is sc after act
172 if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number())
179 action_list_t * SCAnalysis::generateSC(action_list_t *list) {
180 int numactions=buildVectors(list);
183 action_list_t *sclist = new action_list_t();
184 ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
185 int * choices = (int *) model_calloc(1, sizeof(int)*numactions);
190 int numActions = getNextActions(array);
193 ModelAction * act=pruneArray(array, numActions);
195 if (currchoice < endchoice) {
196 act = array[choices[currchoice]];
197 //check whether there is still another option
198 if ((choices[currchoice]+1)<numActions)
199 lastchoice=currchoice;
203 choices[currchoice]=0;
205 lastchoice=currchoice;
209 thread_id_t tid = act->get_tid();
211 threadlists[id_to_int(tid)].pop_front();
212 //add ordering constraints from this choice
213 if (updateConstraints(act)) {
214 //propagate changes if we have them
217 if (!prevc && cyclic) {
218 model_print("ROLLBACK in SC\n");
219 //check whether we have another choice
220 if (lastchoice != -1) {
221 //have to reset everything
222 choices[lastchoice]++;
223 endchoice=lastchoice+1;
235 sclist->push_back(act);
241 int SCAnalysis::buildVectors(action_list_t *list) {
244 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
245 ModelAction *act = *it;
247 int threadid = id_to_int(act->get_tid());
248 if (threadid > maxthreads) {
249 threadlists.resize(threadid + 1);
250 maxthreads = threadid;
252 threadlists[threadid].push_back(act);
257 void SCAnalysis::reset(action_list_t *list) {
258 for (int t = 0; t <= maxthreads; t++) {
259 action_list_t *tlt = &threadlists[t];
262 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
263 ModelAction *act = *it;
264 delete cvmap.get(act);
265 cvmap.put(act, NULL);
271 bool SCAnalysis::updateConstraints(ModelAction *act) {
272 bool changed = false;
273 for (int i = 0; i <= maxthreads; i++) {
274 thread_id_t tid = int_to_id(i);
275 if (tid == act->get_tid())
278 action_list_t *list = &threadlists[id_to_int(tid)];
279 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
280 ModelAction *write = *rit;
281 if (!write->is_write())
283 ClockVector *writecv = cvmap.get(write);
284 if (writecv->synchronized_since(act))
286 if (write->get_location() == act->get_location()) {
287 //write is sc after act
288 merge(writecv, write, act);
297 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
298 bool changed = false;
300 /* Merge in the clock vector from the write */
301 const ModelAction *write = read->get_reads_from();
302 ClockVector *writecv = cvmap.get(write);
303 changed |= merge(cv, read, write) && (*read < *write);
305 for (int i = 0; i <= maxthreads; i++) {
306 thread_id_t tid = int_to_id(i);
307 if (tid == read->get_tid())
309 if (tid == write->get_tid())
311 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
314 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
315 ModelAction *write2 = *rit;
316 if (!write2->is_write())
319 ClockVector *write2cv = cvmap.get(write2);
320 if (write2cv == NULL)
323 /* write -sc-> write2 &&
326 if (write2cv->synchronized_since(write)) {
327 changed |= merge(write2cv, write2, read);
330 //looking for earliest write2 in iteration to satisfy this
333 write2 -sc-> write */
334 if (cv->synchronized_since(write2)) {
335 changed |= writecv==NULL || merge(writecv, write, write2);
343 void SCAnalysis::computeCV(action_list_t *list) {
345 bool firsttime = true;
346 ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
348 changed = changed&firsttime;
351 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
352 ModelAction *act = *it;
353 ModelAction *lastact = last_act[id_to_int(act->get_tid())];
354 if (act->is_thread_start())
355 lastact = execution->get_thread(act)->get_creation();
356 last_act[id_to_int(act->get_tid())] = act;
357 ClockVector *cv = cvmap.get(act);
359 cv = new ClockVector(NULL, act);
362 if (lastact != NULL) {
363 merge(cv, act, lastact);
365 if (act->is_thread_join()) {
366 Thread *joinedthr = act->get_thread_operand();
367 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
368 changed |= merge(cv, act, finish);
370 if (act->is_read()) {
371 changed |= processRead(act, cv);
374 /* Reset the last action array */
376 bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
379 model_free(last_act);