3 SCGenerator::SCGenerator() :
15 stats(new struct sc_statistics),
16 annotationMode(false) {
19 SCGenerator::~SCGenerator() {
22 bool SCGenerator::getCyclic() {
23 return cyclic || hasBadRF;
26 SnapVector<action_list_t>* SCGenerator::getDupThreadLists() {
27 return &dup_threadlists;
30 struct sc_statistics* SCGenerator::getStats() {
34 void SCGenerator::setExecution(ModelExecution *execution) {
35 this->execution = execution;
38 void SCGenerator::setActions(action_list_t *actions) {
39 this->actions = actions;
42 void SCGenerator::setPrintAlways(bool val) {
43 this->print_always = val;
46 bool SCGenerator::getPrintAlways() {
47 return this->print_always;
50 bool SCGenerator::getHasBadRF() {
51 return this->hasBadRF;
54 void SCGenerator::setPrintBuggy(bool val) {
55 this->print_buggy = val;
58 void SCGenerator::setPrintNonSC(bool val) {
59 this->print_nonsc = val;
62 void SCGenerator::setAnnotationMode(bool val) {
63 this->annotationMode = val;
66 action_list_t * SCGenerator::getSCList() {
68 struct timeval finish;
69 gettimeofday(&start, NULL);
71 /* Build up the thread lists for general purpose */
73 buildVectors(&dup_threadlists, &thrdNum, actions);
76 action_list_t *list = generateSC(actions);
81 list = generateSC(actions);
84 gettimeofday(&finish, NULL);
85 stats->elapsedtime+=((finish.tv_sec*1000000+finish.tv_usec)-(start.tv_sec*1000000+start.tv_usec));
90 HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4> * SCGenerator::getBadrfset() {
94 HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > * SCGenerator::getAnnotatedReadSet() {
95 return &annotatedReadSet;
98 void SCGenerator::print_list(action_list_t *list) {
99 model_print("---------------------------------------------------------------------\n");
100 if (cyclic || hasBadRF)
101 model_print("Not SC\n");
102 unsigned int hash = 0;
104 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
105 const ModelAction *act = *it;
106 if (act->get_seq_number() > 0) {
107 if (badrfset.contains(act))
110 if (badrfset.contains(act)) {
111 model_print("Desired Rf: %u \n", badrfset.get(act)->get_seq_number());
114 hash = hash ^ (hash << 3) ^ ((*it)->hash());
116 model_print("HASH %u\n", hash);
117 model_print("---------------------------------------------------------------------\n");
121 action_list_t * SCGenerator::generateSC(action_list_t *list) {
122 int numactions=buildVectors(&threadlists, &maxthreads, list);
123 stats->actions+=numactions;
125 // Analyze which actions we should ignore in the partially SC analysis
126 if (annotationMode) {
127 collectAnnotatedReads();
128 if (annotationError) {
129 model_print("Annotation error!\n");
136 action_list_t *sclist = new action_list_t();
137 ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
138 int * choices = (int *) model_calloc(1, sizeof(int)*numactions);
143 int numActions = getNextActions(array);
146 ModelAction * act=pruneArray(array, numActions);
148 if (currchoice < endchoice) {
149 act = array[choices[currchoice]];
150 //check whether there is still another option
151 if ((choices[currchoice]+1)<numActions)
152 lastchoice=currchoice;
156 choices[currchoice]=0;
158 lastchoice=currchoice;
162 thread_id_t tid = act->get_tid();
164 threadlists[id_to_int(tid)].pop_front();
165 //add ordering constraints from this choice
166 if (updateConstraints(act)) {
167 //propagate changes if we have them
170 if (!prevc && cyclic) {
171 model_print("ROLLBACK in SC\n");
172 //check whether we have another choice
173 if (lastchoice != -1) {
174 //have to reset everything
175 choices[lastchoice]++;
176 endchoice=lastchoice+1;
181 buildVectors(&threadlists, &maxthreads, list);
190 sclist->push_back(act);
196 void SCGenerator::update_stats() {
204 int SCGenerator::buildVectors(SnapVector<action_list_t> *threadlist, int *maxthread,
205 action_list_t *list) {
208 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
209 ModelAction *act = *it;
211 int threadid = id_to_int(act->get_tid());
212 if (threadid > *maxthread) {
213 threadlist->resize(threadid + 1);
214 *maxthread = threadid;
216 (*threadlist)[threadid].push_back(act);
222 bool SCGenerator::updateConstraints(ModelAction *act) {
223 bool changed = false;
224 for (int i = 0; i <= maxthreads; i++) {
225 thread_id_t tid = int_to_id(i);
226 if (tid == act->get_tid())
229 action_list_t *list = &threadlists[id_to_int(tid)];
230 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
231 ModelAction *write = *rit;
232 if (!write->is_write())
234 ClockVector *writecv = cvmap.get(write);
235 if (writecv->synchronized_since(act))
237 if (write->get_location() == act->get_location()) {
238 //write is sc after act
239 merge(writecv, write, act);
248 void SCGenerator::computeCV(action_list_t *list) {
250 bool firsttime = true;
251 ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
254 changed = changed&firsttime;
256 bool updateFuture = false;
258 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
259 ModelAction *act = *it;
260 ModelAction *lastact = last_act[id_to_int(act->get_tid())];
261 if (act->is_thread_start())
262 lastact = execution->get_thread(act)->get_creation();
263 last_act[id_to_int(act->get_tid())] = act;
264 ClockVector *cv = cvmap.get(act);
266 cv = new ClockVector(act->get_cv(), act);
270 if (lastact != NULL) {
271 merge(cv, act, lastact);
273 if (act->is_thread_join()) {
274 Thread *joinedthr = act->get_thread_operand();
275 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
276 changed |= merge(cv, act, finish);
278 if (act->is_read()) {
280 changed |= processReadFast(act, cv);
281 } else if (annotatedReadSet.contains(act)) {
282 changed |= processAnnotatedReadSlow(act, cv, &updateFuture);
284 changed |= processReadSlow(act, cv, &updateFuture);
288 /* Reset the last action array */
290 bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
302 model_free(last_act);
305 bool SCGenerator::processReadFast(ModelAction *read, ClockVector *cv) {
306 bool changed = false;
308 /* Merge in the clock vector from the write */
309 const ModelAction *write = read->get_reads_from();
310 if (!write) { // The case where the write is a promise
313 ClockVector *writecv = cvmap.get(write);
314 changed |= merge(cv, read, write) && (*read < *write);
316 for (int i = 0; i <= maxthreads; i++) {
317 thread_id_t tid = int_to_id(i);
318 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
321 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
322 ModelAction *write2 = *rit;
323 if (!write2->is_write())
327 if (write2 == read) // If read is a RMW
330 ClockVector *write2cv = cvmap.get(write2);
331 if (write2cv == NULL)
333 /* write -sc-> write2 &&
336 if (write2cv->synchronized_since(write)) {
337 changed |= merge(write2cv, write2, read);
341 //looking for earliest write2 in iteration to satisfy this
344 write2 -sc-> write */
345 if (cv->synchronized_since(write2)) {
346 changed |= writecv == NULL || merge(writecv, write, write2);
354 bool SCGenerator::processReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture) {
355 bool changed = false;
357 /* Merge in the clock vector from the write */
358 const ModelAction *write = read->get_reads_from();
359 ClockVector *writecv = cvmap.get(write);
360 if ((*write < *read) || ! *updateFuture) {
361 bool status = merge(cv, read, write) && (*read < *write);
363 *updateFuture = status;
366 for (int i = 0; i <= maxthreads; i++) {
367 thread_id_t tid = int_to_id(i);
368 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
371 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
372 ModelAction *write2 = *rit;
373 if (!write2->is_write())
377 if (write2 == read) // If read is a RMW
380 ClockVector *write2cv = cvmap.get(write2);
381 if (write2cv == NULL)
384 /* write -sc-> write2 &&
387 if (write2cv->synchronized_since(write)) {
388 if ((*read < *write2) || ! *updateFuture) {
389 bool status = merge(write2cv, write2, read);
391 *updateFuture |= status && (*write2 < *read);
395 //looking for earliest write2 in iteration to satisfy this
398 write2 -sc-> write */
399 if (cv->synchronized_since(write2)) {
400 if ((*write2 < *write) || ! *updateFuture) {
401 bool status = writecv == NULL || merge(writecv, write, write2);
403 *updateFuture |= status && (*write < *write2);
412 bool SCGenerator::processAnnotatedReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture) {
413 bool changed = false;
415 /* Merge in the clock vector from the write */
416 const ModelAction *write = read->get_reads_from();
417 if ((*write < *read) || ! *updateFuture) {
418 bool status = merge(cv, read, write) && (*read < *write);
420 *updateFuture = status;
425 int SCGenerator::getNextActions(ModelAction **array) {
428 for (int t = 0; t <= maxthreads; t++) {
429 action_list_t *tlt = &threadlists[t];
432 ModelAction *act = tlt->front();
433 ClockVector *cv = cvmap.get(act);
435 /* Find the earliest in SC ordering */
436 for (int i = 0; i <= maxthreads; i++) {
439 action_list_t *threadlist = &threadlists[i];
440 if (threadlist->empty())
442 ModelAction *first = threadlist->front();
443 if (cv->synchronized_since(first)) {
454 for (int t = 0; t <= maxthreads; t++) {
455 action_list_t *tlt = &threadlists[t];
458 ModelAction *act = tlt->front();
459 ClockVector *cv = act->get_cv();
461 /* Find the earliest in SC ordering */
462 for (int i = 0; i <= maxthreads; i++) {
465 action_list_t *threadlist = &threadlists[i];
466 if (threadlist->empty())
468 ModelAction *first = threadlist->front();
469 if (cv->synchronized_since(first)) {
479 ASSERT(count==0 || cyclic);
484 bool SCGenerator::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) {
485 ClockVector *cv2 = cvmap.get(act2);
489 if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
491 //refuse to introduce cycles into clock vectors
495 bool status = cv->merge(cv2);
500 merged = cv->merge(cv2);
505 if (act2->happens_before(act) ||
506 (act->is_seqcst() && act2->is_seqcst() && *act2 < *act)) {
507 return cv->merge(cv2);
516 void SCGenerator::check_rf1(action_list_t *list) {
517 bool hasBadRF1 = false;
518 HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset1;
519 HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap1;
520 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
521 const ModelAction *act = *it;
522 if (act->is_read()) {
523 if (act->get_reads_from() != lastwrmap1.get(act->get_location())) {
524 badrfset1.put(act, lastwrmap1.get(act->get_location()));
529 lastwrmap1.put(act->get_location(), act);
531 if (cyclic != hasBadRF1 && !annotationMode) {
533 model_print("Assert failure & non-SC\n");
535 model_print("Assert failure & SC\n");
537 model_print("Fast\n");
539 model_print("Slow\n");
543 if (!annotationMode) {
544 ASSERT (cyclic == hasBadRF1);
548 void SCGenerator::check_rf(action_list_t *list) {
550 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
551 const ModelAction *act = *it;
552 if (act->is_read()) {
553 const ModelAction *write = act->get_reads_from();
554 if (write && write != lastwrmap.get(act->get_location())) {
555 badrfset.put(act, lastwrmap.get(act->get_location()));
560 lastwrmap.put(act->get_location(), act);
562 if (cyclic != hasBadRF && !annotationMode) {
564 model_print("Assert failure & non-SC\n");
566 model_print("Assert failure & SC\n");
568 model_print("Fast\n");
570 model_print("Slow\n");
574 if (!annotationMode) {
575 ASSERT (cyclic == hasBadRF);
579 void SCGenerator::reset(action_list_t *list) {
580 for (int t = 0; t <= maxthreads; t++) {
581 action_list_t *tlt = &threadlists[t];
584 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
585 ModelAction *act = *it;
586 delete cvmap.get(act);
587 cvmap.put(act, NULL);
593 ModelAction* SCGenerator::pruneArray(ModelAction **array, int count) {
598 /* Choose first non-write action */
599 ModelAction *nonwrite=NULL;
600 for(int i=0;i<count;i++) {
601 if (!array[i]->is_write())
602 if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number())
605 if (nonwrite != NULL)
608 /* Look for non-conflicting action */
609 ModelAction *nonconflict=NULL;
610 for(int a=0;a<count;a++) {
611 ModelAction *act=array[a];
612 for (int i = 0; i <= maxthreads && act != NULL; i++) {
613 thread_id_t tid = int_to_id(i);
614 if (tid == act->get_tid())
617 action_list_t *list = &threadlists[id_to_int(tid)];
618 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
619 ModelAction *write = *rit;
620 if (!write->is_write())
622 ClockVector *writecv = cvmap.get(write);
623 if (writecv->synchronized_since(act))
625 if (write->get_location() == act->get_location()) {
626 //write is sc after act
633 if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number())
640 /** This routine is operated based on the built threadlists */
641 void SCGenerator::collectAnnotatedReads() {
642 for (unsigned i = 1; i < threadlists.size(); i++) {
643 action_list_t *list = &threadlists.at(i);
644 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
645 ModelAction *act = *it;
646 if (!IS_SC_ANNO(act))
648 if (!IS_ANNO_BEGIN(act)) {
649 model_print("SC annotation should begin with a BEGIN annotation\n");
650 annotationError = true;
654 while (!IS_ANNO_END(act) && it != list->end()) {
655 // Look for the actions to keep in this loop
656 ModelAction *nextAct = *++it;
657 if (!IS_ANNO_KEEP(nextAct)) { // Annotated reads
659 annotatedReadSet.put(act, act);
660 annotatedReadSetSize++;
661 if (IS_ANNO_END(nextAct))
665 if (it == list->end()) {
666 model_print("SC annotation should end with a END annotation\n");
667 annotationError = true;