From b924665809bc0e9a08fbc765fb4d8999fcaac1f7 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 16 Oct 2018 14:51:59 -0700 Subject: [PATCH] Remove SC Analysis --- Makefile | 11 +- main.cc | 1 - plugins.cc | 4 - scanalysis.cc | 458 -------------- scanalysis.h | 52 -- scfence/Makefile | 11 - scfence/fence_common.h | 35 -- scfence/inference.cc | 378 ------------ scfence/inference.h | 154 ----- scfence/inferlist.cc | 207 ------- scfence/inferlist.h | 64 -- scfence/inferset.cc | 300 --------- scfence/inferset.h | 147 ----- scfence/patch.cc | 69 --- scfence/patch.h | 59 -- scfence/sc_annotation.h | 47 -- scfence/scfence.cc | 1298 --------------------------------------- scfence/scfence.h | 412 ------------- scfence/scgen.cc | 672 -------------------- scfence/scgen.h | 119 ---- 20 files changed, 3 insertions(+), 4495 deletions(-) delete mode 100644 scanalysis.cc delete mode 100644 scanalysis.h delete mode 100644 scfence/Makefile delete mode 100644 scfence/fence_common.h delete mode 100644 scfence/inference.cc delete mode 100644 scfence/inference.h delete mode 100644 scfence/inferlist.cc delete mode 100644 scfence/inferlist.h delete mode 100644 scfence/inferset.cc delete mode 100644 scfence/inferset.h delete mode 100644 scfence/patch.cc delete mode 100644 scfence/patch.h delete mode 100644 scfence/sc_annotation.h delete mode 100644 scfence/scfence.cc delete mode 100644 scfence/scfence.h delete mode 100644 scfence/scgen.cc delete mode 100644 scfence/scgen.h diff --git a/Makefile b/Makefile index eb84076d..fe1bf0d1 100644 --- a/Makefile +++ b/Makefile @@ -1,14 +1,12 @@ include common.mk -SCFENCE_DIR := scfence - OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ datarace.o impatomic.o cmodelint.o \ snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \ - context.o scanalysis.o execution.o plugins.o libannotate.o + context.o execution.o plugins.o libannotate.o -CPPFLAGS += -Iinclude -I. -I$(SCFENCE_DIR) +CPPFLAGS += -Iinclude -I. LDFLAGS := -ldl -lrt -rdynamic SHARED := -shared @@ -41,9 +39,6 @@ malloc.o: malloc.c %.o : %.cc $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS) -include $(SCFENCE_DIR)/Makefile - --include $(wildcard $(SCFENCE_DIR)/.*.d) $(LIB_SO): $(OBJECTS) $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) @@ -55,7 +50,7 @@ $(LIB_SO): $(OBJECTS) PHONY += clean clean: - rm -f *.o *.so .*.d *.pdf *.dot $(SCFENCE_DIR)/.*.d $(SCFENCE_DIR)/*.o + rm -f *.o *.so .*.d *.pdf *.dot $(MAKE) -C $(TESTS_DIR) clean PHONY += mrclean diff --git a/main.cc b/main.cc index 502f499e..5b764b61 100644 --- a/main.cc +++ b/main.cc @@ -15,7 +15,6 @@ #include "model.h" #include "params.h" #include "snapshot-interface.h" -#include "scanalysis.h" #include "plugins.h" static void param_defaults(struct model_params *params) diff --git a/plugins.cc b/plugins.cc index 38493deb..c98cb5dd 100644 --- a/plugins.cc +++ b/plugins.cc @@ -1,6 +1,4 @@ #include "plugins.h" -#include "scanalysis.h" -#include "scfence.h" ModelVector * registered_analysis; ModelVector * installed_analysis; @@ -8,8 +6,6 @@ ModelVector * installed_analysis; void register_plugins() { registered_analysis=new ModelVector(); installed_analysis=new ModelVector(); - registered_analysis->push_back(new SCAnalysis()); - registered_analysis->push_back(new SCFence()); } ModelVector * getRegisteredTraceAnalysis() { diff --git a/scanalysis.cc b/scanalysis.cc deleted file mode 100644 index 6fc1e081..00000000 --- a/scanalysis.cc +++ /dev/null @@ -1,458 +0,0 @@ -#include "scanalysis.h" -#include "action.h" -#include "threads-model.h" -#include "clockvector.h" -#include "execution.h" -#include - - -SCAnalysis::SCAnalysis() : - cvmap(), - cyclic(false), - badrfset(), - lastwrmap(), - threadlists(1), - execution(NULL), - print_always(false), - print_buggy(true), - print_nonsc(false), - time(false), - stats((struct sc_statistics *)model_calloc(1, sizeof(struct sc_statistics))) -{ -} - -SCAnalysis::~SCAnalysis() { - delete(stats); -} - -void SCAnalysis::setExecution(ModelExecution * execution) { - this->execution=execution; -} - -const char * SCAnalysis::name() { - const char * name = "SC"; - return name; -} - -void SCAnalysis::finish() { - if (time) - model_print("Elapsed time in usec %llu\n", stats->elapsedtime); - model_print("SC count: %u\n", stats->sccount); - model_print("Non-SC count: %u\n", stats->nonsccount); - model_print("Total actions: %llu\n", stats->actions); - unsigned long long actionperexec=(stats->actions)/(stats->sccount+stats->nonsccount); - model_print("Actions per execution: %llu\n", actionperexec); -} - -bool SCAnalysis::option(char * opt) { - if (strcmp(opt, "verbose")==0) { - print_always=true; - return false; - } else if (strcmp(opt, "buggy")==0) { - return false; - } else if (strcmp(opt, "quiet")==0) { - print_buggy=false; - return false; - } else if (strcmp(opt, "nonsc")==0) { - print_nonsc=true; - return false; - } else if (strcmp(opt, "time")==0) { - time=true; - return false; - } else if (strcmp(opt, "help") != 0) { - model_print("Unrecognized option: %s\n", opt); - } - - model_print("SC Analysis options\n"); - model_print("verbose -- print all feasible executions\n"); - model_print("buggy -- print only buggy executions (default)\n"); - model_print("nonsc -- print non-sc execution\n"); - model_print("quiet -- print nothing\n"); - model_print("time -- time execution of scanalysis\n"); - model_print("\n"); - - return true; -} - -void SCAnalysis::print_list(action_list_t *list) { - model_print("---------------------------------------------------------------------\n"); - if (cyclic) - model_print("Not SC\n"); - unsigned int hash = 0; - - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - const ModelAction *act = *it; - if (act->get_seq_number() > 0) { - 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()); - } - model_print("HASH %u\n", hash); - model_print("---------------------------------------------------------------------\n"); -} - -void SCAnalysis::analyze(action_list_t *actions) { - - struct timeval start; - struct timeval finish; - if (time) - gettimeofday(&start, NULL); - action_list_t *list = generateSC(actions); - check_rf(list); - if (print_always || (print_buggy && execution->have_bug_reports())|| (print_nonsc && cyclic)) - print_list(list); - if (time) { - gettimeofday(&finish, NULL); - stats->elapsedtime+=((finish.tv_sec*1000000+finish.tv_usec)-(start.tv_sec*1000000+start.tv_usec)); - } - update_stats(); -} - -void SCAnalysis::update_stats() { - if (cyclic) { - stats->nonsccount++; - } else { - stats->sccount++; - } -} - -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) { - cyclic = true; - //refuse to introduce cycles into clock vectors - return false; - } - - return cv->merge(cv2); -} - -int SCAnalysis::getNextActions(ModelAction ** array) { - int count=0; - - for (int t = 0; t <= maxthreads; t++) { - action_list_t *tlt = &threadlists[t]; - if (tlt->empty()) - continue; - ModelAction *act = tlt->front(); - ClockVector *cv = cvmap.get(act); - - /* Find the earliest in SC ordering */ - for (int i = 0; i <= maxthreads; i++) { - if ( i == t ) - continue; - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - if (cv->synchronized_since(first)) { - act = NULL; - break; - } - } - if (act != NULL) { - array[count++]=act; - } - } - if (count != 0) - return count; - for (int t = 0; t <= maxthreads; t++) { - action_list_t *tlt = &threadlists[t]; - if (tlt->empty()) - continue; - ModelAction *act = tlt->front(); - ClockVector *cv = act->get_cv(); - - /* Find the earliest in SC ordering */ - for (int i = 0; i <= maxthreads; i++) { - if ( i == t ) - continue; - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - if (cv->synchronized_since(first)) { - act = NULL; - break; - } - } - if (act != NULL) { - array[count++]=act; - } - } - - ASSERT(count==0 || cyclic); - - return count; -} - -ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) { - /* No choice */ - if (count == 1) - return array[0]; - - /* Choose first non-write action */ - ModelAction *nonwrite=NULL; - for(int i=0;iis_write()) - if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number()) - nonwrite = array[i]; - } - if (nonwrite != NULL) - return nonwrite; - - /* Look for non-conflicting action */ - ModelAction *nonconflict=NULL; - for(int a=0;aget_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 - act = NULL; - break; - } - } - } - if (act != NULL) { - if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number()) - nonconflict=act; - } - } - return nonconflict; -} - -action_list_t * SCAnalysis::generateSC(action_list_t *list) { - int numactions=buildVectors(list); - stats->actions+=numactions; - - computeCV(list); - - action_list_t *sclist = new action_list_t(); - ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *)); - int * choices = (int *) model_calloc(1, sizeof(int)*numactions); - int endchoice = 0; - int currchoice = 0; - int lastchoice = -1; - while (true) { - int numActions = getNextActions(array); - if (numActions == 0) - break; - ModelAction * act=pruneArray(array, numActions); - if (act == NULL) { - if (currchoice < endchoice) { - act = array[choices[currchoice]]; - //check whether there is still another option - if ((choices[currchoice]+1)1) - lastchoice=currchoice; - currchoice++; - } - } - 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 - bool prevc=cyclic; - computeCV(list); - if (!prevc && cyclic) { - model_print("ROLLBACK in SC\n"); - //check whether we have another choice - if (lastchoice != -1) { - //have to reset everything - choices[lastchoice]++; - endchoice=lastchoice+1; - currchoice=0; - lastchoice=-1; - reset(list); - buildVectors(list); - computeCV(list); - sclist->clear(); - continue; - } - } - } - //add action to end - sclist->push_back(act); - } - model_free(array); - return sclist; -} - -int SCAnalysis::buildVectors(action_list_t *list) { - maxthreads = 0; - int numactions = 0; - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - ModelAction *act = *it; - numactions++; - int threadid = id_to_int(act->get_tid()); - if (threadid > maxthreads) { - threadlists.resize(threadid + 1); - maxthreads = threadid; - } - threadlists[threadid].push_back(act); - } - return numactions; -} - -void SCAnalysis::reset(action_list_t *list) { - for (int t = 0; t <= maxthreads; t++) { - action_list_t *tlt = &threadlists[t]; - tlt->clear(); - } - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - ModelAction *act = *it; - delete cvmap.get(act); - cvmap.put(act, NULL); - } - - cyclic=false; -} - -bool SCAnalysis::updateConstraints(ModelAction *act) { - bool changed = false; - 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 - merge(writecv, write, act); - changed = true; - break; - } - } - } - return changed; -} - -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 |= merge(cv, read, write) && (*read < *write); - - for (int i = 0; i <= maxthreads; i++) { - thread_id_t tid = int_to_id(i); - if (tid == read->get_tid()) - continue; - if (tid == write->get_tid()) - continue; - action_list_t *list = execution->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; - - /* write -sc-> write2 && - write -rf-> R => - R -sc-> write2 */ - if (write2cv->synchronized_since(write)) { - changed |= merge(write2cv, write2, read); - } - - //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 || merge(writecv, write, write2); - 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 = execution->get_thread(act)->get_creation(); - last_act[id_to_int(act->get_tid())] = act; - ClockVector *cv = cvmap.get(act); - if (cv == NULL) { - cv = new ClockVector(NULL, act); - cvmap.put(act, cv); - } - 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()); - changed |= merge(cv, act, finish); - } - 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 deleted file mode 100644 index 23d127bf..00000000 --- a/scanalysis.h +++ /dev/null @@ -1,52 +0,0 @@ -#ifndef SCANALYSIS_H -#define SCANALYSIS_H -#include "traceanalysis.h" -#include "hashtable.h" - -struct sc_statistics { - unsigned long long elapsedtime; - unsigned int sccount; - unsigned int nonsccount; - unsigned long long actions; -}; - -class SCAnalysis : public TraceAnalysis { - public: - SCAnalysis(); - ~SCAnalysis(); - virtual void setExecution(ModelExecution * execution); - virtual void analyze(action_list_t *); - virtual const char * name(); - virtual bool option(char *); - virtual void finish(); - - - SNAPSHOTALLOC - private: - void update_stats(); - void print_list(action_list_t *list); - int 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); - int getNextActions(ModelAction **array); - bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2); - void check_rf(action_list_t *list); - void reset(action_list_t *list); - ModelAction* pruneArray(ModelAction**, int); - - int maxthreads; - HashTable cvmap; - bool cyclic; - HashTable badrfset; - HashTable lastwrmap; - SnapVector threadlists; - ModelExecution *execution; - bool print_always; - bool print_buggy; - bool print_nonsc; - bool time; - struct sc_statistics *stats; -}; -#endif diff --git a/scfence/Makefile b/scfence/Makefile deleted file mode 100644 index d0cc3136..00000000 --- a/scfence/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -FENCE_OBJS := $(SCFENCE_DIR)/scgen.o \ - $(SCFENCE_DIR)/inference.o \ - $(SCFENCE_DIR)/inferset.o \ - $(SCFENCE_DIR)/inferlist.o \ - $(SCFENCE_DIR)/patch.o \ - $(SCFENCE_DIR)/scfence.o - -$(FENCE_OBJS): $(SCFENCE_DIR)/%.o : $(SCFENCE_DIR)/%.cc $(SCFENCE_DIR)/%.h - $(CXX) -MMD -MF $(SCFENCE_DIR)/.$(notdir $@).d -fPIC -c $< $(CPPFLAGS) -o $@ - -OBJECTS += $(FENCE_OBJS) diff --git a/scfence/fence_common.h b/scfence/fence_common.h deleted file mode 100644 index 014cce11..00000000 --- a/scfence/fence_common.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef _FENCE_COMMON_ -#define _FENCE_COMMON_ - -#include "model.h" -#include "action.h" - -#define DEFAULT_REPETITIVE_READ_BOUND 20 - -#define FENCE_OUTPUT - -#ifdef FENCE_OUTPUT - -#define FENCE_PRINT model_print - -#define ACT_PRINT(x) (x)->print() - -#define CV_PRINT(x) (x)->print() - -#define WILDCARD_ACT_PRINT(x)\ - FENCE_PRINT("Wildcard: %d\n", get_wildcard_id_zero((x)->get_original_mo()));\ - ACT_PRINT(x); - -#else - -#define FENCE_PRINT - -#define ACT_PRINT(x) - -#define CV_PRINT(x) - -#define WILDCARD_ACT_PRINT(x) - -#endif - -#endif diff --git a/scfence/inference.cc b/scfence/inference.cc deleted file mode 100644 index e2d21527..00000000 --- a/scfence/inference.cc +++ /dev/null @@ -1,378 +0,0 @@ -#include "fence_common.h" -#include "wildcard.h" -#include "patch.h" -#include "inferlist.h" -#include "inference.h" - -/** Forward declaration */ -class PatchUnit; -class Patch; -class Inference; -class InferenceList; - -bool isTheInference(Inference *infer) { - for (int i = 0; i < infer->getSize(); i++) { - memory_order mo1 = (*infer)[i], mo2; - if (mo1 == WILDCARD_NONEXIST) - mo1 = relaxed; - switch (i) { - case 3: - mo2 = acquire; - break; - case 11: - mo2 = release; - break; - default: - mo2 = relaxed; - break; - } - if (mo1 != mo2) - return false; - } - return true; -} - -const char* get_mo_str(memory_order order) { - switch (order) { - case std::memory_order_relaxed: return "relaxed"; - case std::memory_order_acquire: return "acquire"; - case std::memory_order_release: return "release"; - case std::memory_order_acq_rel: return "acq_rel"; - case std::memory_order_seq_cst: return "seq_cst"; - default: - //model_print("Weird memory order, a bug or something!\n"); - //model_print("memory_order: %d\n", order); - return "unknown"; - } -} - - -void Inference::resize(int newsize) { - ASSERT (newsize > size && newsize <= MAX_WILDCARD_NUM); - memory_order *newOrders = (memory_order *) model_malloc((newsize + 1) * sizeof(memory_order*)); - int i; - for (i = 0; i <= size; i++) - newOrders[i] = orders[i]; - for (; i <= newsize; i++) - newOrders[i] = WILDCARD_NONEXIST; - model_free(orders); - size = newsize; - orders = newOrders; -} - -/** Return the state of how we update a specific mo; If we have to make an - * uncompatible inference or that inference cannot be imposed because it's - * not a wildcard, it returns -1; if it is a compatible memory order but the - * current memory order is no weaker than mo, it returns 0; otherwise, it - * does strengthen the order, and returns 1 */ -int Inference::strengthen(const ModelAction *act, memory_order mo) { - memory_order wildcard = act->get_original_mo(); - int wildcardID = get_wildcard_id_zero(wildcard); - if (!is_wildcard(wildcard)) { - FENCE_PRINT("We cannot make this update to %s!\n", get_mo_str(mo)); - ACT_PRINT(act); - return -1; - } - if (wildcardID > size) - resize(wildcardID); - ASSERT (is_normal_mo(mo)); - //model_print("wildcardID -> order: %d -> %d\n", wildcardID, orders[wildcardID]); - ASSERT (is_normal_mo_infer(orders[wildcardID])); - switch (orders[wildcardID]) { - case memory_order_seq_cst: - return 0; - case memory_order_relaxed: - if (mo == memory_order_relaxed) - return 0; - orders[wildcardID] = mo; - break; - case memory_order_acquire: - if (mo == memory_order_acquire || mo == memory_order_relaxed) - return 0; - if (mo == memory_order_release) - orders[wildcardID] = memory_order_acq_rel; - else if (mo >= memory_order_acq_rel && mo <= - memory_order_seq_cst) - orders[wildcardID] = mo; - break; - case memory_order_release: - if (mo == memory_order_release || mo == memory_order_relaxed) - return 0; - if (mo == memory_order_acquire) - orders[wildcardID] = memory_order_acq_rel; - else if (mo >= memory_order_acq_rel) - orders[wildcardID] = mo; - break; - case memory_order_acq_rel: - if (mo == memory_order_seq_cst) - orders[wildcardID] = mo; - else - return 0; - break; - default: - orders[wildcardID] = mo; - break; - } - return 1; -} - -Inference::Inference() { - orders = (memory_order *) model_malloc((4 + 1) * sizeof(memory_order*)); - size = 4; - for (int i = 0; i <= size; i++) - orders[i] = WILDCARD_NONEXIST; - initialInfer = this; - buggy = false; - hasFixes = false; - leaf = false; - explored = false; - shouldFix = true; -} - -Inference::Inference(Inference *infer) { - ASSERT (infer->size > 0 && infer->size <= MAX_WILDCARD_NUM); - orders = (memory_order *) model_malloc((infer->size + 1) * sizeof(memory_order*)); - this->size = infer->size; - for (int i = 0; i <= size; i++) - orders[i] = infer->orders[i]; - - initialInfer = infer->initialInfer; - buggy = false; - hasFixes = false; - leaf = false; - explored = false; - shouldFix = true; -} - -/** return value: - * 0 -> mo1 == mo2; - * 1 -> mo1 stronger than mo2; - * -1 -> mo1 weaker than mo2; - * 2 -> mo1 & mo2 are uncomparable. - */ -int Inference::compareMemoryOrder(memory_order mo1, memory_order mo2) { - if (mo1 == WILDCARD_NONEXIST) - mo1 = memory_order_relaxed; - if (mo2 == WILDCARD_NONEXIST) - mo2 = memory_order_relaxed; - if (mo1 == mo2) - return 0; - if (mo1 == memory_order_relaxed) - return -1; - if (mo1 == memory_order_acquire) { - if (mo2 == memory_order_relaxed) - return 1; - if (mo2 == memory_order_release) - return 2; - return -1; - } - if (mo1 == memory_order_release) { - if (mo2 == memory_order_relaxed) - return 1; - if (mo2 == memory_order_acquire) - return 2; - return -1; - } - if (mo1 == memory_order_acq_rel) { - if (mo2 == memory_order_seq_cst) - return -1; - else - return 1; - } - // mo1 now must be SC and mo2 can't be SC - return 1; -} - - -/** Try to calculate the set of inferences that are weaker than this, but - * still stronger than infer */ -InferenceList* Inference::getWeakerInferences(Inference *infer) { - // An array of strengthened wildcards - SnapVector *strengthened = new SnapVector; - model_print("Strengthened wildcards\n"); - for (int i = 1; i <= size; i++) { - memory_order mo1 = orders[i], - mo2 = (*infer)[i]; - int compVal = compareMemoryOrder(mo1, mo2); - if (!(compVal == 0 || compVal == 1)) { - model_print("assert failure\n"); - model_print("compVal=%d\n", compVal); - ASSERT (false); - } - if (compVal == 0) // Same - continue; - model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1), - get_mo_str(mo2)); - strengthened->push_back(i); - } - - // Got the strengthened wildcards, find out weaker inferences - // First get a volatile copy of this inference - Inference *tmpRes = new Inference(this); - InferenceList *res = new InferenceList; - if (strengthened->size() == 0) - return res; - getWeakerInferences(res, tmpRes, this, infer, strengthened, 0); - res->pop_front(); - res->pop_back(); - InferenceList::print(res, "Weakened"); - return res; -} - - -// seq_cst -> acq_rel -> acquire -> release -> relaxed -memory_order Inference::nextWeakOrder(memory_order mo1, memory_order mo2) { - memory_order res; - switch (mo1) { - case memory_order_seq_cst: - res = memory_order_acq_rel; - break; - case memory_order_acq_rel: - res = memory_order_acquire; - break; - case memory_order_acquire: - res = memory_order_relaxed; - break; - case memory_order_release: - res = memory_order_relaxed; - break; - case memory_order_relaxed: - res = memory_order_relaxed; - break; - default: - res = memory_order_relaxed; - break; - } - int compVal = compareMemoryOrder(res, mo2); - if (compVal == 2 || compVal == -1) // Incomparable - res = mo2; - return res; -} - -void Inference::getWeakerInferences(InferenceList* list, Inference *tmpRes, - Inference *infer1, Inference *infer2, SnapVector *strengthened, unsigned idx) { - if (idx == strengthened->size()) { // Ready to produce one weakened result - Inference *res = new Inference(tmpRes); - //model_print("Weakened inference:\n"); - //res->print(); - res->setShouldFix(false); - list->push_back(res); - return; - } - - int w = (*strengthened)[idx]; // The wildcard - memory_order mo1 = (*infer1)[w]; - memory_order mo2 = (*infer2)[w]; - if (mo2 == WILDCARD_NONEXIST) - mo2 = memory_order_relaxed; - memory_order weakenedMO = mo1; - do { - (*tmpRes)[w] = weakenedMO; - getWeakerInferences(list, tmpRes, infer1, infer2, - strengthened, idx + 1); - if (weakenedMO == memory_order_acq_rel) { - (*tmpRes)[w] = memory_order_release; - getWeakerInferences(list, tmpRes, infer1, infer2, - strengthened, idx + 1); - } - weakenedMO = nextWeakOrder(weakenedMO, mo2); - model_print("weakendedMO=%d\n", weakenedMO); - model_print("mo2=%d\n", mo2); - } while (weakenedMO != mo2); - (*tmpRes)[w] = weakenedMO; - getWeakerInferences(list, tmpRes, infer1, infer2, - strengthened, idx + 1); -} - -memory_order& Inference::operator[](int idx) { - if (idx > 0 && idx <= size) - return orders[idx]; - else { - resize(idx); - orders[idx] = WILDCARD_NONEXIST; - return orders[idx]; - } -} - -/** A simple overload, which allows caller to pass two boolean refrence, and - * we will set those two variables indicating whether we can update the - * order (copatible or not) and have updated the order */ -int Inference::strengthen(const ModelAction *act, memory_order mo, bool &canUpdate, bool &hasUpdated) { - int res = strengthen(act, mo); - if (res == -1) - canUpdate = false; - if (res == 1) - hasUpdated = true; - - return res; -} - -/** @Return: - 1 -> 'this> infer'; - -1 -> 'this < infer' - 0 -> 'this == infer' - INFERENCE_INCOMPARABLE(x) -> true means incomparable - */ -int Inference::compareTo(const Inference *infer) const { - int result = size == infer->size ? 0 : (size > infer->size) ? 1 : -1; - int smallerSize = size > infer->size ? infer->size : size; - int subResult; - - for (int i = 0; i <= smallerSize; i++) { - memory_order mo1 = orders[i], - mo2 = infer->orders[i]; - if ((mo1 == memory_order_acquire && mo2 == memory_order_release) || - (mo1 == memory_order_release && mo2 == memory_order_acquire)) { - // Incomparable - return -2; - } else { - if ((mo1 == WILDCARD_NONEXIST && mo2 != WILDCARD_NONEXIST) - || (mo1 == WILDCARD_NONEXIST && mo2 == memory_order_relaxed) - || (mo1 == memory_order_relaxed && mo2 == WILDCARD_NONEXIST) - ) - subResult = 1; - else if (mo1 != WILDCARD_NONEXIST && mo2 == WILDCARD_NONEXIST) - subResult = -1; - else - subResult = mo1 > mo2 ? 1 : (mo1 == mo2) ? 0 : -1; - - if ((subResult > 0 && result < 0) || (subResult < 0 && result > 0)) { - return -2; - } - if (subResult != 0) - result = subResult; - } - } - return result; -} - -unsigned long Inference::getHash() { - unsigned long hash = 0; - for (int i = 1; i <= size; i++) { - memory_order mo = orders[i]; - if (mo == WILDCARD_NONEXIST) { - mo = memory_order_relaxed; - } - hash *= 37; - hash += (mo + 4096); - } - return hash; -} - - -void Inference::print(bool hasHash) { - ASSERT(size > 0 && size <= MAX_WILDCARD_NUM); - for (int i = 1; i <= size; i++) { - memory_order mo = orders[i]; - if (mo != WILDCARD_NONEXIST) { - // Print the wildcard inference result - FENCE_PRINT("wildcard %d -> memory_order_%s\n", i, get_mo_str(mo)); - } - } - if (hasHash) - FENCE_PRINT("Hash: %lu\n", getHash()); -} - -void Inference::print() { - print(false); -} diff --git a/scfence/inference.h b/scfence/inference.h deleted file mode 100644 index 2d61e598..00000000 --- a/scfence/inference.h +++ /dev/null @@ -1,154 +0,0 @@ -#ifndef _INFERENCE_H -#define _INFERENCE_H - -#include "fence_common.h" -#include "wildcard.h" -#include "patch.h" -#include "inferlist.h" - -class InferenceList; -class Inference; - -extern const char* get_mo_str(memory_order order); -extern bool isTheInference(Inference *infer); - -class Inference { - private: - memory_order *orders; - int size; - - /** It's initial inference, if not assigned, set it as itself */ - Inference *initialInfer; - - /** Whether this inference will lead to a buggy execution */ - bool buggy; - - /** Whether this inference has been explored */ - bool explored; - - /** Whether this inference is the leaf node in the inference lattice, see - * inferset.h for more details */ - bool leaf; - - /** When this inference will have buggy executions, this indicates whether - * it has any fixes. */ - bool hasFixes; - - /** When we have a strong enough inference, we also want to weaken specific - * parameters to see if it is possible to be weakened. So we will this - * field to mark if we should fix the inference or not if we get non-SC - * behaviros. By default true. */ - bool shouldFix; - - void resize(int newsize); - - /** Return the state of how we update a specific mo; If we have to make an - * uncompatible inference or that inference cannot be imposed because it's - * not a wildcard, it returns -1; if it is a compatible memory order but the - * current memory order is no weaker than mo, it returns 0; otherwise, it - * does strengthen the order, and returns 1 */ - int strengthen(const ModelAction *act, memory_order mo); - - public: - Inference(); - - Inference(Inference *infer); - - /** return value: - * 0 -> mo1 == mo2; - * 1 -> mo1 stronger than mo2; - * -1 -> mo1 weaker than mo2; - * 2 -> mo1 & mo2 are uncomparable. - */ - static int compareMemoryOrder(memory_order mo1, memory_order mo2); - - - /** Try to calculate the set of inferences that are weaker than this, but - * still stronger than infer */ - InferenceList* getWeakerInferences(Inference *infer); - - static memory_order nextWeakOrder(memory_order mo1, memory_order mo2); - - void getWeakerInferences(InferenceList* list, Inference *tmpRes, Inference *infer1, - Inference *infer2, SnapVector *strengthened, unsigned idx); - - int getSize() { - return size; - } - - memory_order &operator[](int idx); - - /** A simple overload, which allows caller to pass two boolean refrence, and - * we will set those two variables indicating whether we can update the - * order (copatible or not) and have updated the order */ - int strengthen(const ModelAction *act, memory_order mo, bool &canUpdate, - bool &hasUpdated); - - /** @Return: - 1 -> 'this> infer'; - -1 -> 'this < infer' - 0 -> 'this == infer' - INFERENCE_INCOMPARABLE(x) -> true means incomparable - */ - int compareTo(const Inference *infer) const; - - void setInitialInfer(Inference *val) { - initialInfer = val; - } - - Inference* getInitialInfer() { - return initialInfer; - } - - void setShouldFix(bool val) { - shouldFix = val; - } - - bool getShouldFix() { - return shouldFix; - } - - void setHasFixes(bool val) { - hasFixes = val; - } - - bool getHasFixes() { - return hasFixes; - } - - void setBuggy(bool val) { - buggy = val; - } - - bool getBuggy() { - return buggy; - } - - void setExplored(bool val) { - explored = val; - } - - bool isExplored() { - return explored; - } - - void setLeaf(bool val) { - leaf = val; - } - - bool isLeaf() { - return leaf; - } - - unsigned long getHash(); - - void print(); - void print(bool hasHash); - - ~Inference() { - model_free(orders); - } - - MEMALLOC -}; -#endif diff --git a/scfence/inferlist.cc b/scfence/inferlist.cc deleted file mode 100644 index 5cb6326b..00000000 --- a/scfence/inferlist.cc +++ /dev/null @@ -1,207 +0,0 @@ -#include "inferlist.h" - -InferenceList::InferenceList() { - list = new ModelList; -} - -int InferenceList::getSize() { - return list->size(); -} - -void InferenceList::pop_back() { - list->pop_back(); -} - -Inference* InferenceList::back() { - return list->back(); -} - -void InferenceList::push_back(Inference *infer) { - list->push_back(infer); -} - -void InferenceList::pop_front() { - list->pop_front(); -} - -/** We should not call this function too often because we want a nicer - * abstraction of the list of inferences. So far, it will only be called in - * the functions in InferenceSet */ -ModelList* InferenceList::getList() { - return list; -} - -bool InferenceList::applyPatch(Inference *curInfer, Inference *newInfer, Patch *patch) { - bool canUpdate = true, - hasUpdated = false, - updateState = false; - for (int i = 0; i < patch->getSize(); i++) { - canUpdate = true; - hasUpdated = false; - PatchUnit *unit = patch->get(i); - newInfer->strengthen(unit->getAct(), unit->getMO(), canUpdate, hasUpdated); - if (!canUpdate) { - // This is not a feasible patch, bail - break; - } else if (hasUpdated) { - updateState = true; - } - } - if (updateState) { - return true; - } else { - return false; - } -} - -void InferenceList::applyPatch(Inference *curInfer, Patch* patch) { - if (list->empty()) { - Inference *newInfer = new Inference(curInfer); - if (!applyPatch(curInfer, newInfer, patch)) { - delete newInfer; - } else { - list->push_back(newInfer); - } - } else { - ModelList *newList = new ModelList; - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *oldInfer = *it; - Inference *newInfer = new Inference(oldInfer); - if (!applyPatch(curInfer, newInfer, patch)) { - delete newInfer; - } else { - newList->push_back(newInfer); - } - } - // Clean the old list - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - delete *it; - } - delete list; - list = newList; - } -} - -void InferenceList::applyPatch(Inference *curInfer, SnapVector *patches) { - if (list->empty()) { - for (unsigned i = 0; i < patches->size(); i++) { - Inference *newInfer = new Inference(curInfer); - Patch *patch = (*patches)[i]; - if (!applyPatch(curInfer, newInfer, patch)) { - delete newInfer; - } else { - list->push_back(newInfer); - } - } - } else { - ModelList *newList = new ModelList; - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *oldInfer = *it; - for (unsigned i = 0; i < patches->size(); i++) { - Inference *newInfer = new Inference(oldInfer); - Patch *patch = (*patches)[i]; - if (!applyPatch(curInfer, newInfer, patch)) { - delete newInfer; - } else { - newList->push_back(newInfer); - } - } - } - // Clean the old list - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - delete *it; - } - delete list; - list = newList; - } -} - -/** Append another list to this list */ -bool InferenceList::append(InferenceList *inferList) { - if (!inferList) - return false; - ModelList *l = inferList->list; - list->insert(list->end(), l->begin(), l->end()); - return true; -} - -/** Only choose the weakest existing candidates & they must be stronger than the - * current inference */ -void InferenceList::pruneCandidates(Inference *curInfer) { - ModelList *newCandidates = new ModelList(), - *candidates = list; - - ModelList::iterator it1, it2; - int compVal; - for (it1 = candidates->begin(); it1 != candidates->end(); it1++) { - Inference *cand = *it1; - compVal = cand->compareTo(curInfer); - if (compVal == 0) { - // If as strong as curInfer, bail - delete cand; - continue; - } - // Check if the cand is any stronger than those in the newCandidates - for (it2 = newCandidates->begin(); it2 != newCandidates->end(); it2++) { - Inference *addedInfer = *it2; - compVal = addedInfer->compareTo(cand); - if (compVal == 0 || compVal == 1) { // Added inference is stronger - delete addedInfer; - it2 = newCandidates->erase(it2); - it2--; - } - } - // Now push the cand to the list - newCandidates->push_back(cand); - } - delete candidates; - list = newCandidates; -} - -void InferenceList::clearAll() { - clearAll(list); -} - -void InferenceList::clearList() { - delete list; -} - -void InferenceList::clearAll(ModelList *l) { - for (ModelList::iterator it = l->begin(); it != - l->end(); it++) { - Inference *infer = *it; - delete infer; - } - delete l; -} - -void InferenceList::clearAll(InferenceList *inferList) { - clearAll(inferList->list); -} - -void InferenceList::print(InferenceList *inferList, const char *msg) { - print(inferList->getList(), msg); -} - -void InferenceList::print(ModelList *inferList, const char *msg) { - for (ModelList::iterator it = inferList->begin(); it != - inferList->end(); it++) { - int idx = distance(inferList->begin(), it); - Inference *infer = *it; - model_print("%s %d:\n", msg, idx); - infer->print(); - model_print("\n"); - } -} - -void InferenceList::print() { - print(list, "Inference"); -} - -void InferenceList::print(const char *msg) { - print(list, msg); -} diff --git a/scfence/inferlist.h b/scfence/inferlist.h deleted file mode 100644 index bc3476ac..00000000 --- a/scfence/inferlist.h +++ /dev/null @@ -1,64 +0,0 @@ -#ifndef _INFERLIST_H -#define _INFERLIST_H - -#include "fence_common.h" -#include "patch.h" -#include "inference.h" - -class Patch; -class PatchUnit; -class Inference; - -/** This class represents that the list of inferences that can fix the problem - */ -class InferenceList { - private: - ModelList *list; - - public: - InferenceList(); - int getSize(); - Inference* back(); - - /** We should not call this function too often because we want a nicer - * abstraction of the list of inferences. So far, it will only be called in - * the functions in InferenceSet */ - ModelList* getList(); - void push_back(Inference *infer); - void pop_front(); - void pop_back(); - bool applyPatch(Inference *curInfer, Inference *newInfer, Patch *patch); - - void applyPatch(Inference *curInfer, Patch* patch); - - void applyPatch(Inference *curInfer, SnapVector *patches); - - /** Append another list to this list */ - bool append(InferenceList *inferList); - - /** Only choose the weakest existing candidates & they must be stronger than the - * current inference */ - void pruneCandidates(Inference *curInfer); - - void clearAll(); - - void clearList(); - - static void clearAll(ModelList *l); - - static void clearAll(InferenceList *inferList); - - static void print(ModelList *inferList, const char *msg); - - static void print(InferenceList *inferList, const char *msg); - - void print(); - - void print(const char *msg); - - MEMALLOC - -}; - - -#endif diff --git a/scfence/inferset.cc b/scfence/inferset.cc deleted file mode 100644 index 7eeb003a..00000000 --- a/scfence/inferset.cc +++ /dev/null @@ -1,300 +0,0 @@ -#include "patch.h" -#include "inference.h" -#include "inferset.h" - -InferenceSet::InferenceSet() { - discoveredSet = new InferenceList; - results = new InferenceList; - candidates = new InferenceList; -} - -/** Print the result of inferences */ -void InferenceSet::printResults() { - results->print("Result"); - stat.print(); -} - -/** Print candidates of inferences */ -void InferenceSet::printCandidates() { - candidates->print("Candidate"); -} - -/** When we finish model checking or cannot further strenghen with the - * inference, we commit the inference to be explored; if it is feasible, we - * put it in the result list */ -void InferenceSet::commitInference(Inference *infer, bool feasible) { - ASSERT (infer); - - infer->setExplored(true); - FENCE_PRINT("Explored %lu\n", infer->getHash()); - if (feasible) { - addResult(infer); - } -} - -int InferenceSet::getCandidatesSize() { - return candidates->getSize(); -} - -int InferenceSet::getResultsSize() { - return results->getSize(); -} - -/** Be careful that if the candidate is not added, it will be deleted in this - * function. Therefore, caller of this function should just delete the list when - * finishing calling this function. */ -bool InferenceSet::addCandidates(Inference *curInfer, InferenceList *inferList) { - if (!inferList) - return false; - // First prune the list of inference - inferList->pruneCandidates(curInfer); - - ModelList *cands = inferList->getList(); - - // For the purpose of debugging, record all those inferences added here - InferenceList *addedCandidates = new InferenceList; - FENCE_PRINT("List size: %ld.\n", cands->size()); - bool added = false; - - /******** addCurInference ********/ - // Add the current inference to the set, but specifially it marks it as - // non-leaf node so that when it gets popped, we just need to commit it as - // explored - addCurInference(curInfer); - - ModelList::iterator it; - for (it = cands->begin(); it != cands->end(); it++) { - Inference *candidate = *it; - // Before adding those fixes, set its initial inference - candidate->setInitialInfer(curInfer->getInitialInfer()); - bool tmpAdded = false; - /******** addInference ********/ - tmpAdded = addInference(candidate); - if (tmpAdded) { - added = true; - it = cands->erase(it); - it--; - addedCandidates->push_back(candidate); - } - } - - // For debugging, print the list of candidates for this iteration - FENCE_PRINT("Current inference:\n"); - curInfer->print(); - FENCE_PRINT("\n"); - FENCE_PRINT("The added inferences:\n"); - addedCandidates->print("Candidates"); - FENCE_PRINT("\n"); - - // Clean up the candidates - inferList->clearList(); - FENCE_PRINT("potential results size: %d.\n", candidates->getSize()); - return added; -} - - -/** Check if we have stronger or equal inferences in the current result - * list; if we do, we remove them and add the passed-in parameter infer */ - void InferenceSet::addResult(Inference *infer) { - ModelList *list = results->getList(); - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *existResult = *it; - int compVal = existResult->compareTo(infer); - if (compVal == 0 || compVal == 1) { - // The existing result is equal or stronger, remove it - FENCE_PRINT("We are dumping the follwing inference because it's either too weak or the same:\n"); - existResult->print(); - FENCE_PRINT("\n"); - it = list->erase(it); - it--; - } - } - list->push_back(infer); - } - -/** Get the next available unexplored node; @Return NULL - * if we don't have next, meaning that we are done with exploring */ -Inference* InferenceSet::getNextInference() { - Inference *infer = NULL; - while (candidates->getSize() > 0) { - infer = candidates->back(); - candidates->pop_back(); - if (!infer->isLeaf()) { - commitInference(infer, false); - continue; - } - if (infer->getShouldFix() && hasBeenExplored(infer)) { - // Finish exploring this node - // Remove the node from the set - FENCE_PRINT("Explored inference:\n"); - infer->print(); - FENCE_PRINT("\n"); - continue; - } else { - return infer; - } - } - return NULL; -} - -/** Add the current inference to the set before adding fixes to it; in - * this case, fixes will be added afterwards, and infer should've been - * discovered */ -void InferenceSet::addCurInference(Inference *infer) { - infer->setLeaf(false); - candidates->push_back(infer); -} - -/** Add one weaker node (the stronger one has been explored and known to be SC, - * we just want to know if a weaker one might also be SC). - */ -void InferenceSet::addWeakerInference(Inference *curInfer) { - Inference *initialInfer = curInfer->getInitialInfer(); - model_print("Before adding weaker inferece, candidates size=%d\n", - candidates->getSize()); - ModelList *list = discoveredSet->getList(); - - // An array of strengthened wildcards - SnapVector *strengthened = new SnapVector; - model_print("Strengthened wildcards\n"); - for (int i = 1; i <= curInfer->getSize(); i++) { - memory_order mo1 = (*curInfer)[i], - mo2 = (*initialInfer)[i]; - int compVal = Inference::compareMemoryOrder(mo1, mo2); - if (!(compVal == 0 || compVal == 1)) { - model_print("assert failure\n"); - model_print("compVal=%d\n", compVal); - ASSERT (false); - } - if (compVal == 0) // Same - continue; - model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1), - get_mo_str(mo2)); - strengthened->push_back(i); - } - - for (unsigned i = 0; i < strengthened->size(); i++) { - int w = (*strengthened)[i]; // The wildcard - memory_order mo1 = (*curInfer)[w]; - memory_order mo2 = (*initialInfer)[w]; - memory_order weakerMO = Inference::nextWeakOrder(mo1, mo2); - Inference *weakerInfer1 = new Inference(curInfer); - Inference *weakerInfer2 = NULL; - if (mo1 == memory_order_acq_rel) { - if (mo2 == memory_order_acquire) { - (*weakerInfer1)[w] = memory_order_acquire; - } else if (mo2 == memory_order_release) { - (*weakerInfer1)[w] = memory_order_release; - } else { // relaxed - (*weakerInfer1)[w] = memory_order_acquire; - weakerInfer2 = new Inference(curInfer); - (*weakerInfer2)[w] = memory_order_release; - } - } else { - if (mo2 != weakerMO) - (*weakerInfer1)[w] = weakerMO; - } - - weakerInfer1->setShouldFix(false); - weakerInfer1->setLeaf(true); - if (weakerInfer2) { - weakerInfer2->setShouldFix(false); - weakerInfer2->setLeaf(true); - } - - bool foundIt = false; - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *discoveredInfer = *it; - // When we already have an equal inferences in the candidates list - int compVal = discoveredInfer->compareTo(weakerInfer1); - if (compVal == 0 && !discoveredInfer->isLeaf()) { - foundIt = true; - break; - } - } - if (!foundIt) { - addInference(weakerInfer1); - } - if (!weakerInfer2) - continue; - foundIt = false; - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *discoveredInfer = *it; - // When we already have an equal inferences in the candidates list - int compVal = discoveredInfer->compareTo(weakerInfer2); - if (compVal == 0 && !discoveredInfer->isLeaf()) { - foundIt = true; - break; - } - } - if (!foundIt) { - addInference(weakerInfer2); - } - } - - model_print("After adding weaker inferece, candidates size=%d\n", - candidates->getSize()); -} - -/** Add one possible node that represents a fix for the current inference; - * @Return true if the node to add has not been explored yet - */ -bool InferenceSet::addInference(Inference *infer) { - if (!hasBeenDiscovered(infer)) { - // We haven't discovered this inference yet - - // Newly added nodes are leaf by default - infer->setLeaf(true); - candidates->push_back(infer); - discoveredSet->push_back(infer); - FENCE_PRINT("Discovered a parameter assignment with hashcode %lu\n", infer->getHash()); - return true; - } else { - stat.notAddedAtFirstPlace++; - return false; - } -} - -/** Return false if we haven't discovered that inference yet. Basically we - * search the candidates list */ -bool InferenceSet::hasBeenDiscovered(Inference *infer) { - ModelList *list = discoveredSet->getList(); - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *discoveredInfer = *it; - // When we already have an equal inferences in the candidates list - int compVal = discoveredInfer->compareTo(infer); - if (compVal == 0) { - FENCE_PRINT("%lu has beend discovered.\n", - infer->getHash()); - return true; - } - // Or the discoveredInfer is explored and infer is strong than it is - if (compVal == -1 && discoveredInfer->isLeaf() && - discoveredInfer->isExplored()) { - return true; - } - } - return false; -} - -/** Return true if we have explored this inference yet. Basically we - * search the candidates list */ -bool InferenceSet::hasBeenExplored(Inference *infer) { - ModelList *list = discoveredSet->getList(); - for (ModelList::iterator it = list->begin(); it != - list->end(); it++) { - Inference *discoveredInfer = *it; - if (!discoveredInfer->isExplored()) - continue; - // When we already have an equal inferences in the candidates list - int compVal = discoveredInfer->compareTo(infer); - if (compVal == 0 || compVal == -1) { - return true; - } - } - return false; -} diff --git a/scfence/inferset.h b/scfence/inferset.h deleted file mode 100644 index 965d2f9c..00000000 --- a/scfence/inferset.h +++ /dev/null @@ -1,147 +0,0 @@ -#ifndef _INFERSET_H -#define _INFERSET_H - -#include "fence_common.h" -#include "patch.h" -#include "inference.h" -#include "inferlist.h" - -typedef struct inference_stat { - int notAddedAtFirstPlace; - - inference_stat() : - notAddedAtFirstPlace(0) {} - - void print() { - model_print("Inference process statistics output:...\n"); - model_print("The number of inference not added at the first place: %d\n", - notAddedAtFirstPlace); - } -} inference_stat_t; - - -/** Essentially, we have to explore a big lattice of inferences, the bottom of - * which is the inference that has all relaxed orderings, and the top of which - * is the one that has all SC orderings. We define the partial ordering between - * inferences as in compareTo() function in the Infereence class. In another - * word, we compare ordering parameters one by one as a vector. Theoretically, - * we need to explore up to the number of 5^N inferences, where N denotes the - * number of wildcards (since we have 5 possible options for each memory order). - - * We try to reduce the searching space by recording whether an inference has - * been discovered or not, and if so, we only need to explore from that - * inference for just once. We can use a set to record the inferences to be be - * explored, and insert new undiscovered fixes to that set iteratively until it - * gets empty. - - * In detail, we use the InferenceList to represent that set, and use a - * LIFO-like actions in pushing and popping inferences. When we add an - * inference to the stack, we will set it to leaf or non-leaf node. For the - * current inference to be added, it is non-leaf node because it generates - * stronger inferences. On the other hands, for those generated inferences, we - * set them to be leaf node. So when we pop a leaf node, we know that it is - * not just discovered but thoroughly explored. Therefore, when we dicide - * whether an inference is discovered, we can first try to look up the - * discovered set and also derive those inferences that are stronger the - * explored ones to be discovered. - - ********** The main algorithm ********** - Initial: - InferenceSet set; // Store the candiates to explore in a set - Set discoveredSet; // Store the discovered candidates. For each discovered - // candidate, if it's explored (feasible or infeasible, meaning that - // they are already known to work or not work), we set it to be - // explored. With that, we can reduce the searching space by ignoring - // those candidates that are stronger than the explored ones. - Inference curInfer = RELAX; // Initialize the current inference to be all relaxed (RELAX) - - API Methods: - bool addInference(infer, bool isLeaf) { - // Push back infer to the discovered when it's not discvoerd, and return - // whether it's added or not - } - - void commitInference(infer, isFeasible) { - // Set the infer to be explored and add it to the result set if feasible - } - - Inference* getNextInference() { - // Get the next unexplored inference so that we can contine searching - } -*/ - -class InferenceSet { - private: - - /** The set of already discovered nodes in the tree */ - InferenceList *discoveredSet; - - /** The list of feasible inferences */ - InferenceList *results; - - /** The set of candidates */ - InferenceList *candidates; - - /** The staticstics of inference process */ - inference_stat_t stat; - - public: - InferenceSet(); - - /** Print the result of inferences */ - void printResults(); - - /** Print candidates of inferences */ - void printCandidates(); - - /** When we finish model checking or cannot further strenghen with the - * inference, we commit the inference to be explored; if it is feasible, we - * put it in the result list */ - void commitInference(Inference *infer, bool feasible); - - int getCandidatesSize(); - - int getResultsSize(); - - /** Be careful that if the candidate is not added, it will be deleted in this - * function. Therefore, caller of this function should just delete the list when - * finishing calling this function. */ - bool addCandidates(Inference *curInfer, InferenceList *inferList); - - - /** Check if we have stronger or equal inferences in the current result - * list; if we do, we remove them and add the passed-in parameter infer */ - void addResult(Inference *infer); - - /** Get the next available unexplored node; @Return NULL - * if we don't have next, meaning that we are done with exploring */ - Inference* getNextInference(); - - /** Add the current inference to the set before adding fixes to it; in - * this case, fixes will be added afterwards, and infer should've been - * discovered */ - void addCurInference(Inference *infer); - - /** Add one weaker node (the stronger one has been explored and known to be SC, - * we just want to know if a weaker one might also be SC). - * @Return true if the node to add has not been explored yet - */ - void addWeakerInference(Inference *curInfer); - - /** Add one possible node that represents a fix for the current inference; - * @Return true if the node to add has not been explored yet - */ - bool addInference(Inference *infer); - - /** Return false if we haven't discovered that inference yet. Basically we - * search the candidates list */ - bool hasBeenDiscovered(Inference *infer); - - /** Return true if we have explored this inference yet. Basically we - * search the candidates list */ - bool hasBeenExplored(Inference *infer); - - MEMALLOC -}; - -#endif diff --git a/scfence/patch.cc b/scfence/patch.cc deleted file mode 100644 index 3fabe010..00000000 --- a/scfence/patch.cc +++ /dev/null @@ -1,69 +0,0 @@ -#include "patch.h" -#include "inference.h" - -Patch::Patch(const ModelAction *act, memory_order mo) { - PatchUnit *unit = new PatchUnit(act, mo); - units = new SnapVector; - units->push_back(unit); -} - -Patch::Patch(const ModelAction *act1, memory_order mo1, const ModelAction *act2, memory_order mo2) { - units = new SnapVector; - PatchUnit *unit = new PatchUnit(act1, mo1); - units->push_back(unit); - unit = new PatchUnit(act2, mo2); - units->push_back(unit); -} - -Patch::Patch() { - units = new SnapVector; -} - -bool Patch::canStrengthen(Inference *curInfer) { - if (!isApplicable()) - return false; - bool res = false; - for (unsigned i = 0; i < units->size(); i++) { - PatchUnit *u = (*units)[i]; - memory_order wildcard = u->getAct()->get_original_mo(); - memory_order curMO = (*curInfer)[get_wildcard_id(wildcard)]; - if (u->getMO() != curMO) - res = true; - } - return res; -} - -bool Patch::isApplicable() { - for (unsigned i = 0; i < units->size(); i++) { - PatchUnit *u = (*units)[i]; - memory_order wildcard = u->getAct()->get_original_mo(); - if (is_wildcard(wildcard)) - continue; - int compVal = Inference::compareMemoryOrder(wildcard, u->getMO()); - if (compVal == 2 || compVal == -1) - return false; - } - return true; -} - -void Patch::addPatchUnit(const ModelAction *act, memory_order mo) { - PatchUnit *unit = new PatchUnit(act, mo); - units->push_back(unit); -} - -int Patch::getSize() { - return units->size(); -} - -PatchUnit* Patch::get(int i) { - return (*units)[i]; -} - -void Patch::print() { - for (unsigned i = 0; i < units->size(); i++) { - PatchUnit *u = (*units)[i]; - model_print("wildcard %d -> %s\n", - get_wildcard_id_zero(u->getAct()->get_original_mo()), - get_mo_str(u->getMO())); - } -} diff --git a/scfence/patch.h b/scfence/patch.h deleted file mode 100644 index d25bed19..00000000 --- a/scfence/patch.h +++ /dev/null @@ -1,59 +0,0 @@ -#ifndef _PATCH_H -#define _PATCH_H - -#include "fence_common.h" -#include "inference.h" - -class PatchUnit; -class Patch; - -class PatchUnit { - private: - const ModelAction *act; - memory_order mo; - - public: - PatchUnit(const ModelAction *act, memory_order mo) { - this->act= act; - this->mo = mo; - } - - const ModelAction* getAct() { - return act; - } - - memory_order getMO() { - return mo; - } - - SNAPSHOTALLOC -}; - -class Patch { - private: - SnapVector *units; - - public: - Patch(const ModelAction *act, memory_order mo); - - Patch(const ModelAction *act1, memory_order mo1, const ModelAction *act2, - memory_order mo2); - - Patch(); - - bool canStrengthen(Inference *curInfer); - - bool isApplicable(); - - void addPatchUnit(const ModelAction *act, memory_order mo); - - int getSize(); - - PatchUnit* get(int i); - - void print(); - - SNAPSHOTALLOC -}; - -#endif diff --git a/scfence/sc_annotation.h b/scfence/sc_annotation.h deleted file mode 100644 index 1f371072..00000000 --- a/scfence/sc_annotation.h +++ /dev/null @@ -1,47 +0,0 @@ -#ifndef _SC_ANNOTATION_H -#define _SC_ANNOTATION_H - -#include "cdsannotate.h" -#include "action.h" - -#define SC_ANNOTATION 2 - -#define BEGIN 1 -#define END 2 -#define KEEP 3 - - -inline bool IS_SC_ANNO(ModelAction *act) { - return act != NULL && act->is_annotation() && - act->get_value() == SC_ANNOTATION; -} - -inline bool IS_ANNO_BEGIN(ModelAction *act) { - return (void*) BEGIN == act->get_location(); -} - -inline bool IS_ANNO_END(ModelAction *act) { - return (void*) END == act->get_location(); -} - -inline bool IS_ANNO_KEEP(ModelAction *act) { - return (void*) KEEP == act->get_location(); -} - -inline void SC_BEGIN() { - void *loc = (void*) BEGIN; - cdsannotate(SC_ANNOTATION, loc); -} - -inline void SC_END() { - void *loc = (void*) END; - cdsannotate(SC_ANNOTATION, loc); -} - -inline void SC_KEEP() { - void *loc = (void*) KEEP; - cdsannotate(SC_ANNOTATION, loc); -} - - -#endif diff --git a/scfence/scfence.cc b/scfence/scfence.cc deleted file mode 100644 index 130dc3b1..00000000 --- a/scfence/scfence.cc +++ /dev/null @@ -1,1298 +0,0 @@ -#include "scfence.h" -#include "action.h" -#include "threads-model.h" -#include "clockvector.h" -#include "execution.h" -#include "cyclegraph.h" -#include - -#include "model.h" -#include "wildcard.h" -#include "inference.h" -#include "inferset.h" -#include "sc_annotation.h" -#include "errno.h" -#include -#include - -scfence_priv *SCFence::priv; - -SCFence::SCFence() : - scgen(new SCGenerator), - stats((struct sc_statistics *)model_calloc(1, sizeof(struct sc_statistics))), - execution(NULL) -{ - priv = new scfence_priv(); - weaken = true; -} - -SCFence::~SCFence() { - delete(stats); -} - -void SCFence::setExecution(ModelExecution * execution) { - this->execution=execution; -} - -const char * SCFence::name() { - const char * name = "AUTOMO"; - return name; -} - -void SCFence::finish() { - model_print("SCFence finishes!\n"); -} - - -/******************** SCFence-related Functions (Beginning) ********************/ - -void SCFence::inspectModelAction(ModelAction *act) { - if (act == NULL) // Get pass cases like data race detector - return; - if (act->get_mo() >= memory_order_relaxed && act->get_mo() <= - memory_order_seq_cst) { - return; - } else if (act->get_mo() == memory_order_normal) { - // For the purpose of eliminating data races - act->set_mo(memory_order_relaxed); - } else { // For wildcards - Inference *curInfer = getCurInference(); - int wildcardID = get_wildcard_id(act->get_mo()); - memory_order order = (*curInfer)[wildcardID]; - if (order == WILDCARD_NONEXIST) { - (*curInfer)[wildcardID] = memory_order_relaxed; - act->set_mo(memory_order_relaxed); - } else { - act->set_mo((*curInfer)[wildcardID]); - } - } -} - - -void SCFence::actionAtInstallation() { - // When this pluggin gets installed, it become the inspect_plugin - model->set_inspect_plugin(this); -} - -void SCFence::analyze(action_list_t *actions) { - scgen->setActions(actions); - scgen->setExecution(execution); - dup_threadlists = scgen->getDupThreadLists(); - if (getTimeout() > 0 && isTimeout()) { - model_print("Backtrack because we reached the timeout bound.\n"); - routineBacktrack(false); - return; - } - - /* Build up the thread lists for general purpose */ - mo_graph = execution->get_mo_graph(); - - // First of all check if there's any uninitialzed read bugs - if (execution->have_bug_reports()) { - setBuggy(true); - } - - action_list_t *list = scgen->getSCList(); - bool cyclic = scgen->getCyclic(); - - struct sc_statistics *s = scgen->getStats(); - stats->nonsccount += s->nonsccount; - stats->sccount += s->sccount; - stats->elapsedtime += s->elapsedtime; - stats->actions += s->actions; - - if (!cyclic && execution->have_bug_reports()) { - model_print("Be careful. This execution has bugs and still SC\n"); - } - - if (!cyclic && scgen->getPrintAlways()) { - scgen->print_list(list); - } - - // Now we find a non-SC execution - if (cyclic) { - /******** The Non-SC case (beginning) ********/ - // Only print those that should be fixed - if (getCurInference()->getShouldFix()) - scgen->print_list(list); - bool added = addFixes(list, NON_SC); - if (added) { - routineAfterAddFixes(); - return; - } else { // Couldn't imply anymore, backtrack - routineBacktrack(false); - return; - } - /******** The Non-SC case (end) ********/ - } else { - /******** The implicit MO case (beginning) ********/ - if (getInferImplicitMO() && execution->too_many_steps() && - !execution->is_complete_execution()) { - // Only print those that should be fixed - if (getCurInference()->getShouldFix()) - scgen->print_list(list); - bool added = addFixes(list, IMPLICIT_MO); - if (added) { - FENCE_PRINT("Found an implicit mo pattern to fix!\n"); - routineAfterAddFixes(); - return; - } else { - // This can be a good execution, so we can't do anything, - return; - } - } - /******** The implicit MO case (end) ********/ - - /******** The checking data races case (beginning) ********/ - bool added = addFixes(list, DATA_RACE); - if (added) { - FENCE_PRINT("Found an data race pattern to fix!\n"); - routineAfterAddFixes(); - return; - } - } -} - -void SCFence::exitModelChecker() { - model->exit_model_checker(); -} - -void SCFence::restartModelChecker() { - model->restart(); - if (!getHasRestarted()) - setHasRestarted(true); -} - -bool SCFence::modelCheckerAtExitState() { - return model->get_exit_flag(); -} - -void SCFence::actionAtModelCheckingFinish() { - // Just bail if the model checker is at the exit state - if (modelCheckerAtExitState()) - return; - - /** Backtrack with a successful inference */ - routineBacktrack(true); -} - -void SCFence::initializeByFile() { - char *name = getCandidateFile(); - FILE *fp = fopen(name, "r"); - if (fp == NULL) { - fprintf(stderr, "Cannot open the input parameter assignment file: %s!\n", name); - perror(name); - exit(EXIT_FAILURE); - } - Inference *infer = NULL; - int curNum = 0; - memory_order mo = memory_order_relaxed; - char *str = (char *) malloc(sizeof(char) * (30 + 1)); - bool isProcessing = false; - int ret = 0; - while (!feof(fp)) { - // Result #: - if (!isProcessing) { - ret = fscanf(fp, "%s", str); - } - if (strcmp(str, "Result") == 0 || isProcessing) { // In an inference - ret = fscanf(fp, "%s", str); - - infer = new Inference(); - isProcessing = false; - while (!feof(fp)) { // Processing a specific inference - // wildcard # -> memory_order - ret = fscanf(fp, "%s", str); - - if (strcmp(str, "Result") == 0) { - isProcessing = true; - break; - } - ret = fscanf(fp, "%d", &curNum); - ret = fscanf(fp, "%s", str); - if (ret <= 0 && ret != -1) { - fprintf(stderr, "The input parameter assignment file has wrong format\n"); - perror(name); - exit(EXIT_FAILURE); - } - ret = fscanf(fp, "%s", str); - - if (strcmp(str, "memory_order_relaxed") == 0) - mo = memory_order_relaxed; - else if (strcmp(str, "memory_order_acquire") == 0) - mo = memory_order_acquire; - else if (strcmp(str, "memory_order_release") == 0) - mo = memory_order_release; - else if (strcmp(str, "memory_order_acq_rel") == 0) - mo = memory_order_acq_rel; - else if (strcmp(str, "memory_order_seq_cst") == 0) - mo = memory_order_seq_cst; - (*infer)[curNum] = mo; - } - - /******** addInference ********/ - if (!addInference(infer)) - delete infer; - } - } - fclose(fp); - - FENCE_PRINT("candidate size from file: %d\n", setSize()); - Inference *next = getNextInference(); - if (!next) { - model_print("Wrong with the candidate file\n"); - } else { - setCurInference(next); - } -} - -char* SCFence::parseOptionHelper(char *opt, int *optIdx) { - char *res = (char*) model_malloc(1024 * sizeof(char)); - int resIdx = 0; - while (opt[*optIdx] != '\0' && opt[*optIdx] != '|') { - res[resIdx++] = opt[(*optIdx)++]; - } - res[resIdx] = '\0'; - return res; -} - -bool SCFence::parseOption(char *opt) { - int optIdx = 0; - char *val = NULL; - while (true) { - char option = opt[optIdx++]; - val = parseOptionHelper(opt, &optIdx); - switch (option) { - case 'f': // Read initial inference from file - setCandidateFile(val); - if (strcmp(val, "") == 0) { - model_print("Need to specify a file that contains initial inference!\n"); - return true; - } - break; - case 'b': // The bound above - setImplicitMOReadBound(atoi(val)); - if (getImplicitMOReadBound() <= 0) { - model_print("Enter valid bound value!\n"); - return true; - } - break; - case 'm': // Infer the modification order from repetitive reads from - // the same write - setInferImplicitMO(true); - if (strcmp(val, "") != 0) { - model_print("option m doesn't take any arguments!\n"); - return true; - } - break; - case 'a': // Turn on the annotation mode - scgen->setAnnotationMode(true); - if (strcmp(val, "") != 0) { - model_print("option a doesn't take any arguments!\n"); - return true; - } - break; - case 't': // The timeout set to force the analysis to backtrack - model_print("Parsing t option!\n"); - model_print("t value: %s\n", val); - setTimeout(atoi(val)); - break; - default: - model_print("Unknown SCFence option: %c!\n", option); - return true; - break; - } - if (opt[optIdx] == '|') { - optIdx++; - } else { - break; - } - } - return false; - -} - -char* SCFence::getInputFileName(char *opt) { - char *res = NULL; - if (opt[0] == 'f' && - opt[1] == 'i' && - opt[2] == 'l' && - opt[3] == 'e' && - opt[4] == '-') { - - res = (char*) model_malloc(1024 * sizeof(char)); - int i = 0, j = 5; - while (opt[j] != '\0') { - res[i++] = opt[j++]; - } - res[i] = '\0'; - } - return res; -} - -int SCFence::getImplicitMOBound(char *opt) { - char *num = NULL; - if (opt[0] == 'b' && - opt[1] == 'o' && - opt[2] == 'u' && - opt[3] == 'n' && - opt[4] == 'd' && - opt[5] == '-') { - - num = (char*) model_malloc(1024 * sizeof(char)); - int i = 0, j = 6; - while (opt[j] != '\0') { - num[i++] = opt[j++]; - } - num[i] = '\0'; - } - if (num) { - return atoi(num); - } else { - return 0; - } -} - -bool SCFence::option(char * opt) { - char *inputFileName = NULL; - unsigned implicitMOBoundNum = 0; - - if (strcmp(opt, "verbose")==0) { - scgen->setPrintAlways(true); - return false; - } else if (strcmp(opt, "buggy")==0) { - return false; - } else if (strcmp(opt, "quiet")==0) { - scgen->setPrintBuggy(false); - return false; - } else if (strcmp(opt, "nonsc")==0) { - scgen->setPrintNonSC(true); - return false; - } else if (strcmp(opt, "time")==0) { - time=true; - return false; - } else if (strcmp(opt, "no-weaken")==0) { - weaken=false; - return false; - } else if (strcmp(opt, "anno")==0) { - scgen->setAnnotationMode(true); - return false; - } else if (strcmp(opt, "implicit-mo")==0) { - setInferImplicitMO(true); - return false; - } else if ((inputFileName = getInputFileName(opt)) != NULL) { - if (strcmp(inputFileName, "") == 0) { - model_print("Need to specify a file that contains initial inference!\n"); - return true; - } - setCandidateFile(inputFileName); - initializeByFile(); - return false; - } else if ((implicitMOBoundNum = getImplicitMOBound(opt)) > 0) { - setImplicitMOReadBound(implicitMOBoundNum); - return false; - } else { - model_print("file-InputFile -- takes candidate file as argument right after the symbol '-' \n"); - model_print("no-weaken -- turn off the weakening mode (by default ON)\n"); - model_print("anno -- turn on the annotation mode (by default OFF)\n"); - model_print("implicit-mo -- imply implicit modification order, takes no arguments (by default OFF, default bound is %d\n", DEFAULT_REPETITIVE_READ_BOUND); - model_print("bound-NUM -- specify the bound for the implicit mo implication, takes a number as argument right after the symbol '-'\n"); - model_print("\n"); - return true; - } -} - -/** Check whether a chosen reads-from path is a release sequence */ -bool SCFence::isReleaseSequence(path_t *path) { - ASSERT (path); - path_t::reverse_iterator rit = path->rbegin(), - rit_next; - const ModelAction *read, - *write, - *next_read; - for (; rit != path->rend(); rit++) { - read = *rit; - rit_next = rit; - rit_next++; - write = read->get_reads_from(); - if (rit_next != path->rend()) { - next_read = *rit_next; - if (write != next_read) { - return false; - } - } - } - return true; -} - -/** Only return those applicable patches in a vector */ -SnapVector* SCFence::getAcqRel(const ModelAction *read, const - ModelAction *readBound,const ModelAction *write, const ModelAction *writeBound) { - - SnapVector *patches = new SnapVector; - /* Also support rel/acq fences synchronization here */ - // Look for the acq fence after the read action - int readThrdID = read->get_tid(), - writeThrdID = write->get_tid(); - action_list_t *readThrd = &(*dup_threadlists)[readThrdID], - *writeThrd = &(*dup_threadlists)[writeThrdID]; - action_list_t::iterator readIter = std::find(readThrd->begin(), - readThrd->end(), read); - action_list_t::reverse_iterator writeIter = std::find(writeThrd->rbegin(), - writeThrd->rend(), write); - - action_list_t *acqFences = new action_list_t, - *relFences = new action_list_t; - ModelAction *act = *readIter; - while (readIter++ != readThrd->end() && act != readBound) { - if (act->is_fence()) { - acqFences->push_back(act); - } - act = *readIter; - } - act = *writeIter; - while (writeIter++ != writeThrd->rend() && act != writeBound) { - if (act->is_fence()) { - relFences->push_back(act); - } - act = *writeIter; - } - // Now we have a list of rel/acq fences at hand - int acqFenceSize = acqFences->size(), - relFenceSize = relFences->size(); - - Patch *p; - if (acqFenceSize == 0 && relFenceSize == 0) { - //return patches; - } else if (acqFenceSize > 0 && relFenceSize == 0) { - for (action_list_t::iterator it = acqFences->begin(); it != - acqFences->end(); it++) { - ModelAction *fence = *it; - p = new Patch(fence, memory_order_acquire, write, memory_order_release); - if (p->isApplicable()) - patches->push_back(p); - } - } else if (acqFenceSize == 0 && relFenceSize > 0) { - for (action_list_t::iterator it = relFences->begin(); it != - relFences->end(); it++) { - ModelAction *fence = *it; - p = new Patch(fence, memory_order_release, read, memory_order_acquire); - if (p->isApplicable()) - patches->push_back(p); - } - } else { - /* Impose on both relFences and acqFences */ - bool twoFences = false; - for (action_list_t::iterator it1 = relFences->begin(); it1 != - relFences->end(); it1++) { - ModelAction *relFence = *it1; - for (action_list_t::iterator it2 = acqFences->begin(); it2 != - acqFences->end(); it2++) { - ModelAction *acqFence = *it2; - p = new Patch(relFence, memory_order_release, acqFence, memory_order_acquire); - if (p->isApplicable()) { - patches->push_back(p); - twoFences = true; - } - } - } - if (!twoFences) { - /* Only impose on the acqFences */ - for (action_list_t::iterator it = acqFences->begin(); it != - acqFences->end(); it++) { - ModelAction *fence = *it; - p = new Patch(fence, memory_order_acquire, write, memory_order_release); - if (p->isApplicable()) - patches->push_back(p); - } - /* Only impose on the relFences */ - for (action_list_t::iterator it = relFences->begin(); it != - relFences->end(); it++) { - ModelAction *fence = *it; - p = new Patch(fence, memory_order_release, read, memory_order_acquire); - if (p->isApplicable()) - patches->push_back(p); - } - } - } - - // If we can find a fix with fences, we don't fix on the operation - if (patches->size() > 0) - return patches; - p = new Patch(read, memory_order_acquire, write, - memory_order_release); - if (p->isApplicable()) - patches->push_back(p); - return patches; -} - -/** Impose the synchronization between the begin and end action, and the paths - * are a list of paths that each represent the union of rfUsb. We then - * strengthen the current inference by necessity. - */ -bool SCFence::imposeSync(InferenceList *inferList, - paths_t *paths, const ModelAction *begin, const ModelAction *end) { - if (!inferList) - return false; - bool res = false; - for (paths_t::iterator i_paths = paths->begin(); i_paths != paths->end(); i_paths++) { - // Iterator over all the possible paths - path_t *path = *i_paths; - InferenceList *cands = new InferenceList; - // Impose synchronization by path - if (imposeSync(cands, path, begin, end)) - res = true; - inferList->append(cands); - } - return res; -} - -/** Impose the synchronization between the begin and end action, and the path - * is the union of rfUsb. We then strengthen the current inference by - * necessity. - */ -bool SCFence::imposeSync(InferenceList *inferList, - path_t *path, const ModelAction *begin, const ModelAction *end) { - - bool release_seq = isReleaseSequence(path); - SnapVector *patches; - if (release_seq) { - const ModelAction *relHead = path->front()->get_reads_from(), - *lastRead = path->back(); - patches = getAcqRel(lastRead, end, relHead, begin); - if (patches->size() == 0) - return false; - inferList->applyPatch(getCurInference(), patches); - delete patches; - // Bail now for the release sequence because - return true; - } - - for (path_t::iterator it = path->begin(); it != path->end(); it++) { - const ModelAction *read = *it, - *write = read->get_reads_from(), - *prevRead = NULL, *nextRead; - - const ModelAction *readBound = NULL, - *writeBound = NULL; - nextRead = *++it; - if (it == path->end()) { - nextRead = NULL; - } - it--; - if (prevRead) { - readBound = prevRead->get_reads_from(); - } else { - readBound = end; - } - if (nextRead) { - writeBound = nextRead; - } else { - writeBound = begin; - } - - /* Extend to support rel/acq fences synchronization here */ - patches = getAcqRel(read, readBound, write, writeBound); - - if (patches->size() == 0) { - // We cannot strengthen the inference - return false; - } - - inferList->applyPatch(getCurInference(), patches); - delete patches; - } - return true; -} - -/** Impose SC orderings to related actions (including fences) such that we - * either want to establish mo between act1 & act2 (act1 -mo-> act2) when they - * can't establish hb; or that act2 can't read from any actions that are - * modification ordered before act1. All these requirements are consistent with - * the following strengthening strategy: - * 1. make both act1 and act2 SC - * 2. if there are fences in between act1 & act2, and the fences are either in - * the threads of either act1 or act2, we can impose SC on the fences or - * corresponding actions. - */ -bool SCFence::imposeSC(action_list_t * actions, InferenceList *inferList, const ModelAction *act1, const ModelAction *act2) { - if (!inferList) { - return false; - } - action_list_t::iterator act1Iter = std::find(actions->begin(), - actions->end(), act1); - action_list_t::iterator act2Iter = std::find(act1Iter, - actions->end(), act2); - - action_list_t::iterator it = act1Iter; - it++; - action_list_t *fences = new action_list_t; - int size = 0; - while (it != act2Iter) { - ModelAction *fence = *it; - it++; - if (!fence->is_fence()) - continue; - if (!is_wildcard(fence->get_original_mo())) - continue; - fences->push_back(fence); - size++; - } - - Patch *p; - SnapVector *patches = new SnapVector; - - bool twoFences = false; - // Impose SC on two fences - for (action_list_t::iterator fit1 = fences->begin(); fit1 != fences->end(); - fit1++) { - ModelAction *fence1 = *fit1; - action_list_t::iterator fit2 = fit1; - fit2++; - for (; fit2 != fences->end(); fit2++) { - ModelAction *fence2 = *fit2; - p = new Patch(fence1, memory_order_seq_cst, fence2, memory_order_seq_cst); - if (p->isApplicable()) { - Inference *curInfer = getCurInference(); - memory_order mo1 = (*curInfer)[get_wildcard_id(fence1->get_original_mo())]; - memory_order mo2 = (*curInfer)[get_wildcard_id(fence2->get_original_mo())]; - // We can avoid this by adding two fences - if (mo1 != memory_order_seq_cst || mo2 != memory_order_seq_cst) - twoFences = true; - patches->push_back(p); - } - } - } - - // Just impose SC on one fence - if (!twoFences) { - for (action_list_t::iterator fit = fences->begin(); fit != fences->end(); - fit++) { - ModelAction *fence = *fit; - model_print("one fence\n"); - fence->print(); - p = new Patch(act1, memory_order_seq_cst, fence, memory_order_seq_cst); - if (p->isApplicable()) { - // We can avoid this by adding two fences - patches->push_back(p); - } - p = new Patch(act2, memory_order_seq_cst, fence, memory_order_seq_cst); - if (p->isApplicable()) { - // We can avoid this by adding two fences - patches->push_back(p); - } - } - - p = new Patch(act1, memory_order_seq_cst, act2, memory_order_seq_cst); - if (p->isApplicable()) { - patches->push_back(p); - } - } - - if (patches->size() > 0) { - inferList->applyPatch(getCurInference(), patches); - return true; - } - return false; -} - -/** A subroutine that calculates the potential fixes for the non-sc pattern (a), - * a.k.a old value reading. The whole idea is as follows. - * write -isc-> write2 && write2 -isc->read && write -rf-> read!!! - * The fix can be two-step: - * a. make write -mo-> write2, and we can accomplish this by imposing hb - * between write and write2, and if not possible, make write -sc-> write2 - * b. make write2 -hb-> read, and if not possible, make write2 -sc-> read. - */ -InferenceList* SCFence::getFixesFromPatternA(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter) { - ModelAction *read = *readIter, - *write = *writeIter; - - InferenceList *candidates = new InferenceList; - paths_t *paths1, *paths2; - - // Find all writes between the write1 and the read - action_list_t *write2s = new action_list_t(); - ModelAction *write2; - action_list_t::iterator findIt = writeIter; - findIt++; - do { - write2 = *findIt; - if (write2->is_write() && write2->get_location() == - write->get_location()) { - write2s->push_back(write2); - } - findIt++; - } while (findIt != readIter); - - // Found all the possible write2s - FENCE_PRINT("write2s set size: %ld\n", write2s->size()); - for (action_list_t::iterator itWrite2 = write2s->begin(); - itWrite2 != write2s->end(); itWrite2++) { - InferenceList *tmpCandidates = new InferenceList; - write2 = *itWrite2; - // Whether the write and the write2 originally have modification order - bool isWritesMO = false; - FENCE_PRINT("write2:\n"); - ACT_PRINT(write2); - // write1->write2 (write->write2) - // Whether write -mo-> write2 - if (!mo_graph->checkReachable(write, write2)) { - paths1 = get_rf_sb_paths(write, write2); - if (paths1->size() > 0) { - FENCE_PRINT("From write1 to write2: \n"); - print_rf_sb_paths(paths1, write, write2); - // FIXME: Need to make sure at least one path is feasible; what - // if we got empty candidates here, maybe should then impose SC, - // same in the write2->read - imposeSync(tmpCandidates, paths1, write, write2); - } else { - FENCE_PRINT("Have to impose sc on write1 & write2: \n"); - ACT_PRINT(write); - ACT_PRINT(write2); - imposeSC(list, tmpCandidates, write, write2); - } - } else { - if (!write->happens_before(write2)) { - isWritesMO = true; - } - FENCE_PRINT("write1 mo before write2. \n"); - } - - // write2->read (write2->read) - // now we only need to make write2 -hb-> read - if (!write2->happens_before(read)) { - paths2 = get_rf_sb_paths(write2, read); - if (paths2->size() > 0) { - FENCE_PRINT("From write2 to read: \n"); - print_rf_sb_paths(paths2, write2, read); - imposeSync(tmpCandidates, paths2, write2, read); - } else { - FENCE_PRINT("Have to impose sc on write2 & read: \n"); - ACT_PRINT(write2); - ACT_PRINT(read); - imposeSC(list, tmpCandidates, write2, read); - if (isWritesMO) { - // Also need to make sure write -sc/hb-> write2 - FENCE_PRINT("Also have to impose hb/sc on write & write2: \n"); - ACT_PRINT(write); - ACT_PRINT(write2); - paths1 = get_rf_sb_paths(write, write2); - if (paths1->size() > 0) { - FENCE_PRINT("Impose hb, from write1 to write2: \n"); - print_rf_sb_paths(paths1, write, write2); - imposeSync(tmpCandidates, paths1, write, write2); - } else { - FENCE_PRINT("Also have to impose sc on write1 & write2: \n"); - ACT_PRINT(write); - ACT_PRINT(write2); - imposeSC(list, tmpCandidates, write, write2); - } - } - } - } else { - FENCE_PRINT("write2 hb before read. \n"); - } - candidates->append(tmpCandidates); - } - // Return the complete list of candidates - return candidates; -} - -/** To fix this pattern, we have two options: - * 1. impose futureWrite -hb-> read so that the SC analysis will order - * in a way that the the write is ordered before the read; - * 2. impose read -hb->futureWrite so that the reads-from edge from futureWrite - * to the read is not allowed. -*/ -InferenceList* SCFence::getFixesFromPatternB(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter) { - InferenceList *res = new InferenceList, - *candidates = new InferenceList; - - ModelAction *read = *readIter, - *write = *writeIter; - // Fixing one direction (read -> futureWrite) - paths_t *paths1 = get_rf_sb_paths(read, write); - if (paths1->size() > 0) { - FENCE_PRINT("From read to future write: \n"); - print_rf_sb_paths(paths1, read, write); - imposeSync(res, paths1, read, write); - } - - // Fixing the other direction (futureWrite -> read) for one edge case - paths_t *paths2 = get_rf_sb_paths(write, read); - FENCE_PRINT("From future write to read (edge case): \n"); - print_rf_sb_paths(paths2, write, read); - imposeSync(candidates, paths2, write, read); - - // Append the candidates to the res list - res->append(candidates); - return res; -} - -bool SCFence::addFixesNonSC(action_list_t *list) { - bool added = false; - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - InferenceList *candidates = NULL; - ModelAction *act = *it; - - // Save the iterator of the read and the write - action_list_t::iterator readIter = it, writeIter; - if (act->get_seq_number() > 0) { - // Annotated reads will be ignored - if (scgen->getBadrfset()->contains(act) && - !scgen->getAnnotatedReadSet()->contains(act)) { - const ModelAction *write = act->get_reads_from(); - // Check reading old or future value - writeIter = std::find(list->begin(), - list->end(), write); - action_list_t::iterator findIt = std::find(list->begin(), - readIter, write); - bool readOldVal = findIt != readIter ? true : false; - - if (readOldVal) { // Pattern (a) read old value - FENCE_PRINT("Running through pattern (a)!\n"); - candidates = getFixesFromPatternA(list, readIter, writeIter); - // Add candidates pattern (a) - - added = addCandidates(candidates); - } else { // Pattern (b) read future value - // act->read, write->futureWrite - FENCE_PRINT("Running through pattern (b)!\n"); - candidates = getFixesFromPatternB(list, readIter, writeIter); - // Add candidates pattern (b) - added = addCandidates(candidates); - } - // Just eliminate the first cycle we see in the execution - break; - } - } - } - return added; -} - - -/** Return false to indicate there's no fixes for this execution. This can - * happen for specific reason such as it's a user-specified assertion failure */ -bool SCFence::addFixesBuggyExecution(action_list_t *list) { - InferenceList *candidates = new InferenceList; - bool foundFix = false; - bool added = false; - for (action_list_t::reverse_iterator rit = list->rbegin(); rit != - list->rend(); rit++) { - ModelAction *uninitRead = *rit; - if (uninitRead->get_seq_number() > 0) { - if (!uninitRead->is_read() || - !uninitRead->get_reads_from()->is_uninitialized()) - continue; - for (action_list_t::iterator it = list->begin(); it != - list->end(); it++) { - ModelAction *write = *it; - if (write->same_var(uninitRead)) { - // Now we can try to impose sync write hb-> uninitRead - paths_t *paths1 = get_rf_sb_paths(write, uninitRead); - if (paths1->size() > 0) { - FENCE_PRINT("Running through pattern (b') (unint read)!\n"); - print_rf_sb_paths(paths1, write, uninitRead); - imposeSync(candidates, paths1, write, uninitRead); - added = addCandidates(candidates); - if (added) { - foundFix = true; - break; - } - } - } - } - } - if (foundFix) - break; - } - - return added; -} - -/** Return false to indicate there's no implied mo for this execution. The idea - * is that it counts the number of reads in the middle of write1 and write2, if - * that number exceeds a specific number, then the analysis thinks that the - * program is stuck in an infinite loop because write1 does not establish proper - * synchronization with write2 such that the reads can read from write1 for - * ever. */ -bool SCFence::addFixesImplicitMO(action_list_t *list) { - bool added = false; - InferenceList *candidates = new InferenceList; - for (action_list_t::reverse_iterator rit2 = list->rbegin(); rit2 != - list->rend(); rit2++) { - ModelAction *write2 = *rit2; - if (!write2->is_write()) - continue; - action_list_t::reverse_iterator rit1 = rit2; - rit1++; - for (; rit1 != list->rend(); rit1++) { - ModelAction *write1 = *rit1; - if (!write1->is_write() || write1->get_location() != - write2->get_location()) - continue; - int readCnt = 0; - action_list_t::reverse_iterator ritRead = rit2; - ritRead++; - for (; ritRead != rit1; ritRead++) { - ModelAction *read = *ritRead; - if (!read->is_read() || read->get_location() != - write1->get_location()) - continue; - readCnt++; - } - if (readCnt > getImplicitMOReadBound()) { - // Found it, make write1 --hb-> write2 - bool isMO = execution->get_mo_graph()->checkReachable(write1, write2); - if (isMO) // Only impose mo when it doesn't have mo impsed - break; - FENCE_PRINT("Running through pattern (c) -- implicit mo!\n"); - FENCE_PRINT("Read count between the two writes: %d\n", readCnt); - FENCE_PRINT("implicitMOReadBound: %d\n", - getImplicitMOReadBound()); - ACT_PRINT(write1); - ACT_PRINT(write2); - paths_t *paths1 = get_rf_sb_paths(write1, write2); - if (paths1->size() > 0) { - FENCE_PRINT("From write1 to write2: \n"); - print_rf_sb_paths(paths1, write1, write2); - imposeSync(candidates, paths1, write1, write2); - // Add the candidates as potential results - added = addCandidates(candidates); - if (added) - return true; - } else { - FENCE_PRINT("Cannot establish hb between write1 & write2: \n"); - ACT_PRINT(write1); - ACT_PRINT(write2); - } - } - break; - } - } - return false; -} - -bool SCFence::checkDataRace(action_list_t *list, ModelAction **act1, - ModelAction **act2) { - - SnapList *opList = new SnapList; - /** Collect the operations per location */ - for (action_list_t::iterator iter = list->begin(); iter != list->end(); - iter++) { - ModelAction *act = *iter; - if (act->get_original_mo() != memory_order_normal) - continue; - bool foundIt = false; - for (SnapList::iterator listIter = opList->begin(); - listIter != opList->end(); listIter++) { - action_list_t *list = *listIter; - ModelAction *listAct = *(list->begin()); - if (listAct->get_location() != act->get_location()) - continue; - foundIt = true; - list->push_back(act); - } - if (!foundIt) { - action_list_t *newList = new action_list_t; - newList->push_back(act); - opList->push_back(newList); - } - } - - if (opList->size() == 0) - return false; - /** Now check if any two operations (same loc) establish hb */ - for (SnapList::iterator listIter = opList->begin(); - listIter != opList->end(); listIter++) { - action_list_t *list = *listIter; - action_list_t::iterator it1, it2; - for (it1 = list->begin(); it1 != list->end(); it1++) { - ModelAction *raceAct1 = *it1; - it2 = it1; - it2++; - for (; it2 != list->end(); it2++) { - ModelAction *raceAct2 = *it2; - if (!raceAct1->happens_before(raceAct2) && - !raceAct2->happens_before(raceAct1)) { - *act1 = raceAct1; - *act2 = raceAct2; - return true; - } - } - } - } - return false; -} - -ModelAction* SCFence::sbPrevAction(ModelAction *act) { - int idx = id_to_int(act->get_tid()); - // Retrieves the thread list of the action - action_list_t *list = &(*scgen->getDupThreadLists())[idx]; - action_list_t::iterator iter = std::find(list->begin(), - list->end(), act); - return *--iter; -} - -ModelAction* SCFence::sbNextAction(ModelAction *act) { - int idx = id_to_int(act->get_tid()); - // Retrieves the thread list of the action - action_list_t *list = &(*scgen->getDupThreadLists())[idx]; - action_list_t::iterator iter = std::find(list->begin(), - list->end(), act); - return *++iter; -} - -bool SCFence::addFixesDataRace(action_list_t *list) { - ModelAction *act1, *act2; - bool hasRace = checkDataRace(list, &act1, &act2); - if (hasRace) { - InferenceList *candidates1 = new InferenceList, - *candidates2 = new InferenceList; - paths_t *paths1, *paths2; - model_print("Fixing data race: \n"); - paths1 = get_rf_sb_paths(sbNextAction(act1), sbPrevAction(act2)); - paths2 = get_rf_sb_paths(sbNextAction(act2), sbPrevAction(act1)); - bool added = false; - if (paths1->size() > 0) { - model_print("paths1: \n"); - print_rf_sb_paths(paths1, act1, act2); - imposeSync(candidates1, paths1, act1, act2); - bool added = addCandidates(candidates1); - if (paths2->size() > 0) { - model_print("paths2: \n"); - print_rf_sb_paths(paths2, act2, act1); - imposeSync(candidates2, paths2, act2, act1); - added |= addCandidates(candidates2); - } - } - return added; - } - return false; -} - -bool SCFence::addFixes(action_list_t *list, fix_type_t type) { - // First check whether this is a later weakened inference - if (!getCurInference()->getShouldFix()) - return false; - bool added = false; - switch(type) { - case BUGGY_EXECUTION: - added = addFixesBuggyExecution(list); - break; - case IMPLICIT_MO: - added = addFixesImplicitMO(list); - break; - case NON_SC: - added = addFixesNonSC(list); - break; - case DATA_RACE: - added = addFixesDataRace(list); - break; - default: - break; - } - if (added && isBuggy()) { - // If this is a buggy inference and we have got fixes for it, set the - // falg - setHasFixes(true); - } - return added; -} - - -bool SCFence::routineBacktrack(bool feasible) { - model_print("Backtrack routine:\n"); - - /******** commitCurInference ********/ - Inference *curInfer = getCurInference(); - commitInference(curInfer, feasible); - if (feasible) { - if (!isBuggy()) { - model_print("Found one result!\n"); - } else if (!hasFixes()) { // Buggy and have no fixes - model_print("Found one buggy candidate!\n"); - } - curInfer->print(); - // Try to weaken this inference - if (weaken && !isBuggy()) { - getSet()->addWeakerInference(curInfer); - } - - } else { - if (curInfer->getShouldFix()) { - model_print("Reach an infeasible inference!\n"); - } else { - model_print("Get an unweakenable inference!\n"); - curInfer->print(true); - } - } - - /******** getNextInference ********/ - Inference *next = getNextInference(); - - if (next) { - /******** setCurInference ********/ - setCurInference(next); - /******** restartModelChecker ********/ - restartModelChecker(); - return true; - } else { - // Finish exploring the whole process - model_print("We are done with the whole process!\n"); - model_print("The results are as the following:\n"); - printResults(); - printCandidates(); - - /******** exitModelChecker ********/ - exitModelChecker(); - - return false; - } -} - -void SCFence::routineAfterAddFixes() { - model_print("Add fixes routine begin:\n"); - - /******** getNextInference ********/ - Inference *next = getNextInference(); - //ASSERT (next); - - if (next) { - /******** setCurInference ********/ - setCurInference(next); - /******** restartModelChecker ********/ - restartModelChecker(); - - model_print("Add fixes routine end:\n"); - model_print("Restart checking with the follwing inference:\n"); - getCurInference()->print(); - model_print("Checking...\n"); - } else { - routineBacktrack(false); - } -} - - - -/** This function finds all the paths that is a union of reads-from & - * sequence-before relationship between act1 & act2. */ -paths_t * SCFence::get_rf_sb_paths(const ModelAction *act1, const ModelAction *act2) { - int idx1 = id_to_int(act1->get_tid()), - idx2 = id_to_int(act2->get_tid()); - // Retrieves the two lists of actions of thread1 & thread2 - action_list_t *list1 = &(*dup_threadlists)[idx1], - *list2 = &(*dup_threadlists)[idx2]; - if (list1->size() == 0 || list2->size() == 0) { - return new paths_t(); - } - - // The container for all possible results - paths_t *paths = new paths_t(); - // A stack that records all current possible paths - paths_t *stack = new paths_t(); - path_t *path; - // Initialize the stack with loads sb-ordered before act2 - for (action_list_t::iterator it2 = list2->begin(); it2 != list2->end(); it2++) { - ModelAction *act = *it2; - // Add read action not sb after the act2 (including act2) - if (act->get_seq_number() > act2->get_seq_number()) - break; - if (!act->is_read()) - continue; - // Each start with a possible path - path = new path_t(); - path->push_front(act); - stack->push_back(path); - } - while (stack->size() > 0) { - path = stack->back(); - stack->pop_back(); - // The latest read in the temporary path - ModelAction *read = path->front(); - const ModelAction *write = read->get_reads_from(); - // If the read is uninitialized, don't do it - if (write->get_seq_number() == 0) { - delete path; - continue; - } - /** In case of cyclic sbUrf, make sure the write appears in a new thread - * or in an existing thread that is sequence-before the added read - * actions - */ - bool loop = false; - for (path_t::iterator p_it = path->begin(); p_it != path->end(); - p_it++) { - ModelAction *addedRead = *p_it; - if (id_to_int(write->get_tid()) == id_to_int(addedRead->get_tid())) { - // In the same thread - if (write->get_seq_number() >= addedRead->get_seq_number()) { - // Have a loop - delete path; - loop = true; - break; - } - } - } - // Not a useful rfUsb path (loop) - if (loop) { - continue; - } - - unsigned write_seqnum = write->get_seq_number(); - // We then check if we got a valid path - if (id_to_int(write->get_tid()) == idx1 && - write_seqnum >= act1->get_seq_number()) { - // Find a path - paths->push_back(path); - continue; - } - // Extend the path with the latest read - int idx = id_to_int(write->get_tid()); - action_list_t *list = &(*dup_threadlists)[idx]; - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - ModelAction *act = *it; - if (act->get_seq_number() > write_seqnum) // Could be RMW - break; - if (!act->is_read()) - continue; - path_t *new_path = new path_t(*path); - new_path->push_front(act); - stack->push_back(new_path); - } - delete path; - } - return paths; -} - -void SCFence::print_rf_sb_paths(paths_t *paths, const ModelAction *start, const ModelAction *end) { - FENCE_PRINT("Starting from:\n"); - ACT_PRINT(start); - FENCE_PRINT("\n"); - for (paths_t::iterator paths_i = paths->begin(); paths_i != - paths->end(); paths_i++) { - path_t *path = *paths_i; - FENCE_PRINT("Path %ld, size (%ld):\n", distance(paths->begin(), paths_i), - path->size()); - path_t::iterator it = path->begin(), i_next; - for (; it != path->end(); it++) { - i_next = it; - i_next++; - const ModelAction *read = *it, - *write = read->get_reads_from(), - *next_read = (i_next != path->end()) ? *i_next : NULL; - ACT_PRINT(write); - if (next_read == NULL || next_read->get_reads_from() != read) { - // Not the same RMW, also print the read operation - ACT_PRINT(read); - } - } - // Output a linebreak at the end of the path - FENCE_PRINT("\n"); - } - FENCE_PRINT("Ending with:\n"); - ACT_PRINT(end); -} - -/******************** SCFence-related Functions (End) ********************/ diff --git a/scfence/scfence.h b/scfence/scfence.h deleted file mode 100644 index e1e27a14..00000000 --- a/scfence/scfence.h +++ /dev/null @@ -1,412 +0,0 @@ -#ifndef _SCFENCE_H -#define _SCFENCE_H -#include "traceanalysis.h" -#include "scanalysis.h" -#include "hashtable.h" -#include "memoryorder.h" -#include "action.h" - -#include "wildcard.h" -#include "patch.h" -#include "inference.h" -#include "inferlist.h" -#include "inferset.h" - -#include "model.h" -#include "cyclegraph.h" -#include "scgen.h" - -#include - -#ifdef __cplusplus -using std::memory_order; -#endif - -#define DEFAULT_REPETITIVE_READ_BOUND 20 - -#define FENCE_OUTPUT - -#ifdef FENCE_OUTPUT - -#define FENCE_PRINT model_print - -#define ACT_PRINT(x) (x)->print() - -#define CV_PRINT(x) (x)->print() - -#define WILDCARD_ACT_PRINT(x)\ - FENCE_PRINT("Wildcard: %d\n", get_wildcard_id_zero((x)->get_original_mo()));\ - ACT_PRINT(x); - -#else - -#define FENCE_PRINT - -#define ACT_PRINT(x) - -#define CV_PRINT(x) - -#define WILDCARD_ACT_PRINT(x) - -#endif - -/* Forward declaration */ -class SCFence; -class Inference; -class InferenceList; -class PatchUnit; -class Patch; -class SCGenerator; - -extern SCFence *scfence; - -typedef action_list_t path_t; -/** A list of load operations can represent the union of reads-from & - * sequence-before edges; And we have a list of lists of load operations to - * represent all the possible rfUsb paths between two nodes, defined as - * syns_paths_t here - */ -typedef SnapList sync_paths_t; -typedef sync_paths_t paths_t; - -typedef struct scfence_priv { - scfence_priv() { - inferenceSet = new InferenceSet(); - curInference = new Inference(); - candidateFile = NULL; - inferImplicitMO = false; - hasRestarted = false; - implicitMOReadBound = DEFAULT_REPETITIVE_READ_BOUND; - timeout = 0; - gettimeofday(&lastRecordedTime, NULL); - } - - /** The set of the InferenceNode we maintain for exploring */ - InferenceSet *inferenceSet; - - /** The current inference */ - Inference *curInference; - - /** The file which provides a list of candidate wilcard inferences */ - char *candidateFile; - - /** Whether we consider the repetitive read to infer mo (_m) */ - bool inferImplicitMO; - - /** The bound above which we think that write should be the last write (_b) */ - int implicitMOReadBound; - - /** Whether we have restarted the model checker */ - bool hasRestarted; - - /** The amount of time (in second) set to force the analysis to backtrack */ - int timeout; - - /** The time we recorded last time */ - struct timeval lastRecordedTime; - - MEMALLOC -} scfence_priv; - -typedef enum fix_type { - BUGGY_EXECUTION, - IMPLICIT_MO, - NON_SC, - DATA_RACE -} fix_type_t; - - -class SCFence : public TraceAnalysis { - public: - SCFence(); - ~SCFence(); - virtual void setExecution(ModelExecution * execution); - virtual void analyze(action_list_t *); - virtual const char * name(); - virtual bool option(char *); - virtual void finish(); - - virtual void inspectModelAction(ModelAction *ac); - virtual void actionAtInstallation(); - virtual void actionAtModelCheckingFinish(); - - SNAPSHOTALLOC - - private: - /** The SC list generator */ - SCGenerator *scgen; - - struct sc_statistics *stats; - - bool time; - - /** Should we weaken the inferences later */ - bool weaken; - - /** Modification order graph */ - const CycleGraph *mo_graph; - - /** A duplica of the thread lists */ - SnapVector *dup_threadlists; - ModelExecution *execution; - - /** A set of actions that should be ignored in the partially SC analysis */ - HashTable ignoredActions; - int ignoredActionSize; - - /** The non-snapshotting private compound data structure that has the - * necessary stuff for the scfence analysis */ - static scfence_priv *priv; - - /** For the SC analysis */ - void update_stats(); - - /** Get the custom input number for implicit bound */ - int getImplicitMOBound(char *opt); - - /** Get the input file for initial parameter assignments */ - char* getInputFileName(char *opt); - - /** The function to parse the SCFence plugin options */ - bool parseOption(char *opt); - - /** Helper function for option parsing */ - char* parseOptionHelper(char *opt, int *optIdx); - - /** Initialize the search with a file with a list of potential candidates */ - void initializeByFile(); - - /** A pass through the original actions to extract the ignored actions - * (partially SC); it must be called after the threadlist has been built */ - void extractIgnoredActions(); - - /** Functions that work for infering the parameters by impsing - * synchronization */ - paths_t *get_rf_sb_paths(const ModelAction *act1, const ModelAction *act2); - - /** Printing function for those paths imposed by happens-before; only for - * the purpose of debugging */ - void print_rf_sb_paths(paths_t *paths, const ModelAction *start, const ModelAction *end); - - /** Whether there's an edge between from and to actions */ - bool isSCEdge(const ModelAction *from, const ModelAction *to) { - return from->is_seqcst() && to->is_seqcst(); - } - - bool isConflicting(const ModelAction *act1, const ModelAction *act2) { - return act1->get_location() == act2->get_location() ? (act1->is_write() - || act2->is_write()) : false; - } - - /** The two important routine when we find or cannot find a fix for the - * current inference */ - void routineAfterAddFixes(); - - bool routineBacktrack(bool feasible); - - /** A subroutine to find candidates for pattern (a) */ - InferenceList* getFixesFromPatternA(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter); - - /** A subroutine to find candidates for pattern (b) */ - InferenceList* getFixesFromPatternB(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter); - - /** Check if there exists data races, if so, overwrite act1 & act2 to be the - * two */ - bool checkDataRace(action_list_t *list, ModelAction **act1, - ModelAction **act2); - - /** Check if there exists data races, if so, generate the fixes */ - bool addFixesDataRace(action_list_t *list); - - /** The previous action in sb */ - ModelAction* sbPrevAction(ModelAction *act); - /** The next action in sb */ - ModelAction* sbNextAction(ModelAction *act); - - /** When getting a non-SC execution, find potential fixes and add it to the - * set */ - bool addFixesNonSC(action_list_t *list); - - /** When getting a buggy execution (we only target the uninitialized loads - * here), find potential fixes and add it to the set */ - bool addFixesBuggyExecution(action_list_t *list); - - /** When getting an SC and bug-free execution, we check whether we should - * fix the implicit mo problems. If so, find potential fixes and add it to - * the set */ - bool addFixesImplicitMO(action_list_t *list); - - /** General fixes wrapper */ - bool addFixes(action_list_t *list, fix_type_t type); - - /** Check whether a chosen reads-from path is a release sequence */ - bool isReleaseSequence(path_t *path); - - /** Impose synchronization to the existing list of inferences (inferList) - * according to path, begin is the beginning operation, and end is the - * ending operation. */ - bool imposeSync(InferenceList* inferList, paths_t *paths, const - ModelAction *begin, const ModelAction *end); - - bool imposeSync(InferenceList* inferList, path_t *path, const - ModelAction *begin, const ModelAction *end); - - /** For a specific pair of write and read actions, figure out the possible - * acq/rel fences that can impose hb plus the read & write sync pair */ - SnapVector* getAcqRel(const ModelAction *read, - const ModelAction *readBound, const ModelAction *write, - const ModelAction *writeBound); - - /** Impose SC to the existing list of inferences (inferList) by action1 & - * action2. */ - bool imposeSC(action_list_t * actions, InferenceList *inferList, const ModelAction *act1, - const ModelAction *act2); - - /** When we finish model checking or cannot further strenghen with the - * current inference, we commit the current inference (the node at the back - * of the set) to be explored, pop it out of the set; if it is feasible, - * we put it in the result list */ - void commitInference(Inference *infer, bool feasible) { - getSet()->commitInference(infer, feasible); - } - - /** Get the next available unexplored node; @Return NULL - * if we don't have next, meaning that we are done with exploring */ - Inference* getNextInference() { - return getSet()->getNextInference(); - } - - /** Add one possible node that represents a fix for the current inference; - * @Return true if the node to add has not been explored yet - */ - bool addInference(Inference *infer) { - return getSet()->addInference(infer); - } - - /** Add the list of fixes to the inference set. We will have to pass in the - * current inference.; - * @Return true if the node to add has not been explored yet - */ - bool addCandidates(InferenceList *candidates) { - return getSet()->addCandidates(getCurInference(), candidates); - } - - void addCurInference() { - getSet()->addCurInference(getCurInference()); - } - - /** Print the result of inferences */ - void printResults() { - getSet()->printResults(); - } - - /** Print the candidates of inferences */ - void printCandidates() { - getSet()->printCandidates(); - } - - /** The number of nodes in the set (including those parent nodes (set as - * explored) */ - int setSize() { - return getSet()->getCandidatesSize(); - } - - /** Set the restart flag of the model checker in order to restart the - * checking process */ - void restartModelChecker(); - - /** Set the exit flag of the model checker in order to exit the whole - * process */ - void exitModelChecker(); - - bool modelCheckerAtExitState(); - - const char* net_mo_str(memory_order order); - - InferenceSet* getSet() { - return priv->inferenceSet; - } - - void setHasFixes(bool val) { - getCurInference()->setHasFixes(val); - } - - bool hasFixes() { - return getCurInference()->getHasFixes(); - } - - bool isBuggy() { - return getCurInference()->getBuggy(); - } - - void setBuggy(bool val) { - getCurInference()->setBuggy(val); - } - - Inference* getCurInference() { - return priv->curInference; - } - - void setCurInference(Inference* infer) { - priv->curInference = infer; - } - - char* getCandidateFile() { - return priv->candidateFile; - } - - void setCandidateFile(char* file) { - priv->candidateFile = file; - } - - bool getInferImplicitMO() { - return priv->inferImplicitMO; - } - - void setInferImplicitMO(bool val) { - priv->inferImplicitMO = val; - } - - int getImplicitMOReadBound() { - return priv->implicitMOReadBound; - } - - void setImplicitMOReadBound(int bound) { - priv->implicitMOReadBound = bound; - } - - int getHasRestarted() { - return priv->hasRestarted; - } - - void setHasRestarted(int val) { - priv->hasRestarted = val; - } - - void setTimeout(int timeout) { - priv->timeout = timeout; - } - - int getTimeout() { - return priv->timeout; - } - - bool isTimeout() { - struct timeval now; - gettimeofday(&now, NULL); - // Check if it should be timeout - struct timeval *lastRecordedTime = &priv->lastRecordedTime; - unsigned long long elapsedTime = (now.tv_sec*1000000 + now.tv_usec) - - (lastRecordedTime->tv_sec*1000000 + lastRecordedTime->tv_usec); - - // Update the lastRecordedTime - priv->lastRecordedTime = now; - if (elapsedTime / 1000000.0 > priv->timeout) - return true; - else - return false; - } - - /********************** SCFence-related stuff (end) **********************/ -}; -#endif diff --git a/scfence/scgen.cc b/scfence/scgen.cc deleted file mode 100644 index cfcd0e5c..00000000 --- a/scfence/scgen.cc +++ /dev/null @@ -1,672 +0,0 @@ -#include "scgen.h" - -SCGenerator::SCGenerator() : - execution(NULL), - actions(NULL), - cvmap(), - cyclic(false), - badrfset(), - lastwrmap(), - threadlists(1), - dup_threadlists(1), - print_always(false), - print_buggy(false), - print_nonsc(false), - stats(new struct sc_statistics), - annotationMode(false) { -} - -SCGenerator::~SCGenerator() { -} - -bool SCGenerator::getCyclic() { - return cyclic || hasBadRF; -} - -SnapVector* SCGenerator::getDupThreadLists() { - return &dup_threadlists; -} - -struct sc_statistics* SCGenerator::getStats() { - return stats; -} - -void SCGenerator::setExecution(ModelExecution *execution) { - this->execution = execution; -} - -void SCGenerator::setActions(action_list_t *actions) { - this->actions = actions; -} - -void SCGenerator::setPrintAlways(bool val) { - this->print_always = val; -} - -bool SCGenerator::getPrintAlways() { - return this->print_always; -} - -bool SCGenerator::getHasBadRF() { - return this->hasBadRF; -} - -void SCGenerator::setPrintBuggy(bool val) { - this->print_buggy = val; -} - -void SCGenerator::setPrintNonSC(bool val) { - this->print_nonsc = val; -} - -void SCGenerator::setAnnotationMode(bool val) { - this->annotationMode = val; -} - -action_list_t * SCGenerator::getSCList() { - struct timeval start; - struct timeval finish; - gettimeofday(&start, NULL); - - /* Build up the thread lists for general purpose */ - int thrdNum; - buildVectors(&dup_threadlists, &thrdNum, actions); - - fastVersion = true; - action_list_t *list = generateSC(actions); - if (cyclic) { - reset(actions); - delete list; - fastVersion = false; - list = generateSC(actions); - } - check_rf(list); - gettimeofday(&finish, NULL); - stats->elapsedtime+=((finish.tv_sec*1000000+finish.tv_usec)-(start.tv_sec*1000000+start.tv_usec)); - update_stats(); - return list; -} - -HashTable * SCGenerator::getBadrfset() { - return &badrfset; -} - -HashTable * SCGenerator::getAnnotatedReadSet() { - return &annotatedReadSet; -} - -void SCGenerator::print_list(action_list_t *list) { - model_print("---------------------------------------------------------------------\n"); - if (cyclic || hasBadRF) - model_print("Not SC\n"); - unsigned int hash = 0; - - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - const ModelAction *act = *it; - if (act->get_seq_number() > 0) { - 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()); - } - model_print("HASH %u\n", hash); - model_print("---------------------------------------------------------------------\n"); -} - - -action_list_t * SCGenerator::generateSC(action_list_t *list) { - int numactions=buildVectors(&threadlists, &maxthreads, list); - stats->actions+=numactions; - - // Analyze which actions we should ignore in the partially SC analysis - if (annotationMode) { - collectAnnotatedReads(); - if (annotationError) { - model_print("Annotation error!\n"); - return NULL; - } - } - - computeCV(list); - - action_list_t *sclist = new action_list_t(); - ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *)); - int * choices = (int *) model_calloc(1, sizeof(int)*numactions); - int endchoice = 0; - int currchoice = 0; - int lastchoice = -1; - while (true) { - int numActions = getNextActions(array); - if (numActions == 0) - break; - ModelAction * act=pruneArray(array, numActions); - if (act == NULL) { - if (currchoice < endchoice) { - act = array[choices[currchoice]]; - //check whether there is still another option - if ((choices[currchoice]+1)1) - lastchoice=currchoice; - currchoice++; - } - } - 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 - bool prevc=cyclic; - computeCV(list); - if (!prevc && cyclic) { - model_print("ROLLBACK in SC\n"); - //check whether we have another choice - if (lastchoice != -1) { - //have to reset everything - choices[lastchoice]++; - endchoice=lastchoice+1; - currchoice=0; - lastchoice=-1; - - reset(list); - buildVectors(&threadlists, &maxthreads, list); - computeCV(list); - sclist->clear(); - continue; - - } - } - } - //add action to end - sclist->push_back(act); - } - model_free(array); - return sclist; -} - -void SCGenerator::update_stats() { - if (cyclic) { - stats->nonsccount++; - } else { - stats->sccount++; - } -} - -int SCGenerator::buildVectors(SnapVector *threadlist, int *maxthread, - action_list_t *list) { - *maxthread = 0; - int numactions = 0; - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - ModelAction *act = *it; - numactions++; - int threadid = id_to_int(act->get_tid()); - if (threadid > *maxthread) { - threadlist->resize(threadid + 1); - *maxthread = threadid; - } - (*threadlist)[threadid].push_back(act); - } - return numactions; -} - - -bool SCGenerator::updateConstraints(ModelAction *act) { - bool changed = false; - 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 - merge(writecv, write, act); - changed = true; - break; - } - } - } - return changed; -} - -void SCGenerator::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; - bool updateFuture = 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 = execution->get_thread(act)->get_creation(); - last_act[id_to_int(act->get_tid())] = act; - ClockVector *cv = cvmap.get(act); - if (cv == NULL) { - cv = new ClockVector(act->get_cv(), act); - cvmap.put(act, cv); - } - - 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()); - changed |= merge(cv, act, finish); - } - if (act->is_read()) { - if (fastVersion) { - changed |= processReadFast(act, cv); - } else if (annotatedReadSet.contains(act)) { - changed |= processAnnotatedReadSlow(act, cv, &updateFuture); - } else { - changed |= processReadSlow(act, cv, &updateFuture); - } - } - } - /* Reset the last action array */ - if (changed) { - bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *)); - } else { - if (!fastVersion) { - if (!allowNonSC) { - allowNonSC = true; - changed = true; - } else { - break; - } - } - } - } - model_free(last_act); -} - -bool SCGenerator::processReadFast(ModelAction *read, ClockVector *cv) { - bool changed = false; - - /* Merge in the clock vector from the write */ - const ModelAction *write = read->get_reads_from(); - if (!write) { // The case where the write is a promise - return false; - } - ClockVector *writecv = cvmap.get(write); - changed |= merge(cv, read, write) && (*read < *write); - - for (int i = 0; i <= maxthreads; i++) { - thread_id_t tid = int_to_id(i); - action_list_t *list = execution->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; - if (write2 == write) - continue; - if (write2 == read) // If read is a RMW - continue; - - ClockVector *write2cv = cvmap.get(write2); - if (write2cv == NULL) - continue; - /* write -sc-> write2 && - write -rf-> R => - R -sc-> write2 */ - if (write2cv->synchronized_since(write)) { - changed |= merge(write2cv, write2, read); - - } - - //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 || merge(writecv, write, write2); - break; - } - } - } - return changed; -} - -bool SCGenerator::processReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture) { - bool changed = false; - - /* Merge in the clock vector from the write */ - const ModelAction *write = read->get_reads_from(); - ClockVector *writecv = cvmap.get(write); - if ((*write < *read) || ! *updateFuture) { - bool status = merge(cv, read, write) && (*read < *write); - changed |= status; - *updateFuture = status; - } - - for (int i = 0; i <= maxthreads; i++) { - thread_id_t tid = int_to_id(i); - action_list_t *list = execution->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; - if (write2 == write) - continue; - if (write2 == read) // If read is a RMW - continue; - - ClockVector *write2cv = cvmap.get(write2); - if (write2cv == NULL) - continue; - - /* write -sc-> write2 && - write -rf-> R => - R -sc-> write2 */ - if (write2cv->synchronized_since(write)) { - if ((*read < *write2) || ! *updateFuture) { - bool status = merge(write2cv, write2, read); - changed |= status; - *updateFuture |= status && (*write2 < *read); - } - } - - //looking for earliest write2 in iteration to satisfy this - /* write2 -sc-> R && - write -rf-> R => - write2 -sc-> write */ - if (cv->synchronized_since(write2)) { - if ((*write2 < *write) || ! *updateFuture) { - bool status = writecv == NULL || merge(writecv, write, write2); - changed |= status; - *updateFuture |= status && (*write < *write2); - } - break; - } - } - } - return changed; -} - -bool SCGenerator::processAnnotatedReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture) { - bool changed = false; - - /* Merge in the clock vector from the write */ - const ModelAction *write = read->get_reads_from(); - if ((*write < *read) || ! *updateFuture) { - bool status = merge(cv, read, write) && (*read < *write); - changed |= status; - *updateFuture = status; - } - return changed; -} - -int SCGenerator::getNextActions(ModelAction **array) { - int count=0; - - for (int t = 0; t <= maxthreads; t++) { - action_list_t *tlt = &threadlists[t]; - if (tlt->empty()) - continue; - ModelAction *act = tlt->front(); - ClockVector *cv = cvmap.get(act); - - /* Find the earliest in SC ordering */ - for (int i = 0; i <= maxthreads; i++) { - if ( i == t ) - continue; - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - if (cv->synchronized_since(first)) { - act = NULL; - break; - } - } - if (act != NULL) { - array[count++]=act; - } - } - if (count != 0) - return count; - for (int t = 0; t <= maxthreads; t++) { - action_list_t *tlt = &threadlists[t]; - if (tlt->empty()) - continue; - ModelAction *act = tlt->front(); - ClockVector *cv = act->get_cv(); - - /* Find the earliest in SC ordering */ - for (int i = 0; i <= maxthreads; i++) { - if ( i == t ) - continue; - action_list_t *threadlist = &threadlists[i]; - if (threadlist->empty()) - continue; - ModelAction *first = threadlist->front(); - if (cv->synchronized_since(first)) { - act = NULL; - break; - } - } - if (act != NULL) { - array[count++]=act; - } - } - - ASSERT(count==0 || cyclic); - - return count; -} - -bool SCGenerator::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) { - cyclic = true; - //refuse to introduce cycles into clock vectors - return false; - } - if (fastVersion) { - bool status = cv->merge(cv2); - return status; - } else { - bool merged; - if (allowNonSC) { - merged = cv->merge(cv2); - if (merged) - allowNonSC = false; - return merged; - } else { - if (act2->happens_before(act) || - (act->is_seqcst() && act2->is_seqcst() && *act2 < *act)) { - return cv->merge(cv2); - } else { - return false; - } - } - } - -} - -void SCGenerator::check_rf1(action_list_t *list) { - bool hasBadRF1 = false; - HashTable badrfset1; - HashTable lastwrmap1; - 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() != lastwrmap1.get(act->get_location())) { - badrfset1.put(act, lastwrmap1.get(act->get_location())); - hasBadRF1 = true; - } - } - if (act->is_write()) - lastwrmap1.put(act->get_location(), act); - } - if (cyclic != hasBadRF1 && !annotationMode) { - if (cyclic) - model_print("Assert failure & non-SC\n"); - else - model_print("Assert failure & SC\n"); - if (fastVersion) { - model_print("Fast\n"); - } else { - model_print("Slow\n"); - } - print_list(list); - } - if (!annotationMode) { - ASSERT (cyclic == hasBadRF1); - } -} - -void SCGenerator::check_rf(action_list_t *list) { - hasBadRF = false; - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - const ModelAction *act = *it; - if (act->is_read()) { - const ModelAction *write = act->get_reads_from(); - if (write && write != lastwrmap.get(act->get_location())) { - badrfset.put(act, lastwrmap.get(act->get_location())); - hasBadRF = true; - } - } - if (act->is_write()) - lastwrmap.put(act->get_location(), act); - } - if (cyclic != hasBadRF && !annotationMode) { - if (cyclic) - model_print("Assert failure & non-SC\n"); - else - model_print("Assert failure & SC\n"); - if (fastVersion) { - model_print("Fast\n"); - } else { - model_print("Slow\n"); - } - print_list(list); - } - if (!annotationMode) { - ASSERT (cyclic == hasBadRF); - } -} - -void SCGenerator::reset(action_list_t *list) { - for (int t = 0; t <= maxthreads; t++) { - action_list_t *tlt = &threadlists[t]; - tlt->clear(); - } - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - ModelAction *act = *it; - delete cvmap.get(act); - cvmap.put(act, NULL); - } - - cyclic=false; -} - -ModelAction* SCGenerator::pruneArray(ModelAction **array, int count) { - /* No choice */ - if (count == 1) - return array[0]; - - /* Choose first non-write action */ - ModelAction *nonwrite=NULL; - for(int i=0;iis_write()) - if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number()) - nonwrite = array[i]; - } - if (nonwrite != NULL) - return nonwrite; - - /* Look for non-conflicting action */ - ModelAction *nonconflict=NULL; - for(int a=0;aget_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 - act = NULL; - break; - } - } - } - if (act != NULL) { - if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number()) - nonconflict=act; - } - } - return nonconflict; -} - -/** This routine is operated based on the built threadlists */ -void SCGenerator::collectAnnotatedReads() { - for (unsigned i = 1; i < threadlists.size(); i++) { - action_list_t *list = &threadlists.at(i); - for (action_list_t::iterator it = list->begin(); it != list->end(); it++) { - ModelAction *act = *it; - if (!IS_SC_ANNO(act)) - continue; - if (!IS_ANNO_BEGIN(act)) { - model_print("SC annotation should begin with a BEGIN annotation\n"); - annotationError = true; - return; - } - act = *++it; - while (!IS_ANNO_END(act) && it != list->end()) { - // Look for the actions to keep in this loop - ModelAction *nextAct = *++it; - if (!IS_ANNO_KEEP(nextAct)) { // Annotated reads - act->print(); - annotatedReadSet.put(act, act); - annotatedReadSetSize++; - if (IS_ANNO_END(nextAct)) - break; - } - } - if (it == list->end()) { - model_print("SC annotation should end with a END annotation\n"); - annotationError = true; - return; - } - } - } -} diff --git a/scfence/scgen.h b/scfence/scgen.h deleted file mode 100644 index a16e6b09..00000000 --- a/scfence/scgen.h +++ /dev/null @@ -1,119 +0,0 @@ -#ifndef _SCGEN_H -#define _SCGEN_H - -#include "hashtable.h" -#include "memoryorder.h" -#include "action.h" -#include "scanalysis.h" -#include "model.h" -#include "execution.h" -#include "threads-model.h" -#include "clockvector.h" -#include "sc_annotation.h" - -#include - -typedef struct SCGeneratorOption { - bool print_always; - bool print_buggy; - bool print_nonsc; - bool annotationMode; -} SCGeneratorOption; - - -class SCGenerator { -public: - SCGenerator(); - ~SCGenerator(); - - bool getCyclic(); - SnapVector* getDupThreadLists(); - - struct sc_statistics* getStats(); - - void setExecution(ModelExecution *execution); - void setActions(action_list_t *actions); - void setPrintAlways(bool val); - bool getPrintAlways(); - bool getHasBadRF(); - - void setAnnotationMode(bool val); - - void setPrintBuggy(bool val); - - void setPrintNonSC(bool val); - - action_list_t * getSCList(); - - HashTable *getBadrfset(); - - HashTable *getAnnotatedReadSet(); - - void print_list(action_list_t *list); - - SNAPSHOTALLOC -private: - /********************** SC-related stuff (beginning) **********************/ - ModelExecution *execution; - - action_list_t *actions; - - bool fastVersion; - bool allowNonSC; - - action_list_t * generateSC(action_list_t *list); - - void update_stats(); - - int buildVectors(SnapVector *threadlist, int *maxthread, - action_list_t *list); - - bool updateConstraints(ModelAction *act); - - void computeCV(action_list_t *list); - - bool processReadFast(ModelAction *read, ClockVector *cv); - - bool processReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture); - - bool processAnnotatedReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture); - - int getNextActions(ModelAction **array); - - bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2); - - void check_rf(action_list_t *list); - void check_rf1(action_list_t *list); - - void reset(action_list_t *list); - - ModelAction* pruneArray(ModelAction **array, int count); - - /** This routine is operated based on the built threadlists */ - void collectAnnotatedReads(); - - int maxthreads; - HashTable cvmap; - bool cyclic; - HashTable badrfset; - HashTable lastwrmap; - SnapVector threadlists; - SnapVector dup_threadlists; - bool print_always; - bool print_buggy; - bool print_nonsc; - bool hasBadRF; - - struct sc_statistics *stats; - - /** The set of read actions that are annotated to be special and will - * receive special treatment */ - HashTable annotatedReadSet; - int annotatedReadSetSize; - bool annotationMode; - bool annotationError; - - /** A set of actions that should be ignored in the partially SC analysis */ - HashTable ignoredActions; -}; -#endif -- 2.34.1