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
%.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)
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
#include "model.h"
#include "params.h"
#include "snapshot-interface.h"
-#include "scanalysis.h"
#include "plugins.h"
static void param_defaults(struct model_params *params)
#include "plugins.h"
-#include "scanalysis.h"
-#include "scfence.h"
ModelVector<TraceAnalysis *> * registered_analysis;
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() {
+++ /dev/null
-#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);
-}
+++ /dev/null
-#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
+++ /dev/null
-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)
+++ /dev/null
-#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
+++ /dev/null
-#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);
-}
+++ /dev/null
-#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
+++ /dev/null
-#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);
-}
+++ /dev/null
-#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
+++ /dev/null
-#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;
-}
+++ /dev/null
-#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
+++ /dev/null
-#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()));
- }
-}
+++ /dev/null
-#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
+++ /dev/null
-#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
+++ /dev/null
-#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) ********************/
+++ /dev/null
-#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
+++ /dev/null
-#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;
- }
- }
- }
-}
+++ /dev/null
-#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
projects / c11tester.git / commitdiff