more implementation of scanalysis...

[model-checker.git] / scanalysis.cc

diff --git a/scanalysis.cc b/scanalysis.cc
index 8556831c2b091920303ef90372b0c179a587a860..6391e58aac3f7fd0a44685fc305b9abd2c4a700b 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -5,15 +5,75 @@
 
 SCAnalysis::SCAnalysis() {
        cvmap=new HashTable<const ModelAction *, ClockVector *, uintptr_t, 4>();
+       threadlists=new SnapVector<action_list_t>(1);
 }
 
 SCAnalysis::~SCAnalysis() {
-       delete(cvmap);
+       delete cvmap;
+       delete threadlists;
+}
+
+void SCAnalysis::print_list(action_list_t *list) {
+       action_list_t::iterator it;
+
+       model_print("---------------------------------------------------------------------\n");
+
+       unsigned int hash = 0;
+
+       for (it = list->begin(); it != list->end(); it++) {
+               const ModelAction *act = *it;
+               if (act->get_seq_number() > 0)
+                       act->print();
+               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);
+}
+
+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;
+                       continue;
+               }
+               ClockVector *cv=cvmap->get(act);
+               if (cv->synchronized_since(first)) {
+                       act=first;
+               }
+       }
+       return act;
+}
+
+action_list_t * SCAnalysis::generateSC(action_list_t *list) {  
+       action_list_t *sclist=new action_list_t();
+       while (true) {
+               ModelAction * act=getNextAction();
+               if (act==NULL)
+                       break;
+               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
+                       computeCV(list);
+               }
+               //add action to end
+               sclist->push_back(act);
+       }
+       return sclist;
 }
 
 void SCAnalysis::buildVectors(action_list_t *list) {
@@ -21,9 +81,39 @@ void SCAnalysis::buildVectors(action_list_t *list) {
        for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
                ModelAction *act = *it;
                int threadid=id_to_int(act->get_tid());
-               if (threadid > maxthreads)
+               if (threadid > maxthreads) {
+                       threadlists->resize(threadid+1);
                        maxthreads=threadid;
+               }
+               (*threadlists)[threadid].push_back(act);
+       }
+}
+
+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)];
+               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
+                               writecv->merge(actcv);
+                               changed=true;
+                               break;
+                       }
+               }               
        }
+       return changed;
 }
 
 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
@@ -38,11 +128,16 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
                thread_id_t tid=int_to_id(i);
                if (tid==read->get_tid())
                        continue;
+               if (tid==write->get_tid())
+                       continue;
                action_list_t * list=model->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);
                        if (write2cv == NULL)
                                continue;
@@ -90,6 +185,12 @@ void SCAnalysis::computeCV(action_list_t *list) {
                        } else if ( lastcv != NULL ) {
                                        cv->merge(lastcv);
                        }
+                       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) || cv->merge(finishcv);
+                       }
                        if (act->is_read()) {
                                changed|=processRead(act, cv);
                        }