towards supporting scanalysis...

added some accessor methods in model.cc for external analyses

diff --git a/clockvector.cc b/clockvector.cc
index 14bb809dabddb051358e27776a0896ef978c62a5..0945bcf751dcd7eca5de6159affea9db49c58e3f 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -37,10 +37,10 @@ ClockVector::~ClockVector()
  * resulting vector length will be the maximum length of the two being merged.
  * @param cv is the ClockVector being merged into this vector.
  */
-void ClockVector::merge(const ClockVector *cv)
+bool ClockVector::merge(const ClockVector *cv)
 {
        ASSERT(cv != NULL);
-
+       bool changed = false;
        if (cv->num_threads > num_threads) {
                clock = (modelclock_t *)snapshot_realloc(clock, cv->num_threads * sizeof(modelclock_t));
                for (int i = num_threads; i < cv->num_threads; i++)
@@ -50,8 +50,12 @@ void ClockVector::merge(const ClockVector *cv)
 
        /* Element-wise maximum */
        for (int i = 0; i < cv->num_threads; i++)
-               if (cv->clock[i] > clock[i])
+               if (cv->clock[i] > clock[i]) {
                        clock[i] = cv->clock[i];
+                       changed = true;
+               }
+       
+       return changed;
 }
 
 /**

diff --git a/clockvector.h b/clockvector.h
index 9000a5d72eddd90ba1ba5964e4a12105a75ca9b1..e19a2113a5e10f9860669656bb1583ec91da3620 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -15,7 +15,7 @@ class ClockVector {
 public:
        ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
        ~ClockVector();
-       void merge(const ClockVector *cv);
+       bool merge(const ClockVector *cv);
        bool synchronized_since(const ModelAction *act) const;
 
        void print() const;

diff --git a/main.cc b/main.cc
index fa7075408f7d16c8bf92a00abfb13b0e0c878d5d..815a382360d5ed87763fe64e5bdf497cdeb243ae 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -68,7 +68,7 @@ params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expir
 
 static void parse_options(struct model_params *params, int argc, char **argv)
 {
-       const char *shortopts = "hymc:M:s:S:f:e:b:u:v";
+       const char *shortopts = "hycm:M:s:S:f:e:b:u:v";
        int opt;
        bool error = false;
        while (!error && (opt = getopt(argc, argv, shortopts)) != -1) {

diff --git a/model.cc b/model.cc
index 0f2f0366ebf136f448965c2d5449e317b199ca30..23efa8f77566d10752f5d4f7e8c6c70f73aff55d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -151,6 +151,18 @@ static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, Sn
        return tmp;
 }
 
+action_list_t * ModelChecker::get_actions_on_obj(void * obj, thread_id_t tid) {
+       SnapVector<action_list_t> *wrv=obj_thrd_map->get(obj);
+       if (wrv==NULL)
+               return NULL;
+       unsigned int thread=id_to_int(tid);
+       if (thread < wrv->size())
+               return &(*wrv)[thread];
+       else
+               return NULL;
+}
+
+
 /**
  * Restores user program to initial state and resets all model-checker data
  * structures.

diff --git a/model.h b/model.h
index 864f6aeedcc8072c96d19b6071f95169f02be134..78e486078b4de4a805b956992ad6ab3028248263 100644 (file)
--- a/model.h
+++ b/model.h
@@ -29,7 +29,6 @@ struct model_snapshot_members;
 
 /** @brief Shorthand for a list of release sequence heads */
 typedef ModelVector<const ModelAction *> rel_heads_list_t;
-
 typedef SnapList<ModelAction *> action_list_t;
 
 /**
@@ -143,6 +142,8 @@ public:
                trace_analyses->push_back(a);
        }
 
+       action_list_t * get_actions_on_obj(void * obj, thread_id_t tid);
+
        MEMALLOC
 private:
        /** The scheduler to use: tracks the running/ready Threads */

diff --git a/scanalysis.cc b/scanalysis.cc
index 701c50b2f1913ec694e72199658170e2b88e6c2f..8556831c2b091920303ef90372b0c179a587a860 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -1,10 +1,103 @@
 #include "scanalysis.h"
-#include "model.h"
+#include "action.h"
+#include "threads-model.h"
+#include "clockvector.h"
 
 SCAnalysis::SCAnalysis() {
+       cvmap=new HashTable<const ModelAction *, ClockVector *, uintptr_t, 4>();
+}
+
+SCAnalysis::~SCAnalysis() {
+       delete(cvmap);
 }
 
 void SCAnalysis::analyze(action_list_t * actions) {
-       
+       buildVectors(actions);
+       computeCV(actions);
+}
+
+void SCAnalysis::buildVectors(action_list_t *list) {
+       maxthreads=0;
+       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)
+                       maxthreads=threadid;
+       }
+}
+
+bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
+       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 || cv->merge(writecv) && (*read < *write));
+
+       for(int i=0;i<=maxthreads;i++) {
+               thread_id_t tid=int_to_id(i);
+               if (tid==read->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;
+                       ClockVector *write2cv = cvmap->get(write2);
+                       if (write2cv == NULL)
+                               continue;
+                       
+                       /* write -sc-> write2 &&
+                                write -rf-> R =>
+                                R -sc-> write2 */
+                       if (write2cv->synchronized_since(write)) {
+                               changed |= write2cv->merge(cv);
+                       }
+               
+                       //looking for earliest write2 in iteration to satisfy this
+                       /* write2 -sc-> R &&
+                                write -rf-> R =>
+                                write2 -sc-> write */
+                       if (cv->synchronized_since(write2)) {
+                               changed |= writecv == NULL || writecv->merge(write2cv);
+                               break;
+                       }
+               }
+       }
+       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;
 
+               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 ) {
+                                       cv->merge(lastcv);
+                       }
+                       if (act->is_read()) {
+                               changed|=processRead(act, cv);
+                       }
+               }
+               /* Reset the last action array */
+               if (changed) {
+                       bzero(last_act, (maxthreads+1)*sizeof(ModelAction *));
+               }
+       }
+       model_free(last_act);
 }

diff --git a/scanalysis.h b/scanalysis.h
index 0ef12ba407ffa4a80e8b0d82723a2ab872094d05..a6420955be068d8077e03c8900c0663a5218a0e9 100644 (file)
--- a/scanalysis.h
+++ b/scanalysis.h
@@ -1,11 +1,20 @@
 #ifndef SCANALYSIS_H
 #define SCANALYSIS_H
 #include "traceanalysis.h"
+#include "hashtable.h"
 
 class SCAnalysis : public Trace_Analysis {
  public:
        SCAnalysis();
+       ~SCAnalysis();
        virtual void analyze(action_list_t *);
 
+       SNAPSHOTALLOC
+ private:
+       void buildVectors(action_list_t *);
+       void computeCV(action_list_t *);
+       bool processRead(ModelAction *read, ClockVector *cv);
+       int maxthreads;
+       HashTable<const ModelAction *,ClockVector *, uintptr_t, 4 > * cvmap;
 };
 #endif

diff --git a/traceanalysis.h b/traceanalysis.h
index 46856d2fca44761cbffc05b2a7eec2ed85dd2951..a0b1b5cf920d77747b99227c5d076766c3601c7b 100644 (file)
--- a/traceanalysis.h
+++ b/traceanalysis.h
@@ -5,5 +5,6 @@
 class Trace_Analysis {
  public:
        virtual void analyze(action_list_t *) = 0;
+       SNAPSHOTALLOC
 };
 #endif