From b756884bdc8b22457243b76982cf10dc4598f927 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 26 Apr 2013 16:50:30 -0700 Subject: [PATCH] scanalysis: don't rely on greedy search Fix infrastructure to use search in cases where a greedy search is not sufficient. --- scanalysis.cc | 205 +++++++++++++++++++++++++++++++++++++------------- scanalysis.h | 7 +- 2 files changed, 156 insertions(+), 56 deletions(-) diff --git a/scanalysis.cc b/scanalysis.cc index d4102fe..e6cbddc 100644 --- a/scanalysis.cc +++ b/scanalysis.cc @@ -40,8 +40,6 @@ 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); @@ -72,94 +70,180 @@ bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelActio return cv->merge(cv2); } -ModelAction * SCAnalysis::getNextAction() { - ModelAction *act = NULL; - /* Find the earliest in SC ordering */ - for (int i = 0; i <= maxthreads; i++) { - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) +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 *first = threadlist->front(); - if (act==NULL) { - act = first; + 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; + } + } + if (act != NULL) { + array[count++]=act; + } + } + 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; + } } - ClockVector *cv = cvmap.get(act); - if (cv->synchronized_since(first)) { - act = first; + if (act != NULL) { + array[count++]=act; } } - if (act == NULL) - return act; - /* Find the model action with the earliest sequence number in case of a cycle. - */ + ASSERT(count==0 || cyclic); - for (int i = 0; i <= maxthreads; i++) { - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - ClockVector *cvfirst = cvmap.get(first); - if (first->get_seq_number()get_seq_number()) { - bool candidate=true; - for (int j = 0; j <= maxthreads; j++) { - action_list_t *threadlist2 = &threadlists[j]; - if (threadlist2->empty()) + 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; - ModelAction *check = threadlist2->front(); - if ((check!=first) && - cvfirst->synchronized_since(check)) { - candidate=false; + 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 (candidate) - act=first; } - } - - /* See if hb demands an earlier action. */ - for (int i = 0; i <= maxthreads; i++) { - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - ClockVector *cv = act->get_cv(); - if (cv->synchronized_since(first)) { - act = first; + 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(); //add ordering constraints from this choice if (updateConstraints(act)) { //propagate changes if we have them - bool oc=cyclic; + bool prevc=cyclic; computeCV(list); - if (!oc && cyclic) - model_print("XXXXXXXXXXXXXX\n"); + 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); @@ -167,6 +251,21 @@ void SCAnalysis::buildVectors(action_list_t *list) { } 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) { diff --git a/scanalysis.h b/scanalysis.h index 0477930..3b9fed3 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -12,15 +12,16 @@ class SCAnalysis : public TraceAnalysis { SNAPSHOTALLOC private: void print_list(action_list_t *list); - void buildVectors(action_list_t *); + int buildVectors(action_list_t *); bool updateConstraints(ModelAction *act); void computeCV(action_list_t *); action_list_t * generateSC(action_list_t *); bool processRead(ModelAction *read, ClockVector *cv); - ModelAction * getNextAction(); + int getNextActions(ModelAction **array); bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2); void check_rf(action_list_t *list); - + void reset(action_list_t *list); + ModelAction* pruneArray(ModelAction**, int); int maxthreads; HashTable cvmap; -- 2.34.1