From 38cb7400c16ad0a04355ec77af2bf5da2dbfaad5 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 12 Apr 2013 01:33:34 -0700 Subject: [PATCH] more implementation of scanalysis... seems like it might work at this point, but need code to tell whether it is a SC trace or not and which parts are SC --- model.h | 2 +- scanalysis.cc | 105 +++++++++++++++++++++++++++++++++++++++++++++++++- scanalysis.h | 5 +++ 3 files changed, 109 insertions(+), 3 deletions(-) diff --git a/model.h b/model.h index 78e4860..b5c7c30 100644 --- a/model.h +++ b/model.h @@ -143,6 +143,7 @@ public: } action_list_t * get_actions_on_obj(void * obj, thread_id_t tid); + ModelAction * get_last_action(thread_id_t tid) const; MEMALLOC private: @@ -203,7 +204,6 @@ private: void check_curr_backtracking(ModelAction *curr); void add_action_to_lists(ModelAction *act); - ModelAction * get_last_action(thread_id_t tid) const; ModelAction * get_last_fence_release(thread_id_t tid) const; ModelAction * get_last_seq_cst_write(ModelAction *curr) const; ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const; diff --git a/scanalysis.cc b/scanalysis.cc index 8556831..6391e58 100644 --- a/scanalysis.cc +++ b/scanalysis.cc @@ -5,15 +5,75 @@ SCAnalysis::SCAnalysis() { cvmap=new HashTable(); + threadlists=new SnapVector(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); } diff --git a/scanalysis.h b/scanalysis.h index a642095..79f78f1 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -11,10 +11,15 @@ class SCAnalysis : public Trace_Analysis { SNAPSHOTALLOC private: + void print_list(action_list_t *list); void 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 maxthreads; HashTable * cvmap; + SnapVector * threadlists; }; #endif -- 2.34.1