Remove SC Analysis
authorbdemsky <bdemsky@uci.edu>
Tue, 16 Oct 2018 21:51:59 +0000 (14:51 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 16 Oct 2018 21:51:59 +0000 (14:51 -0700)
20 files changed:
Makefile
main.cc
plugins.cc
scanalysis.cc [deleted file]
scanalysis.h [deleted file]
scfence/Makefile [deleted file]
scfence/fence_common.h [deleted file]
scfence/inference.cc [deleted file]
scfence/inference.h [deleted file]
scfence/inferlist.cc [deleted file]
scfence/inferlist.h [deleted file]
scfence/inferset.cc [deleted file]
scfence/inferset.h [deleted file]
scfence/patch.cc [deleted file]
scfence/patch.h [deleted file]
scfence/sc_annotation.h [deleted file]
scfence/scfence.cc [deleted file]
scfence/scfence.h [deleted file]
scfence/scgen.cc [deleted file]
scfence/scgen.h [deleted file]

index eb84076..fe1bf0d 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,14 +1,12 @@
 include common.mk
 
-SCFENCE_DIR := scfence
-
 OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \
-          context.o scanalysis.o execution.o plugins.o libannotate.o
+          context.o execution.o plugins.o libannotate.o
 
-CPPFLAGS += -Iinclude -I. -I$(SCFENCE_DIR)
+CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic
 SHARED := -shared
 
@@ -41,9 +39,6 @@ malloc.o: malloc.c
 %.o : %.cc
        $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS)
 
-include $(SCFENCE_DIR)/Makefile
-
--include $(wildcard $(SCFENCE_DIR)/.*.d)
 
 $(LIB_SO): $(OBJECTS)
        $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS)
@@ -55,7 +50,7 @@ $(LIB_SO): $(OBJECTS)
 
 PHONY += clean
 clean:
