Add SCFence analysis oopsla2015
authorbdemsky <bdemsky@uci.edu>
Tue, 4 Aug 2015 18:22:44 +0000 (11:22 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 2 Sep 2015 17:02:51 +0000 (10:02 -0700)
27 files changed:
Makefile
action.cc
action.h
execution.h
include/wildcard.h [new file with mode: 0644]
main.cc
model.cc
model.h
nodestack.cc
nodestack.h
plugins.cc
scfence/Makefile [new file with mode: 0644]
scfence/fence_common.h [new file with mode: 0644]
scfence/inference.cc [new file with mode: 0644]
scfence/inference.h [new file with mode: 0644]
scfence/inferlist.cc [new file with mode: 0644]
scfence/inferlist.h [new file with mode: 0644]
scfence/inferset.cc [new file with mode: 0644]
scfence/inferset.h [new file with mode: 0644]
scfence/patch.cc [new file with mode: 0644]
scfence/patch.h [new file with mode: 0644]
scfence/sc_annotation.h [new file with mode: 0644]
scfence/scfence.cc [new file with mode: 0644]
scfence/scfence.h [new file with mode: 0644]
scfence/scgen.cc [new file with mode: 0644]
scfence/scgen.h [new file with mode: 0644]
traceanalysis.h

index f44a895..eb84076 100644 (file)
--- 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
index 2010a0b..876de12 100644 (file)
--- 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";
        };
 }
index ad3b828..c8ad85b 100644 (file)
--- 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;
 
index 3635657..9322f55 100644 (file)
@@ -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 (file)
index 0000000..2a18c4c
--- /dev/null
@@ -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<memory_order *>::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 (file)
--- 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();
        }
 }
 
index 72a8d13..3bac903 100644 (file)
--- 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 (file)
--- 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<TraceAnalysis *> 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();
index e5f4687..bacd067 100644 (file)
@@ -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)
index f26100b..6ae96be 100644 (file)
@@ -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;
index b1d3cfb..38493de 100644 (file)
@@ -1,5 +1,6 @@
 #include "plugins.h"
 #include "scanalysis.h"
+#include "scfence.h"
 
 ModelVector<TraceAnalysis *> * registered_analysis;
 ModelVector<TraceAnalysis *> * installed_analysis;
