X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scanalysis.cc;h=13aada1a8fee202149f11b94b8ab3a9078971d39;hp=ff7854a87e8a31aec8e3ae105d403ad0b3559c66;hb=a4d3f2ae3f3a9e2a30cc36c92cee9f83bb09e9b1;hpb=2cd228006768bd0a4e083616a5c6bda4e1fe3507 diff --git a/scanalysis.cc b/scanalysis.cc index ff7854a..13aada1 100644 --- a/scanalysis.cc +++ b/scanalysis.cc @@ -2,150 +2,325 @@ #include "action.h" #include "threads-model.h" #include "clockvector.h" +#include "execution.h" -SCAnalysis::SCAnalysis() { - cvmap=new HashTable(); - cycleset=new HashTable(); - threadlists=new SnapVector(1); +SCAnalysis::SCAnalysis() : + cvmap(), + cyclic(false), + badrfset(), + lastwrmap(), + threadlists(1), + execution(NULL), + print_always(false), + print_buggy(true) +{ } SCAnalysis::~SCAnalysis() { - delete cvmap; - delete cycleset; - delete threadlists; } -void SCAnalysis::print_list(action_list_t *list) { - action_list_t::iterator it; +void SCAnalysis::setExecution(ModelExecution * execution) { + this->execution=execution; +} - model_print("---------------------------------------------------------------------\n"); +const char * SCAnalysis::name() { + const char * name = "SC"; + return name; +} +bool SCAnalysis::option(char * opt) { + if (strcmp(opt, "verbose")==0) { + print_always=true; + return false; + } else if (strcmp(opt, "buggy")==0) { + return false; + } else if (strcmp(opt, "quiet")==0) { + print_buggy=false; + return false; + } if (strcmp(opt, "help") != 0) { + model_print("Unrecognized option: %s\n", opt); + } + + model_print("SC Analysis options\n"); + model_print("verbose -- print all feasible executions\n"); + model_print("buggy -- print only buggy executions (default)\n"); + model_print("quiet -- print nothing\n"); + model_print("\n"); + + return true; +} + +void SCAnalysis::print_list(action_list_t *list) { + 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()); + hash = hash ^ (hash << 3) ^ ((*it)->hash()); } model_print("HASH %u\n", hash); model_print("---------------------------------------------------------------------\n"); } -void SCAnalysis::analyze(action_list_t * actions) { - buildVectors(actions); - computeCV(actions); - action_list_t *list=generateSC(actions); - print_list(list); +void SCAnalysis::analyze(action_list_t *actions) { + action_list_t *list = generateSC(actions); + check_rf(list); + if (print_always || (print_buggy && execution->have_bug_reports())) + print_list(list); +} + +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, ClockVector *cv2) { - if (cv2->getClock(act->get_tid())>=act->get_seq_number() && act->get_seq_number() != 0) { - cycleset->put(act, 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) { + 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=model->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) { - action_list_t *sclist=new action_list_t(); + 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; - thread_id_t tid=act->get_tid(); + 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) { - maxthreads=0; +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; - int threadid=id_to_int(act->get_tid()); + numactions++; + int threadid = id_to_int(act->get_tid()); if (threadid > maxthreads) { - threadlists->resize(threadid+1); - maxthreads=threadid; + 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()) + bool changed = false; + 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); - changed=true; + merge(writecv, write, act); + changed = true; break; } } @@ -154,28 +329,28 @@ bool SCAnalysis::updateConstraints(ModelAction *act) { } bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { - bool changed=false; + bool changed = false; /* 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)); + const ModelAction *write = read->get_reads_from(); + 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); - if (tid==read->get_tid()) + for (int i = 0; i <= maxthreads; i++) { + thread_id_t tid = int_to_id(i); + if (tid == read->get_tid()) continue; - if (tid==write->get_tid()) + if (tid == write->get_tid()) continue; - action_list_t * list=model->get_actions_on_obj(read->get_location(), tid); - if (list==NULL) + action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid); + if (list == NULL) continue; for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *write2 = *rit; if (!write2->is_write()) continue; - ClockVector *write2cv = cvmap->get(write2); + ClockVector *write2cv = cvmap.get(write2); if (write2cv == NULL) continue; @@ -183,7 +358,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 @@ -191,7 +366,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; } } @@ -199,42 +374,40 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { return changed; } - void SCAnalysis::computeCV(action_list_t *list) { - bool changed=true; - bool firsttime=true; - ModelAction **last_act=(ModelAction **)model_calloc(1,(maxthreads+1)*sizeof(ModelAction *)); - while(changed) { - changed=changed&firsttime; - firsttime=false; + bool changed = true; + bool firsttime = true; + ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *)); + while (changed) { + changed = changed&firsttime; + firsttime = false; for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { ModelAction *act = *it; ModelAction *lastact = last_act[id_to_int(act->get_tid())]; if (act->is_thread_start()) - lastact=model->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); - if ( cv == NULL ) { - cv = new ClockVector(lastcv, act); - cvmap->put(act, cv); - } else if ( lastcv != NULL ) { - merge(cv, act, lastcv); + lastact = execution->get_thread(act)->get_creation(); + last_act[id_to_int(act->get_tid())] = act; + ClockVector *cv = cvmap.get(act); + if (cv == NULL) { + 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 = model->get_last_action(joinedthr->get_id()); - ClockVector *finishcv = cvmap->get(finish); - changed |= (finishcv == NULL) || merge(cv, act, finishcv); + ModelAction *finish = execution->get_last_action(joinedthr->get_id()); + changed |= merge(cv, act, finish); } if (act->is_read()) { - changed|=processRead(act, cv); + changed |= processRead(act, cv); } } /* Reset the last action array */ if (changed) { - bzero(last_act, (maxthreads+1)*sizeof(ModelAction *)); + bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *)); } } model_free(last_act);