-       rm -f *.o *.so .*.d *.pdf *.dot $(SCFENCE_DIR)/.*.d $(SCFENCE_DIR)/*.o
+       rm -f *.o *.so .*.d *.pdf *.dot
        $(MAKE) -C $(TESTS_DIR) clean
 
 PHONY += mrclean
diff --git a/main.cc b/main.cc
index 502f499..5b764b6 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -15,7 +15,6 @@
 #include "model.h"
 #include "params.h"
 #include "snapshot-interface.h"
-#include "scanalysis.h"
 #include "plugins.h"
 
 static void param_defaults(struct model_params *params)
index 38493de..c98cb5d 100644 (file)
@@ -1,6 +1,4 @@
 #include "plugins.h"
-#include "scanalysis.h"
-#include "scfence.h"
 
 ModelVector<TraceAnalysis *> * registered_analysis;
 ModelVector<TraceAnalysis *> * installed_analysis;
@@ -8,8 +6,6 @@ ModelVector<TraceAnalysis *> * installed_analysis;
 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/scanalysis.cc b/scanalysis.cc
deleted file mode 100644 (file)
index 6fc1e08..0000000
+++ /dev/null
@@ -1,458 +0,0 @@
-#include "scanalysis.h"
-#include "action.h"
-#include "threads-model.h"
-#include "clockvector.h"
-#include "execution.h"
-#include <sys/time.h>
-
-
-SCAnalysis::SCAnalysis() :
-       cvmap(),
-       cyclic(false),
-       badrfset(),
-       lastwrmap(),
-       threadlists(1),
-       execution(NULL),
-       print_always(false),
-       print_buggy(true),
-       print_nonsc(false),
-       time(false),
-       stats((struct sc_statistics *)model_calloc(1, sizeof(struct sc_statistics)))
-{
-}
-
-SCAnalysis::~SCAnalysis() {
-       delete(stats);
-}
-
-void SCAnalysis::setExecution(ModelExecution * execution) {
-       this->execution=execution;
-}
-
-const char * SCAnalysis::name() {
-       const char * name = "SC";
-       return name;
-}
-
-void SCAnalysis::finish() {
-       if (time)
-               model_print("Elapsed time in usec %llu\n", stats->elapsedtime);
-       model_print("SC count: %u\n", stats->sccount);
-       model_print("Non-SC count: %u\n", stats->nonsccount);
-       model_print("Total actions: %llu\n", stats->actions);
-       unsigned long long actionperexec=(stats->actions)/(stats->sccount+stats->nonsccount);
-       model_print("Actions per execution: %llu\n", actionperexec);
-}
-
-bool SCAnalysis::option(char * opt) {
-       if (strcmp(opt, "verbose")==0) {
-               print_always=true;
-               return false;
-       } else if (strcmp(opt, "buggy")==0) {
-               return false;
-       } else if (strcmp(opt, "quiet")==0) {
-               print_buggy=false;
-               return false;
-       } else if (strcmp(opt, "nonsc")==0) {
-               print_nonsc=true;
-               return false;
-       } else if (strcmp(opt, "time")==0) {
-               time=true;
-               return false;
-       } else if (strcmp(opt, "help") != 0) {
-               model_print("Unrecognized option: %s\n", opt);
-       }
-
-       model_print("SC Analysis options\n");
-       model_print("verbose -- print all feasible executions\n");
-       model_print("buggy -- print only buggy executions (default)\n");
-       model_print("nonsc -- print non-sc execution\n");
-       model_print("quiet -- print nothing\n");
-       model_print("time -- time execution of scanalysis\n");
-       model_print("\n");
-       
-       return true;
-}
-
-void SCAnalysis::print_list(action_list_t *list) {
-       model_print("---------------------------------------------------------------------\n");
-       if (cyclic)
-               model_print("Not SC\n");
-       unsigned int hash = 0;
-
-       for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
-               const ModelAction *act = *it;
-               if (act->get_seq_number() > 0) {
-                       if (badrfset.contains(act))
-                               model_print("BRF ");
-                       act->print();
-                       if (badrfset.contains(act)) {
-                               model_print("Desired Rf: %u \n", badrfset.get(act)->get_seq_number());
-                       }
-               }
-               hash = hash ^ (hash << 3) ^ ((*it)->hash());
-       }
-       model_print("HASH %u\n", hash);
-       model_print("---------------------------------------------------------------------\n");
-}
-
-void SCAnalysis::analyze(action_list_t *actions) {
-
-       struct timeval start;
-       struct timeval finish;
-       if (time)
-               gettimeofday(&start, NULL);
-       action_list_t *list = generateSC(actions);
-       check_rf(list);
-       if (print_always || (print_buggy && execution->have_bug_reports())|| (print_nonsc && cyclic))
-               print_list(list);
-       if (time) {
-               gettimeofday(&finish, NULL);
-               stats->elapsedtime+=((finish.tv_sec*1000000+finish.tv_usec)-(start.tv_sec*1000000+start.tv_usec));
-       }
-       update_stats();
-}
-
-void SCAnalysis::update_stats() {
-       if (cyclic) {
-               stats->nonsccount++;
-       } else {
-               stats->sccount++;
-       }
-}
-
-void SCAnalysis::check_rf(action_list_t *list) {
-       for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
-               const ModelAction *act = *it;
-               if (act->is_read()) {
-                       if (act->get_reads_from() != lastwrmap.get(act->get_location()))
-                               badrfset.put(act, lastwrmap.get(act->get_location()));
-               }
-               if (act->is_write())
-                       lastwrmap.put(act->get_location(), act);
-       }
-}
-
-bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) {
-       ClockVector *cv2 = cvmap.get(act2);
-       if (cv2 == NULL)
-               return true;
-       if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
-               cyclic = true;
-               //refuse to introduce cycles into clock vectors
-               return false;
-       }
-
-       return cv->merge(cv2);
-}
-
-int SCAnalysis::getNextActions(ModelAction ** array) {
-       int count=0;
-
-       for (int t = 0; t <= maxthreads; t++) {
-               action_list_t *tlt = &threadlists[t];
-               if (tlt->empty())
-                       continue;
-               ModelAction *act = tlt->front();
-               ClockVector *cv = cvmap.get(act);
-               
-               /* Find the earliest in SC ordering */
-               for (int i = 0; i <= maxthreads; i++) {
-                       if ( i == t )
-                               continue;
-                       action_list_t *threadlist = &threadlists[i];
-                       if (threadlist->empty())
-                               continue;
-                       ModelAction *first = threadlist->front();
-                       if (cv->synchronized_since(first)) {
-                               act = NULL;
-                               break;
-                       }
-               }
-               if (act != NULL) {
-                       array[count++]=act;
-               }
-       }
-       if (count != 0)
-               return count;
-       for (int t = 0; t <= maxthreads; t++) {
-               action_list_t *tlt = &threadlists[t];
-               if (tlt->empty())
-                       continue;
-               ModelAction *act = tlt->front();
-               ClockVector *cv = act->get_cv();
-               
-               /* Find the earliest in SC ordering */
-               for (int i = 0; i <= maxthreads; i++) {
-                       if ( i == t )
-                               continue;
-                       action_list_t *threadlist = &threadlists[i];
-                       if (threadlist->empty())
-                               continue;
-                       ModelAction *first = threadlist->front();
-                       if (cv->synchronized_since(first)) {
-                               act = NULL;
-                               break;
-                       }
-               }
-               if (act != NULL) {
-                       array[count++]=act;
-               }
-       }
-
-       ASSERT(count==0 || cyclic);
-
-       return count;
-}
-
-ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) {
-       /* No choice */
-       if (count == 1)
-               return array[0];
-
-       /* Choose first non-write action */
-       ModelAction *nonwrite=NULL;
-       for(int i=0;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;
-}
-
-action_list_t * SCAnalysis::generateSC(action_list_t *list) {
-       int numactions=buildVectors(list);
-       stats->actions+=numactions;
-
-       computeCV(list);
-
-       action_list_t *sclist = new action_list_t();
-       ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
-       int * choices = (int *) model_calloc(1, sizeof(int)*numactions);
-       int endchoice = 0;
-       int currchoice = 0;
-       int lastchoice = -1;
-       while (true) {
-               int numActions = getNextActions(array);
-               if (numActions == 0)
-                       break;
-               ModelAction * act=pruneArray(array, numActions);
-               if (act == NULL) {
-                       if (currchoice < endchoice) {
-                               act = array[choices[currchoice]];
-                               //check whether there is still another option
-                               if ((choices[currchoice]+1)<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(list);
-                                       computeCV(list);
-                                       sclist->clear();
-                                       continue;
-                               }
-                       }
-               }
-               //add action to end
-               sclist->push_back(act);
-       }
-       model_free(array);
-       return sclist;
-}
-
-int SCAnalysis::buildVectors(action_list_t *list) {
-       maxthreads = 0;
-       int numactions = 0;
-       for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
-               ModelAction *act = *it;
-               numactions++;
-               int threadid = id_to_int(act->get_tid());
-               if (threadid > maxthreads) {
-                       threadlists.resize(threadid + 1);
-                       maxthreads = threadid;
-               }
-               threadlists[threadid].push_back(act);
-       }
-       return numactions;
-}
-
-void SCAnalysis::reset(action_list_t *list) {
-       for (int t = 0; t <= maxthreads; t++) {
-               action_list_t *tlt = &threadlists[t];
-               tlt->clear();
-       }
-       for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
-               ModelAction *act = *it;
-               delete cvmap.get(act);
-               cvmap.put(act, NULL);
-       }
-
-       cyclic=false;   
-}
-
-bool SCAnalysis::updateConstraints(ModelAction *act) {
-       bool changed = false;
-       for (int i = 0; i <= maxthreads; i++) {
-               thread_id_t tid = int_to_id(i);
-               if (tid == act->get_tid())
-                       continue;
-
-               action_list_t *list = &threadlists[id_to_int(tid)];
-               for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
-                       ModelAction *write = *rit;
-                       if (!write->is_write())
-                               continue;
-                       ClockVector *writecv = cvmap.get(write);
-                       if (writecv->synchronized_since(act))
-                               break;
-                       if (write->get_location() == act->get_location()) {
-                               //write is sc after act
-                               merge(writecv, write, act);
-                               changed = true;
-                               break;
-                       }
-               }
-       }
-       return changed;
-}
-
-bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
-       bool changed = false;
-
-       /* Merge in the clock vector from the write */
-       const ModelAction *write = read->get_reads_from();
-       ClockVector *writecv = cvmap.get(write);
-       changed |= merge(cv, read, write) && (*read < *write);
-
-       for (int i = 0; i <= maxthreads; i++) {
-               thread_id_t tid = int_to_id(i);
-               if (tid == read->get_tid())
-                       continue;
-               if (tid == write->get_tid())
-                       continue;
-               action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
-               if (list == NULL)
-                       continue;
-               for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
-                       ModelAction *write2 = *rit;
-                       if (!write2->is_write())
-                               continue;
-
-                       ClockVector *write2cv = cvmap.get(write2);
-                       if (write2cv == NULL)
-                               continue;
-
-                       /* write -sc-> write2 &&
-                                write -rf-> R =>
-                                R -sc-> write2 */
-                       if (write2cv->synchronized_since(write)) {
-                               changed |= merge(write2cv, write2, read);
-                       }
-
-                       //looking for earliest write2 in iteration to satisfy this
-                       /* write2 -sc-> R &&
-                                write -rf-> R =>
-                                write2 -sc-> write */
-                       if (cv->synchronized_since(write2)) {
-                               changed |= writecv == NULL || merge(writecv, write, write2);
-                               break;
-                       }
-               }
-       }
-       return changed;
-}
-
-void SCAnalysis::computeCV(action_list_t *list) {
-       bool changed = true;
-       bool firsttime = true;
-       ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
-       while (changed) {
-               changed = changed&firsttime;
-               firsttime = false;
-
-               for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
-                       ModelAction *act = *it;
-                       ModelAction *lastact = last_act[id_to_int(act->get_tid())];
-                       if (act->is_thread_start())
-                               lastact = execution->get_thread(act)->get_creation();
-                       last_act[id_to_int(act->get_tid())] = act;
-                       ClockVector *cv = cvmap.get(act);
-                       if (cv == NULL) {
-                               cv = new ClockVector(NULL, act);
-                               cvmap.put(act, cv);
-                       }
-                       if (lastact != NULL) {
-                               merge(cv, act, lastact);
-                       }
-                       if (act->is_thread_join()) {
-                               Thread *joinedthr = act->get_thread_operand();
-                               ModelAction *finish = execution->get_last_action(joinedthr->get_id());
-                               changed |= merge(cv, act, finish);
-                       }
-                       if (act->is_read()) {
-                               changed |= processRead(act, cv);
-                       }
-               }
-               /* Reset the last action array */
-               if (changed) {
-                       bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
-               }
-       }
-       model_free(last_act);
-}
diff --git a/scanalysis.h b/scanalysis.h
deleted file mode 100644 (file)
index 23d127b..0000000
+++ /dev/null
@@ -1,52 +0,0 @@
-#ifndef SCANALYSIS_H
-#define SCANALYSIS_H
-#include "traceanalysis.h"
-#include "hashtable.h"
-
-struct sc_statistics {
-       unsigned long long elapsedtime;
-       unsigned int sccount;
-       unsigned int nonsccount;
-       unsigned long long actions;
-};
-
-class SCAnalysis : public TraceAnalysis {
- public:
-       SCAnalysis();
-       ~SCAnalysis();
-       virtual void setExecution(ModelExecution * execution);
-       virtual void analyze(action_list_t *);
-       virtual const char * name();
-       virtual bool option(char *);
-       virtual void finish();
-
-
-       SNAPSHOTALLOC
- private:
-       void update_stats();
-       void print_list(action_list_t *list);
-       int buildVectors(action_list_t *);
-       bool updateConstraints(ModelAction *act);
-       void computeCV(action_list_t *);
-       action_list_t * generateSC(action_list_t *);
-       bool processRead(ModelAction *read, ClockVector *cv);
-       int getNextActions(ModelAction **array);
-       bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2);
-       void check_rf(action_list_t *list);
-       void reset(action_list_t *list);
-       ModelAction* pruneArray(ModelAction**, int);
-
-       int maxthreads;
-       HashTable<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;
-       ModelExecution *execution;
-       bool print_always;
-       bool print_buggy;
-       bool print_nonsc;
-       bool time;
-       struct sc_statistics *stats;
-};
-#endif
diff --git a/scfence/Makefile b/scfence/Makefile
deleted file mode 100644 (file)
index d0cc313..0000000
+++ /dev/null
@@ -1,11 +0,0 @@
-FENCE_OBJS := $(SCFENCE_DIR)/scgen.o \
-       $(SCFENCE_DIR)/inference.o \
-       $(SCFENCE_DIR)/inferset.o \
-       $(SCFENCE_DIR)/inferlist.o \
-       $(SCFENCE_DIR)/patch.o \
-       $(SCFENCE_DIR)/scfence.o
-
-$(FENCE_OBJS): $(SCFENCE_DIR)/%.o : $(SCFENCE_DIR)/%.cc $(SCFENCE_DIR)/%.h
-       $(CXX) -MMD -MF $(SCFENCE_DIR)/.$(notdir $@).d -fPIC -c $< $(CPPFLAGS) -o $@
-
-OBJECTS += $(FENCE_OBJS)
diff --git a/scfence/fence_common.h b/scfence/fence_common.h
deleted file mode 100644 (file)
index 014cce1..0000000
+++ /dev/null
@@ -1,35 +0,0 @@
-#ifndef _FENCE_COMMON_
-#define _FENCE_COMMON_
-
-#include "model.h"
-#include "action.h"
-
-#define DEFAULT_REPETITIVE_READ_BOUND 20
-
-#define FENCE_OUTPUT
-
-#ifdef FENCE_OUTPUT
-
-#define FENCE_PRINT model_print
-
-#define ACT_PRINT(x) (x)->print()
-
-#define CV_PRINT(x) (x)->print()
-
-#define WILDCARD_ACT_PRINT(x)\
-       FENCE_PRINT("Wildcard: %d\n", get_wildcard_id_zero((x)->get_original_mo()));\
-       ACT_PRINT(x);
-
-#else
-
-#define FENCE_PRINT
-
-#define ACT_PRINT(x)
-
-#define CV_PRINT(x)
-
-#define WILDCARD_ACT_PRINT(x)
-
-#endif
-
-#endif
diff --git a/scfence/inference.cc b/scfence/inference.cc
deleted file mode 100644 (file)
index e2d2152..0000000
+++ /dev/null
@@ -1,378 +0,0 @@
-#include "fence_common.h"
-#include "wildcard.h"
-#include "patch.h"
-#include "inferlist.h"
-#include "inference.h"
-
-/** Forward declaration */
-class PatchUnit;
-class Patch;
-class Inference;
-class InferenceList;
-
-bool isTheInference(Inference *infer) {
-       for (int i = 0; i < infer->getSize(); i++) {
-               memory_order mo1 = (*infer)[i], mo2;
-               if (mo1 == WILDCARD_NONEXIST)
-                       mo1 = relaxed;
-               switch (i) {
-                       case 3:
-                               mo2 = acquire;
-                       break;
-                       case 11:
-                               mo2 = release;
-                       break;
-                       default:
-                               mo2 = relaxed;
-                       break;
-               }
-               if (mo1 != mo2)
-                       return false;
-       }
-       return true;
-}
-
-const char* get_mo_str(memory_order order) {
-       switch (order) {
-               case std::memory_order_relaxed: return "relaxed";
-               case std::memory_order_acquire: return "acquire";
-               case std::memory_order_release: return "release";
-               case std::memory_order_acq_rel: return "acq_rel";
-               case std::memory_order_seq_cst: return "seq_cst";
-               default: 
-                       //model_print("Weird memory order, a bug or something!\n");
-                       //model_print("memory_order: %d\n", order);
-                       return "unknown";
-       }
-}
-
-
-void Inference::resize(int newsize) {
-       ASSERT (newsize > size && newsize <= MAX_WILDCARD_NUM);
-       memory_order *newOrders = (memory_order *) model_malloc((newsize + 1) * sizeof(memory_order*));
-       int i;
-       for (i = 0; i <= size; i++)
-               newOrders[i] = orders[i];
-       for (; i <= newsize; i++)
-               newOrders[i] = WILDCARD_NONEXIST;
-       model_free(orders);
-       size = newsize;
-       orders = newOrders;
-}
-
-/** Return the state of how we update a specific mo; If we have to make an
- * uncompatible inference or that inference cannot be imposed because it's
- * not a wildcard, it returns -1; if it is a compatible memory order but the
- * current memory order is no weaker than mo, it returns 0; otherwise, it
- * does strengthen the order, and returns 1 */
-int Inference::strengthen(const ModelAction *act, memory_order mo) {
-       memory_order wildcard = act->get_original_mo();
-       int wildcardID = get_wildcard_id_zero(wildcard);
-       if (!is_wildcard(wildcard)) {
-               FENCE_PRINT("We cannot make this update to %s!\n", get_mo_str(mo));
-               ACT_PRINT(act);
-               return -1;
-       }
-       if (wildcardID > size)
-               resize(wildcardID);
-       ASSERT (is_normal_mo(mo));
-       //model_print("wildcardID -> order: %d -> %d\n", wildcardID, orders[wildcardID]);
-       ASSERT (is_normal_mo_infer(orders[wildcardID]));
-       switch (orders[wildcardID]) {
-               case memory_order_seq_cst:
-                       return 0;
-               case memory_order_relaxed:
-                       if (mo == memory_order_relaxed)
-                               return 0;
-                       orders[wildcardID] = mo;
-                       break;
-               case memory_order_acquire:
-                       if (mo == memory_order_acquire || mo == memory_order_relaxed)
-                               return 0;
-                       if (mo == memory_order_release)
-                               orders[wildcardID] = memory_order_acq_rel;
-                       else if (mo >= memory_order_acq_rel && mo <=
-                               memory_order_seq_cst)
-                               orders[wildcardID] = mo;
-                       break;
-               case memory_order_release:
-                       if (mo == memory_order_release || mo == memory_order_relaxed)
-                               return 0;
-                       if (mo == memory_order_acquire)
-                               orders[wildcardID] = memory_order_acq_rel;
-                       else if (mo >= memory_order_acq_rel)
-                               orders[wildcardID] = mo;
-                       break;
-               case memory_order_acq_rel:
-                       if (mo == memory_order_seq_cst)
-                               orders[wildcardID] = mo;
-                       else
-                               return 0;
-                       break;
-               default:
-                       orders[wildcardID] = mo;
-                       break;
-       }
-       return 1;
-}
-
-Inference::Inference() {
-       orders = (memory_order *) model_malloc((4 + 1) * sizeof(memory_order*));
-       size = 4;
-       for (int i = 0; i <= size; i++)
-               orders[i] = WILDCARD_NONEXIST;
-       initialInfer = this;
-       buggy = false;
-       hasFixes = false;
-       leaf = false;
-       explored = false;
-       shouldFix = true;
-}
-
-Inference::Inference(Inference *infer) {
-       ASSERT (infer->size > 0 && infer->size <= MAX_WILDCARD_NUM);
-       orders = (memory_order *) model_malloc((infer->size + 1) * sizeof(memory_order*));
-       this->size = infer->size;
-       for (int i = 0; i <= size; i++)
-               orders[i] = infer->orders[i];
-
-       initialInfer = infer->initialInfer;
-       buggy = false;
-       hasFixes = false;
-       leaf = false;
-       explored = false;
-       shouldFix = true;
-}
-
-/** return value:
-  * 0 -> mo1 == mo2;
-  * 1 -> mo1 stronger than mo2;
-  * -1 -> mo1 weaker than mo2;
-  * 2 -> mo1 & mo2 are uncomparable.
- */
-int Inference::compareMemoryOrder(memory_order mo1, memory_order mo2) {
-       if (mo1 == WILDCARD_NONEXIST)
-               mo1 = memory_order_relaxed;
-       if (mo2 == WILDCARD_NONEXIST)
-               mo2 = memory_order_relaxed;
-       if (mo1 == mo2)
-               return 0;
-       if (mo1 == memory_order_relaxed)
-               return -1;
-       if (mo1 == memory_order_acquire) {
-               if (mo2 == memory_order_relaxed)
-                       return 1;
-               if (mo2 == memory_order_release)
-                       return 2;
-               return -1;
-       }
-       if (mo1 == memory_order_release) {
-               if (mo2 == memory_order_relaxed)
-                       return 1;
-               if (mo2 == memory_order_acquire)
-                       return 2;
-               return -1;
-       }
-       if (mo1 == memory_order_acq_rel) {
-               if (mo2 == memory_order_seq_cst)
-                       return -1;
-               else
-                       return 1;
-       }
-       // mo1 now must be SC and mo2 can't be SC
-       return 1;
-}
-
-
-/** Try to calculate the set of inferences that are weaker than this, but
- *  still stronger than infer */
-InferenceList* Inference::getWeakerInferences(Inference *infer) {
-       // An array of strengthened wildcards
-       SnapVector<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
deleted file mode 100644 (file)
index 2d61e59..0000000
+++ /dev/null
@@ -1,154 +0,0 @@
-#ifndef _INFERENCE_H
-#define _INFERENCE_H
-
-#include "fence_common.h"
-#include "wildcard.h"
-#include "patch.h"
-#include "inferlist.h"
-
-class InferenceList;
-class Inference;
-
-extern const char* get_mo_str(memory_order order);
-extern bool isTheInference(Inference *infer);
-
-class Inference {
-       private:
-       memory_order *orders;
-       int size;
-
-       /** It's initial inference, if not assigned, set it as itself */
-       Inference *initialInfer;
-
-       /** Whether this inference will lead to a buggy execution */
-       bool buggy;
-
-       /** Whether this inference has been explored */
-       bool explored;
-
-       /** Whether this inference is the leaf node in the inference lattice, see
-        * inferset.h for more details */
-       bool leaf;
-
-       /** When this inference will have buggy executions, this indicates whether
-        * it has any fixes. */
-       bool hasFixes;
-
-       /** When we have a strong enough inference, we also want to weaken specific
-        *  parameters to see if it is possible to be weakened. So we will this
-        *  field to mark if we should fix the inference or not if we get non-SC
-        *  behaviros. By default true. */
-       bool shouldFix;
-
-       void resize(int newsize);
-       
-       /** Return the state of how we update a specific mo; If we have to make an
-        * uncompatible inference or that inference cannot be imposed because it's
-        * not a wildcard, it returns -1; if it is a compatible memory order but the
-        * current memory order is no weaker than mo, it returns 0; otherwise, it
-        * does strengthen the order, and returns 1 */
-       int strengthen(const ModelAction *act, memory_order mo);
-
-       public:
-       Inference();
-
-       Inference(Inference *infer);
-       
-       /** return value:
-         * 0 -> mo1 == mo2;
-         * 1 -> mo1 stronger than mo2;
-         * -1 -> mo1 weaker than mo2;
-         * 2 -> mo1 & mo2 are uncomparable.
-        */
-       static int compareMemoryOrder(memory_order mo1, memory_order mo2);
-
-
-       /** Try to calculate the set of inferences that are weaker than this, but
-        *  still stronger than infer */
-       InferenceList* getWeakerInferences(Inference *infer);
-
-       static memory_order nextWeakOrder(memory_order mo1, memory_order mo2);
-
-       void getWeakerInferences(InferenceList* list, Inference *tmpRes, Inference *infer1,
-               Inference *infer2, SnapVector<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
deleted file mode 100644 (file)
index 5cb6326..0000000
+++ /dev/null
@@ -1,207 +0,0 @@
-#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
deleted file mode 100644 (file)
index bc3476a..0000000
+++ /dev/null
@@ -1,64 +0,0 @@
-#ifndef _INFERLIST_H
-#define _INFERLIST_H
-
-#include "fence_common.h"
-#include "patch.h"
-#include "inference.h"
-
-class Patch;
-class PatchUnit;
-class Inference;
-
-/** This class represents that the list of inferences that can fix the problem
- */
-class InferenceList {
-       private:
-       ModelList<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
deleted file mode 100644 (file)
index 7eeb003..0000000
+++ /dev/null
@@ -1,300 +0,0 @@
-#include "patch.h"
-#include "inference.h"
-#include "inferset.h"
-
-InferenceSet::InferenceSet() {
-       discoveredSet = new InferenceList;
-       results = new InferenceList;
-       candidates = new InferenceList;
-}
-
-/** Print the result of inferences  */
-void InferenceSet::printResults() {
-       results->print("Result");
-       stat.print();
-}
-
-/** Print candidates of inferences */
-void InferenceSet::printCandidates() {
-       candidates->print("Candidate");
-}
-
-/** When we finish model checking or cannot further strenghen with the
- * inference, we commit the inference to be explored; if it is feasible, we
- * put it in the result list */
-void InferenceSet::commitInference(Inference *infer, bool feasible) {
-       ASSERT (infer);
-       
-       infer->setExplored(true);
-       FENCE_PRINT("Explored %lu\n", infer->getHash());
-       if (feasible) {
-               addResult(infer);
-       }
-}
-
-int InferenceSet::getCandidatesSize() {
-       return candidates->getSize();
-}
-
-int InferenceSet::getResultsSize() {
-       return results->getSize();
-}
-
-/** Be careful that if the candidate is not added, it will be deleted in this
- *  function. Therefore, caller of this function should just delete the list when
- *  finishing calling this function. */
-bool InferenceSet::addCandidates(Inference *curInfer, InferenceList *inferList) {
-       if (!inferList)
-               return false;
-       // First prune the list of inference
-       inferList->pruneCandidates(curInfer);
-
-       ModelList<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
deleted file mode 100644 (file)
index 965d2f9..0000000
+++ /dev/null
@@ -1,147 +0,0 @@
-#ifndef _INFERSET_H
-#define _INFERSET_H
-
-#include "fence_common.h"
-#include "patch.h"
-#include "inference.h"
-#include "inferlist.h"
-
-typedef struct inference_stat {
-       int notAddedAtFirstPlace;
-
-       inference_stat() :
-               notAddedAtFirstPlace(0) {}
-
-       void print() {
-               model_print("Inference process statistics output:...\n");
-               model_print("The number of inference not added at the first place: %d\n",
-                       notAddedAtFirstPlace);
-       }
-} inference_stat_t;
-
-
-/** Essentially, we have to explore a big lattice of inferences, the bottom of
- *  which is the inference that has all relaxed orderings, and the top of which
- *  is the one that has all SC orderings. We define the partial ordering between
- *  inferences as in compareTo() function in the Infereence class. In another
- *  word, we compare ordering parameters one by one as a vector. Theoretically,
- *  we need to explore up to the number of 5^N inferences, where N denotes the
- *  number of wildcards (since we have 5 possible options for each memory order).
-
- *  We try to reduce the searching space by recording whether an inference has
- *  been discovered or not, and if so, we only need to explore from that
- *  inference for just once. We can use a set to record the inferences to be be
- *  explored, and insert new undiscovered fixes to that set iteratively until it
- *  gets empty.
-
- *  In detail, we use the InferenceList to represent that set, and use a
- *  LIFO-like actions in pushing and popping inferences. When we add an
- *  inference to the stack, we will set it to leaf or non-leaf node. For the
- *  current inference to be added, it is non-leaf node because it generates
- *  stronger inferences. On the other hands, for those generated inferences, we
- *  set them to be leaf node. So when we pop a leaf node, we know that it is
- *  not just discovered but thoroughly explored. Therefore, when we dicide
- *  whether an inference is discovered, we can first try to look up the
- *  discovered set and also derive those inferences that are stronger the
- *  explored ones to be discovered.
-
- ********** The main algorithm **********
- Initial:
-       InferenceSet set; // Store the candiates to explore in a set
-       Set discoveredSet; // Store the discovered candidates. For each discovered
-               // candidate, if it's explored (feasible or infeasible, meaning that
-               // they are already known to work or not work), we set it to be
-               // explored. With that, we can reduce the searching space by ignoring
-               // those candidates that are stronger than the explored ones.
-       Inference curInfer = RELAX; // Initialize the current inference to be all relaxed (RELAX)
-
- API Methods:
-       bool addInference(infer, bool isLeaf) {
-               // Push back infer to the discovered when it's not discvoerd, and return
-               // whether it's added or not
-       }
-       
-       void commitInference(infer, isFeasible) {
-               // Set the infer to be explored and add it to the result set if feasible 
-       }
-
-       Inference* getNextInference() {
-               // Get the next unexplored inference so that we can contine searching
-       }
-*/
-
-class InferenceSet {
-       private:
-
-       /** The set of already discovered nodes in the tree */
-       InferenceList *discoveredSet;
-
-       /** The list of feasible inferences */
-       InferenceList *results;
-
-       /** The set of candidates */
-       InferenceList *candidates;
-
-       /** The staticstics of inference process */
-       inference_stat_t stat;
-       
-       public:
-       InferenceSet();
-
-       /** Print the result of inferences  */
-       void printResults();
-
-       /** Print candidates of inferences */
-       void printCandidates();
-
-       /** When we finish model checking or cannot further strenghen with the
-        * inference, we commit the inference to be explored; if it is feasible, we
-        * put it in the result list */
-       void commitInference(Inference *infer, bool feasible);
-
-       int getCandidatesSize();
-
-       int getResultsSize();
-
-       /** Be careful that if the candidate is not added, it will be deleted in this
-        *  function. Therefore, caller of this function should just delete the list when
-        *  finishing calling this function. */
-       bool addCandidates(Inference *curInfer, InferenceList *inferList);
-
-
-       /** Check if we have stronger or equal inferences in the current result
-        * list; if we do, we remove them and add the passed-in parameter infer */
-        void addResult(Inference *infer);
-
-       /** Get the next available unexplored node; @Return NULL 
-        * if we don't have next, meaning that we are done with exploring */
-       Inference* getNextInference();
-
-       /** Add the current inference to the set before adding fixes to it; in
-        * this case, fixes will be added afterwards, and infer should've been
-        * discovered */
-       void addCurInference(Inference *infer);
-       
-       /** Add one weaker node (the stronger one has been explored and known to be SC,
-        *  we just want to know if a weaker one might also be SC).
-        *  @Return true if the node to add has not been explored yet
-        */
-       void addWeakerInference(Inference *curInfer);
-
-       /** Add one possible node that represents a fix for the current inference;
-        * @Return true if the node to add has not been explored yet
-        */
-       bool addInference(Inference *infer);
-
-       /** Return false if we haven't discovered that inference yet. Basically we
-        * search the candidates list */
-       bool hasBeenDiscovered(Inference *infer);
-
-       /** Return true if we have explored this inference yet. Basically we
-        * search the candidates list */
-       bool hasBeenExplored(Inference *infer);
-
-       MEMALLOC
-};
-
-#endif
diff --git a/scfence/patch.cc b/scfence/patch.cc
deleted file mode 100644 (file)
index 3fabe01..0000000
+++ /dev/null
@@ -1,69 +0,0 @@
-#include "patch.h"
-#include "inference.h"
-
-Patch::Patch(const ModelAction *act, memory_order mo) {
-       PatchUnit *unit = new PatchUnit(act, mo);
-       units = new SnapVector<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
deleted file mode 100644 (file)
index d25bed1..0000000
+++ /dev/null
@@ -1,59 +0,0 @@
-#ifndef _PATCH_H
-#define _PATCH_H
-
-#include "fence_common.h"
-#include "inference.h"
-
-class PatchUnit;
-class Patch;
-
-class PatchUnit {
-       private:
-       const ModelAction *act;
-       memory_order mo;
-
-       public:
-       PatchUnit(const ModelAction *act, memory_order mo) {
-               this->act= act;
-               this->mo = mo;
-       }
-
-       const ModelAction* getAct() {
-               return act;
-       }
-
-       memory_order getMO() {
-               return mo;
-       }
-
-       SNAPSHOTALLOC
-};
-
-class Patch {
-       private:
-       SnapVector<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
deleted file mode 100644 (file)
index 1f37107..0000000
+++ /dev/null
@@ -1,47 +0,0 @@
-#ifndef _SC_ANNOTATION_H
-#define _SC_ANNOTATION_H
-
-#include "cdsannotate.h"
-#include "action.h"
-
-#define SC_ANNOTATION 2
-
-#define BEGIN 1
-#define END 2
-#define KEEP 3
-
-
-inline bool IS_SC_ANNO(ModelAction *act) {
-       return act != NULL && act->is_annotation() &&
-               act->get_value() == SC_ANNOTATION;
-}
-
-inline bool IS_ANNO_BEGIN(ModelAction *act) {
-       return (void*) BEGIN == act->get_location();
-}
-
-inline bool IS_ANNO_END(ModelAction *act) {
-       return (void*) END == act->get_location();
-}
-
-inline bool IS_ANNO_KEEP(ModelAction *act) {
-       return (void*) KEEP == act->get_location();
-}
-
-inline void SC_BEGIN() {
-       void *loc = (void*) BEGIN;
-       cdsannotate(SC_ANNOTATION, loc);
-}
-
-inline void SC_END() {
-       void *loc = (void*) END;
-       cdsannotate(SC_ANNOTATION, loc);
-}
-
-inline void SC_KEEP() {
-       void *loc = (void*) KEEP;
-       cdsannotate(SC_ANNOTATION, loc);
-}
-
-
-#endif
diff --git a/scfence/scfence.cc b/scfence/scfence.cc
deleted file mode 100644 (file)
index 130dc3b..0000000
+++ /dev/null
@@ -1,1298 +0,0 @@
-#include "scfence.h"
-#include "action.h"
-#include "threads-model.h"
-#include "clockvector.h"
-#include "execution.h"
-#include "cyclegraph.h"
-#include <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 = "AUTOMO";
-       return name;
-}
-
-void SCFence::finish() {
-       model_print("SCFence finishes!\n");
-}
-
-
-/******************** SCFence-related Functions (Beginning) ********************/
-
-void SCFence::inspectModelAction(ModelAction *act) {
-       if (act == NULL) // Get pass cases like data race detector
-               return;
-       if (act->get_mo() >= memory_order_relaxed && act->get_mo() <=
-               memory_order_seq_cst) {
-               return;
-       } else if (act->get_mo() == memory_order_normal) {
-               // For the purpose of eliminating data races
-               act->set_mo(memory_order_relaxed);
-       } else { // For wildcards
-               Inference *curInfer = getCurInference();
-               int wildcardID = get_wildcard_id(act->get_mo());
-               memory_order order = (*curInfer)[wildcardID];
-               if (order == WILDCARD_NONEXIST) {
-                       (*curInfer)[wildcardID] = memory_order_relaxed;
-                       act->set_mo(memory_order_relaxed);
-               } else {
-                       act->set_mo((*curInfer)[wildcardID]);
-               }
-       }
-}
-
-
-void SCFence::actionAtInstallation() {
-       // When this pluggin gets installed, it become the inspect_plugin
-       model->set_inspect_plugin(this);
-}
-
-void SCFence::analyze(action_list_t *actions) {
-       scgen->setActions(actions);
-       scgen->setExecution(execution);
-       dup_threadlists = scgen->getDupThreadLists();
-       if (getTimeout() > 0 && isTimeout()) {
-               model_print("Backtrack because we reached the timeout bound.\n");
-               routineBacktrack(false);
-               return;
-       }
-
-       /* Build up the thread lists for general purpose */
-       mo_graph = execution->get_mo_graph();
-
-       // First of all check if there's any uninitialzed read bugs
-       if (execution->have_bug_reports()) {
-               setBuggy(true);
-       }
-
-       action_list_t *list = scgen->getSCList();
-       bool cyclic = scgen->getCyclic();
-       
-       struct sc_statistics *s = scgen->getStats();
-       stats->nonsccount += s->nonsccount;
-       stats->sccount += s->sccount;
-       stats->elapsedtime += s->elapsedtime;
-       stats->actions += s->actions;
-
-       if (!cyclic && execution->have_bug_reports()) {
-               model_print("Be careful. This execution has bugs and still SC\n");
-       }
-
-       if (!cyclic && scgen->getPrintAlways()) {
-               scgen->print_list(list);
-       }
-
-       // Now we find a non-SC execution
-       if (cyclic) {
-               /******** The Non-SC case (beginning) ********/
-               // Only print those that should be fixed
-               if (getCurInference()->getShouldFix())
-                       scgen->print_list(list);
-               bool added = addFixes(list, NON_SC);
-               if (added) {
-                       routineAfterAddFixes();
-                       return;
-               } else { // Couldn't imply anymore, backtrack
-                       routineBacktrack(false);
-                       return;
-               }
-               /******** The Non-SC case (end) ********/
-       } else {
-               /******** The implicit MO case (beginning) ********/
-               if (getInferImplicitMO() && execution->too_many_steps() &&
-                       !execution->is_complete_execution()) {
-                       // Only print those that should be fixed
-                       if (getCurInference()->getShouldFix())
-                               scgen->print_list(list);
-                       bool added = addFixes(list, IMPLICIT_MO);
-                       if (added) {
-                               FENCE_PRINT("Found an implicit mo pattern to fix!\n");
-                               routineAfterAddFixes();
-                               return;
-                       } else {
-                               // This can be a good execution, so we can't do anything,
-                               return;
-                       }
-               }
-               /******** The implicit MO case (end) ********/
-
-               /******** The checking data races case (beginning) ********/
-               bool added = addFixes(list, DATA_RACE);
-               if (added) {
-                       FENCE_PRINT("Found an data race pattern to fix!\n");
-                       routineAfterAddFixes();
-                       return;
-               }
-       }
-}
-
-void SCFence::exitModelChecker() {
-       model->exit_model_checker();
-}
-
-void SCFence::restartModelChecker() {
-       model->restart();
-       if (!getHasRestarted())
-               setHasRestarted(true);
-}
-
-bool SCFence::modelCheckerAtExitState() {
-       return model->get_exit_flag();
-}
-
-void SCFence::actionAtModelCheckingFinish() {
-       // Just bail if the model checker is at the exit state
-       if (modelCheckerAtExitState())
-               return;
-
-       /** Backtrack with a successful inference */
-       routineBacktrack(true);
-}
-
-void SCFence::initializeByFile() {
-       char *name = getCandidateFile();
-       FILE *fp = fopen(name, "r");
-       if (fp == NULL) {
-               fprintf(stderr, "Cannot open the input parameter assignment file: %s!\n", name);
-               perror(name);
-               exit(EXIT_FAILURE);
-       }
-       Inference *infer = NULL;
-       int curNum = 0;
-       memory_order mo = memory_order_relaxed;
-       char *str = (char *) malloc(sizeof(char) * (30 + 1));
-       bool isProcessing = false;
-       int ret = 0;
-       while (!feof(fp)) {
-               // Result #:
-               if (!isProcessing) {
-                       ret = fscanf(fp, "%s", str);
-               }
-               if (strcmp(str, "Result") == 0 || isProcessing) { // In an inference
-                       ret = fscanf(fp, "%s", str);
-                       
-                       infer = new Inference();
-                       isProcessing = false;
-                       while (!feof(fp)) { // Processing a specific inference
-                               // wildcard # -> memory_order
-                               ret = fscanf(fp, "%s", str);
-                                       
-                               if (strcmp(str, "Result") == 0) {
-                                       isProcessing = true;
-                                       break;
-                               }
-                               ret = fscanf(fp, "%d", &curNum);
-                               ret = fscanf(fp, "%s", str);
-                               if (ret <= 0 && ret != -1) {
-                                       fprintf(stderr, "The input parameter assignment file has wrong format\n");
-                                       perror(name);
-                                       exit(EXIT_FAILURE);
-                               }
-                               ret = fscanf(fp, "%s", str);
-                                
-                               if (strcmp(str, "memory_order_relaxed") == 0)
-                                       mo = memory_order_relaxed;
-                               else if (strcmp(str, "memory_order_acquire") == 0)
-                                       mo = memory_order_acquire;
-                               else if (strcmp(str, "memory_order_release") == 0)
-                                       mo = memory_order_release;
-                               else if (strcmp(str, "memory_order_acq_rel") == 0)
-                                       mo = memory_order_acq_rel;
-                               else if (strcmp(str, "memory_order_seq_cst") == 0)
-                                       mo = memory_order_seq_cst;
-                               (*infer)[curNum] = mo;
-                       }
-
-                       /******** addInference ********/
-                       if (!addInference(infer))
-                               delete infer;
-               }
-       }
-       fclose(fp);
-
-       FENCE_PRINT("candidate size from file: %d\n", setSize());
-       Inference *next = getNextInference();
-       if (!next) {
-               model_print("Wrong with the candidate file\n");
-       } else {
-               setCurInference(next);
-       }
-}
-
-char* SCFence::parseOptionHelper(char *opt, int *optIdx) {
-       char *res = (char*) model_malloc(1024 * sizeof(char));
-       int resIdx = 0;
-       while (opt[*optIdx] != '\0' && opt[*optIdx] != '|') {
-               res[resIdx++] = opt[(*optIdx)++];
-       }
-       res[resIdx] = '\0';
-       return res;
-}
-
-bool SCFence::parseOption(char *opt) {
-       int optIdx = 0;
-       char *val = NULL;
-       while (true) {
-               char option = opt[optIdx++];
-               val = parseOptionHelper(opt, &optIdx);
-               switch (option) {
-                       case 'f': // Read initial inference from file
-                               setCandidateFile(val);
-                               if (strcmp(val, "") == 0) {
-                                       model_print("Need to specify a file that contains initial inference!\n");
-                                       return true;
-                               }
-                               break;
-                       case 'b': // The bound above 
-                               setImplicitMOReadBound(atoi(val));
-                               if (getImplicitMOReadBound() <= 0) {
-                                       model_print("Enter valid bound value!\n");
-                                       return true;
-                               }
-                               break;
-                       case 'm': // Infer the modification order from repetitive reads from
-                                         // the same write
-                               setInferImplicitMO(true);
-                               if (strcmp(val, "") != 0) {
-                                       model_print("option m doesn't take any arguments!\n");
-                                       return true;
-                               }
-                               break;
-                       case 'a': // Turn on the annotation mode 
-                               scgen->setAnnotationMode(true);
-                               if (strcmp(val, "") != 0) {
-                                       model_print("option a doesn't take any arguments!\n");
-                                       return true;
-                               }
-                               break;
-                       case 't': // The timeout set to force the analysis to backtrack
-                               model_print("Parsing t option!\n");
-                               model_print("t value: %s\n", val);
-                               setTimeout(atoi(val));
-                               break;
-                       default:
-                               model_print("Unknown SCFence option: %c!\n", option);
-                               return true;
-                               break;
-               }
-               if (opt[optIdx] == '|') {
-                       optIdx++;
-               } else {
-                       break;
-               }
-       }
-       return false;
-
-}
-
-char* SCFence::getInputFileName(char *opt) {
-       char *res = NULL;
-       if (opt[0] == 'f' &&
-               opt[1] == 'i' &&
-               opt[2] == 'l' &&
-               opt[3] == 'e' &&
-               opt[4] == '-') {
-               
-               res = (char*) model_malloc(1024 * sizeof(char));
-               int i = 0, j = 5;
-               while (opt[j] != '\0') {
-                       res[i++] = opt[j++];
-               }
-               res[i] = '\0';
-       }
-       return res;
-}
-
-int SCFence::getImplicitMOBound(char *opt) {
-       char *num = NULL;
-       if (opt[0] == 'b' &&
-               opt[1] == 'o' &&
-               opt[2] == 'u' &&
-               opt[3] == 'n' &&
-               opt[4] == 'd' &&
-               opt[5] == '-') {
-               
-               num = (char*) model_malloc(1024 * sizeof(char));
-               int i = 0, j = 6;
-               while (opt[j] != '\0') {
-                       num[i++] = opt[j++];
-               }
-               num[i] = '\0';
-       }
-       if (num) {
-               return atoi(num);
-       } else {
-               return 0;
-       }
-}
-
-bool SCFence::option(char * opt) {
-       char *inputFileName = NULL;
-       unsigned implicitMOBoundNum = 0;
-
-       if (strcmp(opt, "verbose")==0) {
-               scgen->setPrintAlways(true);
-               return false;
-       } else if (strcmp(opt, "buggy")==0) {
-               return false;
-       } else if (strcmp(opt, "quiet")==0) {
-               scgen->setPrintBuggy(false);
-               return false;
-       } else if (strcmp(opt, "nonsc")==0) {
-               scgen->setPrintNonSC(true);
-               return false;
-       } else if (strcmp(opt, "time")==0) {
-               time=true;
-               return false;
-       } else if (strcmp(opt, "no-weaken")==0) {
-               weaken=false;
-               return false;
-       } else if (strcmp(opt, "anno")==0) {
-               scgen->setAnnotationMode(true);
-               return false;
-       } else if (strcmp(opt, "implicit-mo")==0) {
-               setInferImplicitMO(true);
-               return false;
-       } else if ((inputFileName = getInputFileName(opt)) != NULL) {
-               if (strcmp(inputFileName, "") == 0) {
-                       model_print("Need to specify a file that contains initial inference!\n");
-                       return true;
-               }
-               setCandidateFile(inputFileName);
-               initializeByFile();
-               return false;
-       } else if ((implicitMOBoundNum = getImplicitMOBound(opt)) > 0) {
-               setImplicitMOReadBound(implicitMOBoundNum);
-               return false;
-       } else {
-               model_print("file-InputFile -- takes candidate file as argument right after the symbol '-' \n");
-               model_print("no-weaken -- turn off the weakening mode (by default ON)\n");
-               model_print("anno -- turn on the annotation mode (by default OFF)\n");
-               model_print("implicit-mo -- imply implicit modification order, takes no arguments (by default OFF, default bound is %d\n", DEFAULT_REPETITIVE_READ_BOUND);
-               model_print("bound-NUM -- specify the bound for the implicit mo implication, takes a number as argument right after the symbol '-'\n");
-               model_print("\n");
-               return true;
-       }
-}
-
-/** Check whether a chosen reads-from path is a release sequence */
-bool SCFence::isReleaseSequence(path_t *path) {
-       ASSERT (path);
-       path_t::reverse_iterator rit = path->rbegin(),
-               rit_next;
-       const ModelAction *read,
-               *write,
-               *next_read;
-       for (; rit != path->rend(); rit++) {
-               read = *rit;
-               rit_next = rit;
-               rit_next++;
-               write = read->get_reads_from();
-               if (rit_next != path->rend()) {
-                       next_read = *rit_next;
-                       if (write != next_read) {
-                               return false;
-                       }
-               }
-       }
-       return true;
-}
-
-/** Only return those applicable patches in a vector */
-SnapVector<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
deleted file mode 100644 (file)
index e1e27a1..0000000
+++ /dev/null
@@ -1,412 +0,0 @@
-#ifndef _SCFENCE_H
-#define _SCFENCE_H
-#include "traceanalysis.h"
-#include "scanalysis.h"
-#include "hashtable.h"
-#include "memoryorder.h"
-#include "action.h"
-
-#include "wildcard.h"
-#include "patch.h"
-#include "inference.h"
-#include "inferlist.h"
-#include "inferset.h"
-
-#include "model.h"
-#include "cyclegraph.h"
-#include "scgen.h"
-
-#include <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
deleted file mode 100644 (file)
index cfcd0e5..0000000
+++ /dev/null
@@ -1,672 +0,0 @@
-#include "scgen.h"
-       
-SCGenerator::SCGenerator() :
-       execution(NULL),
-       actions(NULL),
-       cvmap(),
-       cyclic(false),
-       badrfset(),
-       lastwrmap(),
-       threadlists(1),
-       dup_threadlists(1),
-       print_always(false),
-       print_buggy(false),
-       print_nonsc(false),
-       stats(new struct sc_statistics),
-       annotationMode(false) {
-}
-
-SCGenerator::~SCGenerator() {
-}
-
-bool SCGenerator::getCyclic() {
-       return cyclic || hasBadRF;
-}
-
-SnapVector<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
deleted file mode 100644 (file)
index a16e6b0..0000000
+++ /dev/null
@@ -1,119 +0,0 @@
-#ifndef _SCGEN_H
-#define _SCGEN_H
-
-#include "hashtable.h"
-#include "memoryorder.h"
-#include "action.h"
-#include "scanalysis.h"
-#include "model.h"
-#include "execution.h"
-#include "threads-model.h"
-#include "clockvector.h"
-#include "sc_annotation.h"
-
-#include <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