From 9508fe09d2eeaaf7fbe7193d9cb81b3bc66316b5 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Thu, 11 Apr 2013 03:01:07 -0700 Subject: [PATCH] towards supporting scanalysis... added some accessor methods in model.cc for external analyses --- clockvector.cc | 10 +++-- clockvector.h | 2 +- main.cc | 2 +- model.cc | 12 ++++++ model.h | 3 +- scanalysis.cc | 97 ++++++++++++++++++++++++++++++++++++++++++++++++- scanalysis.h | 9 +++++ traceanalysis.h | 1 + 8 files changed, 128 insertions(+), 8 deletions(-) diff --git a/clockvector.cc b/clockvector.cc index 14bb809d..0945bcf7 100644 --- 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 9000a5d7..e19a2113 100644 --- 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 fa707540..815a3823 100644 --- 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 0f2f0366..23efa8f7 100644 --- a/model.cc +++ b/model.cc @@ -151,6 +151,18 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *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 864f6aee..78e48607 100644 --- 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 rel_heads_list_t; - typedef SnapList 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 701c50b2..8556831c 100644 --- 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(); +} + +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 0ef12ba4..a6420955 100644 --- 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 * cvmap; }; #endif diff --git a/traceanalysis.h b/traceanalysis.h index 46856d2f..a0b1b5cf 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -5,5 +5,6 @@ class Trace_Analysis { public: virtual void analyze(action_list_t *) = 0; + SNAPSHOTALLOC }; #endif -- 2.34.1