scanalysis: don't rely on greedy search

Fix infrastructure to use search in cases where a greedy search is not
sufficient.

diff --git a/scanalysis.cc b/scanalysis.cc
index d4102fe8b6a20148ff30ae5a83cdaf506f2753df..e6cbddc71e4f01f70f176e7c63ad5917c25888b2 100644 (file)
--- 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()<act->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;i<count;i++) {
+               if (!array[i]->is_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;a<count;a++) {
+               ModelAction *act=array[a];
+               for (int i = 0; i <= maxthreads && act != NULL; i++) {
+                       thread_id_t tid = int_to_id(i);
+                       if (tid == act->get_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)<numActions)
+                                       lastchoice=currchoice;
+                               currchoice++;
+                       } else {
+                               act = array[0];
+                               choices[currchoice]=0;
+                               if (numActions>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 047793045e63c954b03b775fd433738aaf8d08d7..3b9fed3547dc74b8cf7d27c80eb25fbc423c87c3 100644 (file)
--- 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<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;