From: Brian Norris Date: Tue, 23 Apr 2013 01:43:20 +0000 (-0700) Subject: Merge remote-tracking branch 'private/master' X-Git-Tag: oopsla2013~25 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=473bdc841f3b03b722911a5fa0b4f21ba3a217ed;hp=732f2a6b8c2083eb47fadcdf1eae0f9a837be32f;p=model-checker.git Merge remote-tracking branch 'private/master' --- diff --git a/scanalysis.cc b/scanalysis.cc index abed220..8aa400c 100644 --- a/scanalysis.cc +++ b/scanalysis.cc @@ -6,7 +6,9 @@ SCAnalysis::SCAnalysis(const ModelExecution *execution) : cvmap(), - cycleset(), + cyclic(false), + badrfset(), + lastwrmap(), threadlists(1), execution(execution) { @@ -16,18 +18,20 @@ SCAnalysis::~SCAnalysis() { } void SCAnalysis::print_list(action_list_t *list) { - action_list_t::iterator it; - model_print("---------------------------------------------------------------------\n"); - + if (cyclic) + model_print("Not SC\n"); unsigned int hash = 0; - for (it = list->begin(); it != list->end(); it++) { + for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { const ModelAction *act = *it; if (act->get_seq_number() > 0) { - if (cycleset.contains(act)) - model_print("CYC"); + if (badrfset.contains(act)) + model_print("BRF "); act->print(); + if (badrfset.contains(act)) { + model_print("Desired Rf: %u \n",badrfset.get(act)->get_seq_number()); + } } hash = hash ^ (hash << 3) ^ ((*it)->hash()); } @@ -39,13 +43,32 @@ void SCAnalysis::analyze(action_list_t *actions) { buildVectors(actions); computeCV(actions); action_list_t *list = generateSC(actions); + check_rf(list); print_list(list); } -bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2) { +void SCAnalysis::check_rf(action_list_t *list) { + for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { + const ModelAction *act = *it; + if (act->is_read()) { + if (act->get_reads_from()!=lastwrmap.get(act->get_location())) + badrfset.put(act,lastwrmap.get(act->get_location())); + } + if (act->is_write()) + lastwrmap.put(act->get_location(), act); + } +} + +bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) { + ClockVector * cv2=cvmap.get(act2); + if (cv2==NULL) + return true; if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) { - cycleset.put(act, act); + cyclic=true; + //refuse to introduce cycles into clock vectors + return false; } + return cv->merge(cv2); } @@ -58,7 +81,7 @@ ModelAction * SCAnalysis::getNextAction() { continue; ModelAction *first = threadlist->front(); if (act==NULL) { - act=first; + act = first; continue; } ClockVector *cv = cvmap.get(act); @@ -69,7 +92,6 @@ ModelAction * SCAnalysis::getNextAction() { if (act == NULL) return act; - /* Find the model action with the earliest sequence number in case of a cycle. */ @@ -78,11 +100,22 @@ ModelAction * SCAnalysis::getNextAction() { if (threadlist->empty()) continue; ModelAction *first = threadlist->front(); - ClockVector *cv = cvmap.get(act); ClockVector *cvfirst = cvmap.get(first); - if (first->get_seq_number()get_seq_number()&& - (cv->synchronized_since(first)||!cvfirst->synchronized_since(act))) { - act=first; + if (first->get_seq_number()get_seq_number()) { + bool candidate=true; + for (int j = 0; j <= maxthreads; j++) { + action_list_t *threadlist2 = &threadlists[j]; + if (threadlist2->empty()) + continue; + ModelAction *check = threadlist2->front(); + if ((check!=first) && + cvfirst->synchronized_since(check)) { + candidate=false; + break; + } + } + if (candidate) + act=first; } } @@ -135,7 +168,6 @@ void SCAnalysis::buildVectors(action_list_t *list) { 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()) @@ -151,7 +183,7 @@ bool SCAnalysis::updateConstraints(ModelAction *act) { break; if (write->get_location() == act->get_location()) { //write is sc after act - merge(writecv, write, actcv); + merge(writecv, write, act); changed = true; break; } @@ -166,7 +198,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { /* Merge in the clock vector from the write */ const ModelAction *write = read->get_reads_from(); ClockVector *writecv = cvmap.get(write); - changed |= writecv == NULL || (merge(cv, read, writecv) && (*read < *write)); + changed |= merge(cv, read, write) && (*read < *write); for (int i = 0; i <= maxthreads; i++) { thread_id_t tid = int_to_id(i); @@ -190,7 +222,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { write -rf-> R => R -sc-> write2 */ if (write2cv->synchronized_since(write)) { - changed |= merge(write2cv, write2, cv); + changed |= merge(write2cv, write2, read); } //looking for earliest write2 in iteration to satisfy this @@ -198,7 +230,7 @@ bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) { write -rf-> R => write2 -sc-> write */ if (cv->synchronized_since(write2)) { - changed |= writecv == NULL || merge(writecv, write, write2cv); + changed |= writecv==NULL || merge(writecv, write, write2); break; } } @@ -219,20 +251,19 @@ void SCAnalysis::computeCV(action_list_t *list) { ModelAction *lastact = last_act[id_to_int(act->get_tid())]; if (act->is_thread_start()) lastact = execution->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); + cv = new ClockVector(NULL, act); cvmap.put(act, cv); - } else if (lastcv != NULL) { - merge(cv, act, lastcv); + } + if (lastact != NULL) { + merge(cv, act, lastact); } if (act->is_thread_join()) { Thread *joinedthr = act->get_thread_operand(); ModelAction *finish = execution->get_last_action(joinedthr->get_id()); - ClockVector *finishcv = cvmap.get(finish); - changed |= (finishcv == NULL) || merge(cv, act, finishcv); + changed |= merge(cv, act, finish); } if (act->is_read()) { changed |= processRead(act, cv); diff --git a/scanalysis.h b/scanalysis.h index e8afc18..0477930 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -18,11 +18,15 @@ class SCAnalysis : public TraceAnalysis { action_list_t * generateSC(action_list_t *); bool processRead(ModelAction *read, ClockVector *cv); ModelAction * getNextAction(); - bool merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2); + bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2); + void check_rf(action_list_t *list); + int maxthreads; HashTable cvmap; - HashTable cycleset; + bool cyclic; + HashTable badrfset; + HashTable lastwrmap; SnapVector threadlists; const ModelExecution *execution; };