From a65e234b607444355eb6e34097ee55ba93d4c01b Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 4 Aug 2015 11:22:44 -0700 Subject: [PATCH 1/1] Add SCFence analysis --- Makefile | 17 +- action.cc | 4 +- action.h | 5 + execution.h | 2 + include/wildcard.h | 36 ++ main.cc | 2 + model.cc | 57 +- model.h | 24 +- nodestack.cc | 10 + nodestack.h | 1 + plugins.cc | 2 + 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 ++++ traceanalysis.h | 15 + 27 files changed, 4135 insertions(+), 12 deletions(-) create mode 100644 include/wildcard.h create mode 100644 scfence/Makefile create mode 100644 scfence/fence_common.h create mode 100644 scfence/inference.cc create mode 100644 scfence/inference.h create mode 100644 scfence/inferlist.cc create mode 100644 scfence/inferlist.h create mode 100644 scfence/inferset.cc create mode 100644 scfence/inferset.h create mode 100644 scfence/patch.cc create mode 100644 scfence/patch.h create mode 100644 scfence/sc_annotation.h create mode 100644 scfence/scfence.cc create mode 100644 scfence/scfence.h create mode 100644 scfence/scgen.cc create mode 100644 scfence/scgen.h diff --git a/Makefile b/Makefile index f44a895..eb84076 100644 --- a/Makefile +++ b/Makefile @@ -1,12 +1,14 @@ 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 -CPPFLAGS += -Iinclude -I. +CPPFLAGS += -Iinclude -I. -I$(SCFENCE_DIR) LDFLAGS := -ldl -lrt -rdynamic SHARED := -shared @@ -32,15 +34,20 @@ docs: *.c *.cc *.h README.html README.html: README.md $(MARKDOWN) $< > $@ -$(LIB_SO): $(OBJECTS) - $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) malloc.o: malloc.c $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable -%.o: %.cc +%.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) + %.pdf: %.dot dot -Tpdf $< -o $@ @@ -48,7 +55,7 @@ malloc.o: malloc.c PHONY += clean clean: - rm -f *.o *.so .*.d *.pdf *.dot + rm -f *.o *.so .*.d *.pdf *.dot $(SCFENCE_DIR)/.*.d $(SCFENCE_DIR)/*.o $(MAKE) -C $(TESTS_DIR) clean PHONY += mrclean diff --git a/action.cc b/action.cc index 2010a0b..876de12 100644 --- a/action.cc +++ b/action.cc @@ -9,6 +9,7 @@ #include "common.h" #include "threads-model.h" #include "nodestack.h" +#include "wildcard.h" #define ACTION_INITIAL_CLOCK 0 @@ -34,6 +35,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, Thread *thread) : type(type), order(order), + original_order(order), location(loc), value(value), reads_from(NULL), @@ -553,7 +555,7 @@ const char * ModelAction::get_type_str() const case ATOMIC_WAIT: return "wait"; case ATOMIC_NOTIFY_ONE: return "notify one"; case ATOMIC_NOTIFY_ALL: return "notify all"; - case ATOMIC_ANNOTATION: return "atomic annotation"; + case ATOMIC_ANNOTATION: return "annotation"; default: return "unknown type"; }; } diff --git a/action.h b/action.h index ad3b828..c8ad85b 100644 --- a/action.h +++ b/action.h @@ -96,6 +96,8 @@ public: thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } memory_order get_mo() const { return order; } + memory_order get_original_mo() const { return original_order; } + void set_mo(memory_order order) { this->order = order; } void * get_location() const { return location; } modelclock_t get_seq_number() const { return seq_number; } uint64_t get_value() const { return value; } @@ -194,6 +196,9 @@ private: /** @brief The memory order for this operation. */ memory_order order; + /** @brief The original memory order parameter for this operation. */ + memory_order original_order; + /** @brief A pointer to the memory location for this action. */ void *location; diff --git a/execution.h b/execution.h index 3635657..9322f55 100644 --- a/execution.h +++ b/execution.h @@ -116,6 +116,8 @@ public: action_list_t * get_action_trace() { return &action_trace; } + CycleGraph * const get_mo_graph() { return mo_graph; } + SNAPSHOTALLOC private: int get_execution_number() const; diff --git a/include/wildcard.h b/include/wildcard.h new file mode 100644 index 0000000..2a18c4c --- /dev/null +++ b/include/wildcard.h @@ -0,0 +1,36 @@ +#ifndef _WILDCARD_H +#define _WILDCARD_H +#include "memoryorder.h" + +#define MAX_WILDCARD_NUM 50 + +#define memory_order_normal ((memory_order) (0x2000)) + +#define memory_order_wildcard(x) ((memory_order) (0x1000+x)) + +#define wildcard(x) ((memory_order) (0x1000+x)) +#define get_wildcard_id(x) ((int) (x-0x1000)) +#define get_wildcard_id_zero(x) ((get_wildcard_id(x)) > 0 ? get_wildcard_id(x) : 0) + +#define INIT_WILDCARD_NUM 20 +#define WILDCARD_NONEXIST (memory_order) -1 +#define INFERENCE_INCOMPARABLE(x) (!(-1 <= (x) <= 1)) + +#define is_wildcard(x) (!(x >= memory_order_relaxed && x <= memory_order_seq_cst) && x != memory_order_normal) +#define is_normal_mo_infer(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == WILDCARD_NONEXIST || x == memory_order_normal) +#define is_normal_mo(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == memory_order_normal) + +#define assert_infer(x) for (int i = 0; i <= wildcardNum; i++)\ + ASSERT(is_normal_mo_infer((x[i]))); + +#define assert_infers(x) for (ModelList::iterator iter =\ + (x)->begin(); iter != (x)->end(); iter++)\ + assert_infer((*iter)); + +#define relaxed memory_order_relaxed +#define release memory_order_release +#define acquire memory_order_acquire +#define seqcst memory_order_seq_cst +#define acqrel memory_order_acq_rel + +#endif diff --git a/main.cc b/main.cc index c93c5e9..0d1fa1c 100644 --- a/main.cc +++ b/main.cc @@ -231,6 +231,8 @@ static void install_trace_analyses(ModelExecution *execution) TraceAnalysis * ta=(*installedanalysis)[i]; ta->setExecution(execution); model->add_trace_analysis(ta); + /** Call the installation event for each installed plugin */ + ta->actionAtInstallation(); } } diff --git a/model.cc b/model.cc index 72a8d13..3bac903 100644 --- a/model.cc +++ b/model.cc @@ -23,13 +23,16 @@ ModelChecker *model; ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ params(params), + restart_flag(false), + exit_flag(false), scheduler(new Scheduler()), node_stack(new NodeStack()), execution(new ModelExecution(this, &this->params, scheduler, node_stack)), execution_number(1), diverge(NULL), earliest_diverge(NULL), - trace_analyses() + trace_analyses(), + inspect_plugin(NULL) { memset(&stats,0,sizeof(struct execution_stats)); } @@ -300,6 +303,9 @@ bool ModelChecker::next_execution() checkDataRaces(); run_trace_analyses(); + } else if (inspect_plugin && !execution->is_complete_execution() && + (execution->too_many_steps())) { + inspect_plugin->analyze(execution->get_action_trace()); } record_stats(); @@ -313,6 +319,14 @@ bool ModelChecker::next_execution() if (complete) earliest_diverge = NULL; + if (restart_flag) { + do_restart(); + return true; + } + + if (exit_flag) + return false; + if ((diverge = execution->get_next_backtrack()) == NULL) return false; @@ -386,6 +400,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) Thread *old = thread_current(); scheduler->set_current_thread(NULL); ASSERT(!old->get_pending()); + if (inspect_plugin != NULL) { + inspect_plugin->inspectModelAction(act); + } old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); @@ -415,9 +432,35 @@ bool ModelChecker::should_terminate_execution() return false; } +/** @brief Exit ModelChecker upon returning to the run loop of the + * model checker. */ +void ModelChecker::exit_model_checker() +{ + exit_flag = true; +} + +/** @brief Restart ModelChecker upon returning to the run loop of the + * model checker. */ +void ModelChecker::restart() +{ + restart_flag = true; +} + +void ModelChecker::do_restart() +{ + restart_flag = false; + diverge = NULL; + earliest_diverge = NULL; + reset_to_initial_state(); + node_stack->full_reset(); + memset(&stats,0,sizeof(struct execution_stats)); + execution_number = 1; +} + /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { + bool has_next; do { thrd_t user_thread; Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); @@ -465,7 +508,17 @@ void ModelChecker::run() t = execution->take_step(curr); } while (!should_terminate_execution()); - } while (next_execution()); + has_next = next_execution(); + if (inspect_plugin != NULL && !has_next) { + inspect_plugin->actionAtModelCheckingFinish(); + // Check if the inpect plugin set the restart flag + if (restart_flag) { + model_print("******* Model-checking RESTART: *******\n"); + has_next = true; + do_restart(); + } + } + } while (has_next); execution->fixup_release_sequences(); diff --git a/model.h b/model.h index 74cb4e1..9448353 100644 --- a/model.h +++ b/model.h @@ -47,6 +47,15 @@ public: void run(); + /** Restart the model checker, intended for pluggins. */ + void restart(); + + /** Exit the model checker, intended for pluggins. */ + void exit_model_checker(); + + /** Check the exit_flag. */ + bool get_exit_flag() const { return exit_flag; } + /** @returns the context for the main model-checking system thread */ ucontext_t * get_system_context() { return &system_context; } @@ -66,12 +75,15 @@ public: void assert_user_bug(const char *msg); const model_params params; - void add_trace_analysis(TraceAnalysis *a) { - trace_analyses.push_back(a); - } - + void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } + void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } MEMALLOC private: + /** Flag indicates whether to restart the model checker. */ + bool restart_flag; + /** Flag indicates whether to exit the model checker. */ + bool exit_flag; + /** The scheduler to use: tracks the running/ready Threads */ Scheduler * const scheduler; NodeStack * const node_stack; @@ -97,6 +109,10 @@ private: ModelVector trace_analyses; + /** @bref Implement restart. */ + void do_restart(); + /** @bref Plugin that can inspect new actions. */ + TraceAnalysis *inspect_plugin; /** @brief The cumulative execution stats */ struct execution_stats stats; void record_stats(); diff --git a/nodestack.cc b/nodestack.cc index e5f4687..bacd067 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -838,6 +838,16 @@ void NodeStack::pop_restofstack(int numAhead) node_list.back()->clear_backtracking(); } +/** Reset the node stack. */ +void NodeStack::full_reset() +{ + for (unsigned int i = 0; i < node_list.size(); i++) + delete node_list[i]; + node_list.clear(); + reset_execution(); + total_nodes = 1; +} + Node * NodeStack::get_head() const { if (node_list.empty() || head_idx < 0) diff --git a/nodestack.h b/nodestack.h index f26100b..6ae96be 100644 --- a/nodestack.h +++ b/nodestack.h @@ -198,6 +198,7 @@ public: Node * get_next() const; void reset_execution(); void pop_restofstack(int numAhead); + void full_reset(); int get_total_nodes() { return total_nodes; } void print() const; diff --git a/plugins.cc b/plugins.cc index b1d3cfb..38493de 100644 --- a/plugins.cc +++ b/plugins.cc @@ -1,5 +1,6 @@ #include "plugins.h" #include "scanalysis.h" +#include "scfence.h" ModelVector * registered_analysis; ModelVector * installed_analysis; @@ -8,6 +9,7 @@ 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/scfence/Makefile b/scfence/Makefile new file mode 100644 index 0000000..d0cc313 --- /dev/null +++ b/scfence/Makefile @@ -0,0 +1,11 @@ +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 new file mode 100644 index 0000000..014cce1 --- /dev/null +++ b/scfence/fence_common.h @@ -0,0 +1,35 @@ +#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 new file mode 100644 index 0000000..e2d2152 --- /dev/null +++ b/scfence/inference.cc @@ -0,0 +1,378 @@ +#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 new file mode 100644 index 0000000..2d61e59 --- /dev/null +++ b/scfence/inference.h @@ -0,0 +1,154 @@ +#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 new file mode 100644 index 0000000..5cb6326 --- /dev/null +++ b/scfence/inferlist.cc @@ -0,0 +1,207 @@ +#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 new file mode 100644 index 0000000..bc3476a --- /dev/null +++ b/scfence/inferlist.h @@ -0,0 +1,64 @@ +#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 new file mode 100644 index 0000000..7eeb003 --- /dev/null +++ b/scfence/inferset.cc @@ -0,0 +1,300 @@ +#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 new file mode 100644 index 0000000..965d2f9 --- /dev/null +++ b/scfence/inferset.h @@ -0,0 +1,147 @@ +#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 new file mode 100644 index 0000000..3fabe01 --- /dev/null +++ b/scfence/patch.cc @@ -0,0 +1,69 @@ +#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 new file mode 100644 index 0000000..d25bed1 --- /dev/null +++ b/scfence/patch.h @@ -0,0 +1,59 @@ +#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 new file mode 100644 index 0000000..1f37107 --- /dev/null +++ b/scfence/sc_annotation.h @@ -0,0 +1,47 @@ +#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 new file mode 100644 index 0000000..63408cb --- /dev/null +++ b/scfence/scfence.cc @@ -0,0 +1,1298 @@ +#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 = "SCFENCE"; + 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 new file mode 100644 index 0000000..e1e27a1 --- /dev/null +++ b/scfence/scfence.h @@ -0,0 +1,412 @@ +#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 new file mode 100644 index 0000000..cfcd0e5 --- /dev/null +++ b/scfence/scgen.cc @@ -0,0 +1,672 @@ +#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 new file mode 100644 index 0000000..a16e6b0 --- /dev/null +++ b/scfence/scgen.h @@ -0,0 +1,119 @@ +#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 diff --git a/traceanalysis.h b/traceanalysis.h index df3356a..d363150 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -2,6 +2,7 @@ #define TRACE_ANALYSIS_H #include "model.h" + class TraceAnalysis { public: /** setExecution is called once after installation with a reference to @@ -30,6 +31,20 @@ class TraceAnalysis { virtual void finish() = 0; + /** This method is used to inspect the normal/abnormal model + * action. */ + virtual void inspectModelAction(ModelAction *act) {} + + /** This method will be called by when a plugin is installed by the + * model checker. */ + virtual void actionAtInstallation() {} + + /** This method will be called when the model checker finishes the + * executions; With this method, the model checker can alter the + * state of the plugin and then the plugin can choose whether or not + * restart the model checker. */ + virtual void actionAtModelCheckingFinish() {} + SNAPSHOTALLOC }; #endif -- 2.34.1