X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=scanalysis.cc;h=98dd8eb43d43bd729a59139dff778a93ceb9fd48;hb=6a2d1dcdcff89e68d8a2fe9de1f38ecfac345caf;hp=d3120fc3f612518f5bca1b5b80aed3f813454147;hpb=49e01b46a51804ca1aef3e4c260d832b38d40bdc;p=model-checker.git diff --git a/scanalysis.cc b/scanalysis.cc index d3120fc..98dd8eb 100644 --- a/scanalysis.cc +++ b/scanalysis.cc @@ -5,32 +5,33 @@ #include "execution.h" SCAnalysis::SCAnalysis(const ModelExecution *execution) : + cvmap(), + cyclic(false), + badrfset(), + lastwrmap(), + threadlists(1), execution(execution) { - cvmap = new HashTable (); - cycleset = new HashTable (); - threadlists = new SnapVector (1); } SCAnalysis::~SCAnalysis() { - delete cvmap; - delete cycleset; - delete threadlists; } void SCAnalysis::print_list(action_list_t *list) { - action_list_t::iterator it; - model_print("---------------------------------------------------------------------\n"); - + if (cyclic) + model_print("Not SC\n"); unsigned int hash = 0; - for (it = list->begin(); it != list->end(); it++) { + for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { const ModelAction *act = *it; if (act->get_seq_number() > 0) { - if (cycleset->contains(act)) - model_print("CYC"); + if (badrfset.contains(act)) + model_print("BRF "); act->print(); + if (badrfset.contains(act)) { + model_print("Desired Rf: %u \n", badrfset.get(act)->get_seq_number()); + } } hash = hash ^ (hash << 3) ^ ((*it)->hash()); } @@ -39,115 +40,252 @@ void SCAnalysis::print_list(action_list_t *list) { } void SCAnalysis::analyze(action_list_t *actions) { - buildVectors(actions); - computeCV(actions); action_list_t *list = generateSC(actions); + check_rf(list); print_list(list); } -bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2) { +void SCAnalysis::check_rf(action_list_t *list) { + for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { + const ModelAction *act = *it; + if (act->is_read()) { + if (act->get_reads_from() != lastwrmap.get(act->get_location())) + badrfset.put(act, lastwrmap.get(act->get_location())); + } + if (act->is_write()) + lastwrmap.put(act->get_location(), act); + } +} + +bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) { + ClockVector *cv2 = cvmap.get(act2); + if (cv2 == NULL) + return true; if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) { - cycleset->put(act, act); + cyclic = true; + //refuse to introduce cycles into clock vectors + return false; } + return cv->merge(cv2); } -ModelAction * SCAnalysis::getNextAction() { - ModelAction *act = NULL; - for (int i = 0; i <= maxthreads; i++) { - action_list_t *threadlist = &(*threadlists)[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - if (act == NULL) { - act = first; +int SCAnalysis::getNextActions(ModelAction ** array) { + int count=0; + + for (int t = 0; t <= maxthreads; t++) { + action_list_t *tlt = &threadlists[t]; + if (tlt->empty()) continue; + ModelAction *act = tlt->front(); + ClockVector *cv = cvmap.get(act); + + /* Find the earliest in SC ordering */ + for (int i = 0; i <= maxthreads; i++) { + if ( i == t ) + continue; + action_list_t *threadlist = &threadlists[i]; + if (threadlist->empty()) + continue; + ModelAction *first = threadlist->front(); + if (cv->synchronized_since(first)) { + act = NULL; + break; + } } - ClockVector *cv = cvmap->get(act); - if (cv->synchronized_since(first)) { - act = first; + if (act != NULL) { + array[count++]=act; } } - if (act == NULL) - return act; - //print cycles in a nice way to avoid confusion - //make sure thread starts appear after the create - if (act->is_thread_start()) { - ModelAction *createact = execution->get_thread(act)->get_creation(); - if (createact) { - action_list_t *threadlist = &(*threadlists)[id_to_int(createact->get_tid())]; - if (!threadlist->empty()) { - ModelAction *first = threadlist->front(); - if (first->get_seq_number() <= createact->get_seq_number()) - act = first; + if (count != 0) + return count; + for (int t = 0; t <= maxthreads; t++) { + action_list_t *tlt = &threadlists[t]; + if (tlt->empty()) + continue; + ModelAction *act = tlt->front(); + ClockVector *cv = act->get_cv(); + + /* Find the earliest in SC ordering */ + for (int i = 0; i <= maxthreads; i++) { + if ( i == t ) + continue; + action_list_t *threadlist = &threadlists[i]; + if (threadlist->empty()) + continue; + ModelAction *first = threadlist->front(); + if (cv->synchronized_since(first)) { + act = NULL; + break; } } + if (act != NULL) { + array[count++]=act; + } } - //make sure that joins appear after the thread is finished - if (act->is_thread_join()) { - int jointhread = id_to_int(act->get_thread_operand()->get_id()); - action_list_t *threadlist = &(*threadlists)[jointhread]; - if (!threadlist->empty()) { - act = threadlist->front(); + ASSERT(count==0 || cyclic); + + return count; +} + +ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) { + /* No choice */ + if (count == 1) + return array[0]; + + /* Choose first non-write action */ + ModelAction *nonwrite=NULL; + for(int i=0;iis_write()) + if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number()) + nonwrite = array[i]; + } + if (nonwrite != NULL) + return nonwrite; + + /* Look for non-conflicting action */ + ModelAction *nonconflict=NULL; + for(int a=0;aget_tid()) + continue; + + action_list_t *list = &threadlists[id_to_int(tid)]; + for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) { + ModelAction *write = *rit; + if (!write->is_write()) + continue; + ClockVector *writecv = cvmap.get(write); + if (writecv->synchronized_since(act)) + break; + if (write->get_location() == act->get_location()) { + //write is sc after act + act = NULL; + break; + } + } + } + if (act != NULL) { + if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number()) + nonconflict=act; } } - - return act; + return nonconflict; } action_list_t * SCAnalysis::generateSC(action_list_t *list) { + int numactions=buildVectors(list); + computeCV(list); + action_list_t *sclist = new action_list_t(); + ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *)); + int * choices = (int *) model_calloc(1, sizeof(int)*numactions); + int endchoice = 0; + int currchoice = 0; + int lastchoice = -1; while (true) { - ModelAction *act = getNextAction(); - if (act == NULL) + int numActions = getNextActions(array); + if (numActions == 0) break; + ModelAction * act=pruneArray(array, numActions); + if (act == NULL) { + if (currchoice < endchoice) { + act = array[choices[currchoice]]; + //check whether there is still another option + if ((choices[currchoice]+1)1) + lastchoice=currchoice; + currchoice++; + } + } thread_id_t tid = act->get_tid(); //remove action - (*threadlists)[id_to_int(tid)].pop_front(); + threadlists[id_to_int(tid)].pop_front(); //add ordering constraints from this choice if (updateConstraints(act)) { //propagate changes if we have them + bool prevc=cyclic; computeCV(list); + if (!prevc && cyclic) { + model_print("ROLLBACK in SC\n"); + //check whether we have another choice + if (lastchoice != -1) { + //have to reset everything + choices[lastchoice]++; + endchoice=lastchoice+1; + currchoice=0; + lastchoice=-1; + reset(list); + buildVectors(list); + computeCV(list); + sclist->clear(); + continue; + } + } } //add action to end sclist->push_back(act); } + model_free(array); return sclist; } -void SCAnalysis::buildVectors(action_list_t *list) { +int SCAnalysis::buildVectors(action_list_t *list) { maxthreads = 0; + int numactions = 0; for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { ModelAction *act = *it; + numactions++; int threadid = id_to_int(act->get_tid()); if (threadid > maxthreads) { - threadlists->resize(threadid + 1); + threadlists.resize(threadid + 1); maxthreads = threadid; } - (*threadlists)[threadid].push_back(act); + threadlists[threadid].push_back(act); } + return numactions; +} + +void SCAnalysis::reset(action_list_t *list) { + for (int t = 0; t <= maxthreads; t++) { + action_list_t *tlt = &threadlists[t]; + tlt->clear(); + } + for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { + ModelAction *act = *it; + delete cvmap.get(act); + cvmap.put(act, NULL); + } + + cyclic=false; } bool SCAnalysis::updateConstraints(ModelAction *act) { bool changed = false; - ClockVector *actcv = cvmap->get(act); for (int i = 0; i <= maxthreads; i++) { thread_id_t tid = int_to_id(i); if (tid == act->get_tid()) continue; - action_list_t *list = &(*threadlists)[id_to_int(tid)]; + action_list_t *list = &threadlists[id_to_int(tid)]; for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) { ModelAction *write = *rit; if (!write->is_write()) continue; - ClockVector *writecv = cvmap->get(write); + ClockVector *writecv = cvmap.get(write); if (writecv->synchronized_since(act)) break; if (write->get_location() == act->get_location()) { //write is sc after act - merge(writecv, write, actcv); + merge(writecv, write, act); changed = true; break; } @@ -161,8 +299,8 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { /* Merge in the clock vector from the write */ const ModelAction *write = read->get_reads_from(); - ClockVector *writecv = cvmap->get(write); - changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write)); + ClockVector *writecv = cvmap.get(write); + changed |= merge(cv, read, write) && (*read < *write); for (int i = 0; i <= maxthreads; i++) { thread_id_t tid = int_to_id(i); @@ -178,7 +316,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { if (!write2->is_write()) continue; - ClockVector *write2cv = cvmap->get(write2); + ClockVector *write2cv = cvmap.get(write2); if (write2cv == NULL) continue; @@ -186,7 +324,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { write -rf-> R => R -sc-> write2 */ if (write2cv->synchronized_since(write)) { - changed |= merge(write2cv, write2, cv); + changed |= merge(write2cv, write2, read); } //looking for earliest write2 in iteration to satisfy this @@ -194,7 +332,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { write -rf-> R => write2 -sc-> write */ if (cv->synchronized_since(write2)) { - changed |= writecv == NULL || merge(writecv, write, write2cv); + changed |= writecv == NULL || merge(writecv, write, write2); break; } } @@ -215,20 +353,19 @@ void SCAnalysis::computeCV(action_list_t *list) { ModelAction *lastact = last_act[id_to_int(act->get_tid())]; if (act->is_thread_start()) lastact = execution->get_thread(act)->get_creation(); - ClockVector *lastcv = (lastact != NULL) ? cvmap->get(lastact) : NULL; last_act[id_to_int(act->get_tid())] = act; - ClockVector *cv = cvmap->get(act); + ClockVector *cv = cvmap.get(act); if (cv == NULL) { - cv = new ClockVector(lastcv, act); - cvmap->put(act, cv); - } else if (lastcv != NULL) { - merge(cv, act, lastcv); + cv = new ClockVector(NULL, act); + cvmap.put(act, cv); + } + if (lastact != NULL) { + merge(cv, act, lastact); } if (act->is_thread_join()) { Thread *joinedthr = act->get_thread_operand(); ModelAction *finish = execution->get_last_action(joinedthr->get_id()); - ClockVector *finishcv = cvmap->get(finish); - changed |= (finishcv == NULL) || merge(cv, act, finishcv); + changed |= merge(cv, act, finish); } if (act->is_read()) { changed |= processRead(act, cv);