@@ -8,6 +9,7 @@ void register_plugins() {
        registered_analysis=new ModelVector<TraceAnalysis *>();
        installed_analysis=new ModelVector<TraceAnalysis *>();
        registered_analysis->push_back(new SCAnalysis());
+       registered_analysis->push_back(new SCFence());
 }
 
 ModelVector<TraceAnalysis *> * getRegisteredTraceAnalysis() {
diff --git a/scfence/Makefile b/scfence/Makefile
new file mode 100644 (file)
index 0000000..d0cc313
--- /dev/null
@@ -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 (file)
index 0000000..014cce1
--- /dev/null
@@ -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 (file)
index 0000000..e2d2152
--- /dev/null
@@ -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<int> *strengthened = new SnapVector<int>;
+       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<int> *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 (file)
index 0000000..2d61e59
--- /dev/null
@@ -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<int> *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 (file)
index 0000000..5cb6326
--- /dev/null
@@ -0,0 +1,207 @@
+#include "inferlist.h"
+
+InferenceList::InferenceList() {
+       list = new ModelList<Inference*>;
+}
+
+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<Inference*>* 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<Inference*> *newList = new ModelList<Inference*>;
+               for (ModelList<Inference*>::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<Inference*>::iterator it = list->begin(); it !=
+                       list->end(); it++) {
+                       delete *it;
+               }
+               delete list;
+               list = newList;
+       }       
+}
+
+void InferenceList::applyPatch(Inference *curInfer, SnapVector<Patch*> *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<Inference*> *newList = new ModelList<Inference*>;
+               for (ModelList<Inference*>::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<Inference*>::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<Inference*> *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<Inference*> *newCandidates = new ModelList<Inference*>(),
+               *candidates = list;
+
+       ModelList<Inference*>::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<Inference*> *l) {
+       for (ModelList<Inference*>::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<Inference*> *inferList, const char *msg) {
+       for (ModelList<Inference*>::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 (file)
index 0000000..bc3476a
--- /dev/null
@@ -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<Inference*> *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<Inference*>* 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<Patch*> *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<Inference*> *l);
+
+       static void clearAll(InferenceList *inferList);
+       
+       static void print(ModelList<Inference*> *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 (file)
index 0000000..7eeb003
--- /dev/null
@@ -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<Inference*> *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<Inference*>::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<Inference*> *list = results->getList();
+       for (ModelList<Inference*>::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<Inference*> *list = discoveredSet->getList();
+
+       // An array of strengthened wildcards
+       SnapVector<int> *strengthened = new SnapVector<int>;
+       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<Inference*>::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<Inference*>::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<Inference*> *list = discoveredSet->getList();
+       for (ModelList<Inference*>::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<Inference*> *list = discoveredSet->getList();
+       for (ModelList<Inference*>::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 (file)
index 0000000..965d2f9
--- /dev/null
@@ -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 (file)
index 0000000..3fabe01
--- /dev/null
@@ -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<PatchUnit*>;
+       units->push_back(unit);
+}
+
+Patch::Patch(const ModelAction *act1, memory_order mo1, const ModelAction *act2, memory_order mo2) {
+       units = new SnapVector<PatchUnit*>;
+       PatchUnit *unit = new PatchUnit(act1, mo1);
+       units->push_back(unit);
+       unit = new PatchUnit(act2, mo2);
+       units->push_back(unit);
+}
+
+Patch::Patch() {
+       units = new SnapVector<PatchUnit*>;
+}
+
+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 (file)
index 0000000..d25bed1
--- /dev/null
@@ -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<PatchUnit*> *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 (file)
index 0000000..1f37107
--- /dev/null
@@ -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 (file)
index 0000000..63408cb
--- /dev/null
@@ -0,0 +1,1298 @@
+#include "scfence.h"
+#include "action.h"
+#include "threads-model.h"
+#include "clockvector.h"
+#include "execution.h"
+#include "cyclegraph.h"
+#include <sys/time.h>
+
+#include "model.h"
+#include "wildcard.h"
+#include "inference.h"
+#include "inferset.h"
+#include "sc_annotation.h"
+#include "errno.h"
+#include <stdio.h>
+#include <algorithm>
+
+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<Patch*>* SCFence::getAcqRel(const ModelAction *read, const
+       ModelAction *readBound,const ModelAction *write, const ModelAction *writeBound) {
+       
+       SnapVector<Patch*> *patches = new SnapVector<Patch*>;
+       /* 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<Patch*> *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<Patch*> *patches = new SnapVector<Patch*>;
+       
+       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<action_list_t*> *opList = new SnapList<action_list_t*>;
+       /** 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<action_list_t*>::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<action_list_t*>::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 (file)
index 0000000..e1e27a1
--- /dev/null
@@ -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 <sys/time.h>
+
+#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<path_t *> 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<action_list_t> *dup_threadlists;
+       ModelExecution *execution;
+
+       /** A set of actions that should be ignored in the partially SC analysis */
+       HashTable<const ModelAction*, const ModelAction*, uintptr_t, 4> 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<Patch*>* 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 (file)
index 0000000..cfcd0e5
--- /dev/null
@@ -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<action_list_t>* 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<const ModelAction *, const ModelAction *, uintptr_t, 4> * SCGenerator::getBadrfset() {
+       return &badrfset;
+}
+
+HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > * 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)<numActions)
+                                       lastchoice=currchoice;
+                               currchoice++;
+                       } else {
+                               act = array[0];
+                               choices[currchoice]=0;
+                               if (numActions>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<action_list_t> *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<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset1;
+       HashTable<void *, const ModelAction *, uintptr_t, 4 > 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;i<count;i++) {
+               if (!array[i]->is_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;a<count;a++) {
+               ModelAction *act=array[a];
+               for (int i = 0; i <= maxthreads && act != NULL; 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
+                                       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 (file)
index 0000000..a16e6b0
--- /dev/null
@@ -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 <sys/time.h>
+
+typedef struct SCGeneratorOption {
+       bool print_always;
+       bool print_buggy;
+       bool print_nonsc;
+       bool annotationMode;
+} SCGeneratorOption;
+
+
+class SCGenerator {
+public:
+       SCGenerator();
+       ~SCGenerator();
+
+       bool getCyclic();
+       SnapVector<action_list_t>* 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<const ModelAction *, const ModelAction *, uintptr_t, 4> *getBadrfset();
+
+       HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > *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<action_list_t> *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<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;
+       bool cyclic;
+       HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset;
+       HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap;
+       SnapVector<action_list_t> threadlists;
+       SnapVector<action_list_t> 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<const ModelAction *, const ModelAction *, uintptr_t, 4 > annotatedReadSet;
+       int annotatedReadSetSize;
+       bool annotationMode;
+       bool annotationError;
+
+       /** A set of actions that should be ignored in the partially SC analysis */
+       HashTable<const ModelAction*, const ModelAction*, uintptr_t, 4> ignoredActions;
+};
+#endif
index df3356a..d363150 100644 (file)
@@ -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