From: Peizhao Ou Date: Mon, 26 Sep 2016 18:00:59 +0000 (-0700) Subject: Add the CDSSpec checker back end X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=17ab7c2fda3a12aab91636c08fba589f7d2040ee;p=model-checker.git Add the CDSSpec checker back end --- diff --git a/Makefile b/Makefile index eb84076..56d0dab 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ include common.mk -SCFENCE_DIR := scfence +SPEC_DIR := spec-analysis OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ @@ -8,7 +8,9 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \ context.o scanalysis.o execution.o plugins.o libannotate.o -CPPFLAGS += -Iinclude -I. -I$(SCFENCE_DIR) +include $(SPEC_DIR)/Makefile + +CPPFLAGS += -Iinclude -I. -I$(SPEC_DIR) LDFLAGS := -ldl -lrt -rdynamic SHARED := -shared @@ -34,28 +36,27 @@ docs: *.c *.cc *.h README.html README.html: README.md $(MARKDOWN) $< > $@ +$(LIB_SO): $(OBJECTS) + $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) malloc.o: malloc.c - $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable - -%.o : %.cc - $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS) - -include $(SCFENCE_DIR)/Makefile + $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPLAGS) -Wno-unused-variable --include $(wildcard $(SCFENCE_DIR)/.*.d) - -$(LIB_SO): $(OBJECTS) - $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) +%.o: %.cc + $(CXX) -MMD -MF $(dir $@).$(notdir $@).d -fPIC -c $< -o $@ $(CPPFLAGS) %.pdf: %.dot dot -Tpdf $< -o $@ --include $(OBJECTS:%=.%.d) +# Replace all the basename with +ALL_DEPS := $(shell echo $(OBJECTS) | sed -E 's/([^ ]*\/)?([^\/ ]*)/\1\.\2.d/g') +-include $(ALL_DEPS) +#-include $(OBJECTS:%=.%.d) + PHONY += clean clean: - rm -f *.o *.so .*.d *.pdf *.dot $(SCFENCE_DIR)/.*.d $(SCFENCE_DIR)/*.o + rm -f *.o *.so $(ALL_DEPS) *.pdf *.dot $(OBJECTS) $(MAKE) -C $(TESTS_DIR) clean PHONY += mrclean diff --git a/action.cc b/action.cc index d4c6253..2e9dece 100644 --- a/action.cc +++ b/action.cc @@ -9,7 +9,6 @@ #include "common.h" #include "threads-model.h" #include "nodestack.h" -#include "wildcard.h" #define ACTION_INITIAL_CLOCK 0 @@ -35,7 +34,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, Thread *thread) : type(type), order(order), - original_order(order), location(loc), value(value), reads_from(NULL), @@ -555,7 +553,7 @@ const char * ModelAction::get_type_str() const case ATOMIC_WAIT: return "wait"; case ATOMIC_NOTIFY_ONE: return "notify one"; case ATOMIC_NOTIFY_ALL: return "notify all"; - case ATOMIC_ANNOTATION: return "annotation"; + case ATOMIC_ANNOTATION: return "atomic annotation"; default: return "unknown type"; }; } diff --git a/action.h b/action.h index c8ad85b..ad3b828 100644 --- a/action.h +++ b/action.h @@ -96,8 +96,6 @@ public: thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } memory_order get_mo() const { return order; } - memory_order get_original_mo() const { return original_order; } - void set_mo(memory_order order) { this->order = order; } void * get_location() const { return location; } modelclock_t get_seq_number() const { return seq_number; } uint64_t get_value() const { return value; } @@ -196,9 +194,6 @@ private: /** @brief The memory order for this operation. */ memory_order order; - /** @brief The original memory order parameter for this operation. */ - memory_order original_order; - /** @brief A pointer to the memory location for this action. */ void *location; diff --git a/common.mk b/common.mk index bc068df..46f7e7c 100644 --- a/common.mk +++ b/common.mk @@ -8,7 +8,9 @@ UNAME := $(shell uname) LIB_NAME := model LIB_SO := lib$(LIB_NAME).so -CPPFLAGS += -Wall -g -O3 +CPPFLAGS += -Wall -O3 -g + +CFLAGS := $(CPPFLAGS) # Mac OSX options ifeq ($(UNAME), Darwin) diff --git a/execution.cc b/execution.cc index 2a7e0da..eaf245d 100644 --- a/execution.cc +++ b/execution.cc @@ -34,7 +34,6 @@ struct model_snapshot_members { too_many_reads(false), no_valid_reads(false), bad_synchronization(false), - bad_sc_read(false), asserted(false) { } @@ -54,7 +53,6 @@ struct model_snapshot_members { bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; - bool bad_sc_read; bool asserted; SNAPSHOTALLOC @@ -204,13 +202,6 @@ void ModelExecution::set_bad_synchronization() priv->bad_synchronization = true; } -/** @brief Alert the model-checker that an incorrectly-ordered - * synchronization was made */ -void ModelExecution::set_bad_sc_read() -{ - priv->bad_sc_read = true; -} - bool ModelExecution::assert_bug(const char *msg) { priv->bugs.push_back(new bug_message(msg)); @@ -1315,12 +1306,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (rf) { if (r_modification_order(act, rf)) updated = true; - if (act->is_seqcst()) { - ModelAction *last_sc_write = get_last_seq_cst_write(act); - if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { - set_bad_sc_read(); - } - } } else if (promise) { if (r_modification_order(act, promise)) updated = true; @@ -1400,8 +1385,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const ptr += sprintf(ptr, "[no valid reads-from]"); if (priv->bad_synchronization) ptr += sprintf(ptr, "[bad sw ordering]"); - if (priv->bad_sc_read) - ptr += sprintf(ptr, "[bad sc read]"); if (promises_expired()) ptr += sprintf(ptr, "[promise expired]"); if (promises.size() != 0) @@ -1432,7 +1415,6 @@ bool ModelExecution::is_infeasible() const priv->no_valid_reads || priv->too_many_reads || priv->bad_synchronization || - priv->bad_sc_read || priv->hard_failed_promise || promises_expired(); } @@ -1601,6 +1583,9 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; + // FIXME: The read from promise might read from an annotation + if (act->get_type() == ATOMIC_ANNOTATION) + continue; /* Skip curr */ if (act == curr) @@ -1634,6 +1619,12 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) } } + /* C++, Section 29.3 statement 3 (second subpoint) */ + if (curr->is_seqcst() && last_sc_write && act == last_sc_write) { + added = mo_graph->addEdge(act, rf) || added; + break; + } + /* * Include at most one act per-thread that "happens * before" curr @@ -1765,10 +1756,9 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectoraddEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going - if (act->get_reads_from() == NULL) { - added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added; - } else - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + if (act->get_reads_from() == NULL) + continue; + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && diff --git a/execution.h b/execution.h index 9322f55..fd117ab 100644 --- a/execution.h +++ b/execution.h @@ -117,11 +117,11 @@ public: action_list_t * get_action_trace() { return &action_trace; } CycleGraph * const get_mo_graph() { return mo_graph; } + + int get_execution_number() const; SNAPSHOTALLOC private: - int get_execution_number() const; - ModelChecker *model; const model_params * const params; @@ -134,7 +134,6 @@ private: bool mo_may_allow(const ModelAction *writer, const ModelAction *reader); bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const; void set_bad_synchronization(); - void set_bad_sc_read(); bool promises_expired() const; bool should_wake_up(const ModelAction *curr, const Thread *thread) const; void wake_up_sleeping_actions(ModelAction *curr); diff --git a/impatomic.cc b/impatomic.cc index 4b5d1c2..2d48989 100644 --- a/impatomic.cc +++ b/impatomic.cc @@ -26,15 +26,11 @@ void atomic_flag_clear_explicit void atomic_flag_clear( volatile atomic_flag* __a__ ) { atomic_flag_clear_explicit( __a__, memory_order_seq_cst ); } -void __atomic_flag_wait__( volatile atomic_flag* __a__ ) { - while ( atomic_flag_test_and_set( __a__ ) ) - ; -} +void __atomic_flag_wait__( volatile atomic_flag* __a__ ) +{ while ( atomic_flag_test_and_set( __a__ ) ); } void __atomic_flag_wait_explicit__( volatile atomic_flag* __a__, - memory_order __x__ ) { - while ( atomic_flag_test_and_set_explicit( __a__, __x__ )) - ; -} + memory_order __x__ ) +{ while ( atomic_flag_test_and_set_explicit( __a__, __x__ ) ); } } diff --git a/include/cdsannotate.h b/include/cdsannotate.h index bb6e3d6..b58486d 100644 --- a/include/cdsannotate.h +++ b/include/cdsannotate.h @@ -2,6 +2,13 @@ #define CDS_ANNOTATE_H #include +//#ifdef __cplusplus +//extern "C" { +//#endif void cdsannotate(uint64_t analysistype, void *annotation); +//#ifdef __cplusplus +//} +//#endif + #endif diff --git a/include/impatomic.h b/include/impatomic.h index b4273ee..1b9ce6b 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -2330,28 +2330,23 @@ inline bool atomic_compare_exchange_strong inline void* atomic_fetch_add_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) { - volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); - __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); - __typeof__((__a__)->__f__) __copy__= __old__; - __copy__ = (void *) (((char *)__copy__) + __m__); - model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); - return __old__; -} + void* volatile* __p__ = &((__a__)->__f__); + void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__); + model_rmw_action((void *)__p__, __x__, (uint64_t) ((char*)(*__p__) + __m__)); + return __r__; } - inline void* atomic_fetch_add +inline void* atomic_fetch_add ( volatile atomic_address* __a__, ptrdiff_t __m__ ) { return atomic_fetch_add_explicit( __a__, __m__, memory_order_seq_cst ); } inline void* atomic_fetch_sub_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) -{ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); - __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); - __typeof__((__a__)->__f__) __copy__= __old__; - __copy__ = (void *) (((char *)__copy__) - __m__); - model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); - return __old__; -} +{ + void* volatile* __p__ = &((__a__)->__f__); + void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__); + model_rmw_action((void *)__p__, __x__, (uint64_t)((char*)(*__p__) - __m__)); + return __r__; } inline void* atomic_fetch_sub ( volatile atomic_address* __a__, ptrdiff_t __m__ ) diff --git a/include/model_memory.h b/include/model_memory.h new file mode 100644 index 0000000..bb5a001 --- /dev/null +++ b/include/model_memory.h @@ -0,0 +1,25 @@ +#ifndef _MODEL_MEMORY_H +#define _MODEL_MEMORY_H + +#ifdef __cplusplus +extern "C" { +#endif + +void* snapshot_malloc(size_t size); +void* snapshot_calloc(size_t count, size_t size); +void snapshot_free(void *ptr); + +#define MODEL_MALLOC(x) snapshot_malloc((x)) +#define MODEL_CALLOC(x, y) snapshot_calloc((x), (y)) +#define MODEL_FREE(x) snapshot_free((x)) + +#define CMODEL_MALLOC(x) snapshot_malloc((x)) +#define CMODEL_CALLOC(x, y) snapshot_calloc((x), (y)) +#define CMODEL_FREE(x) snapshot_free((x)) + +#ifdef __cplusplus +} /* extern "C" */ +#endif + + +#endif diff --git a/include/stdatomic.h b/include/stdatomic.h index d4d2198..a5038ff 100644 --- a/include/stdatomic.h +++ b/include/stdatomic.h @@ -56,6 +56,38 @@ using std::atomic_ullong; using std::atomic_wchar_t; +/****** More atomic types *****/ +using std::atomic_int_least8_t; +using std::atomic_uint_least8_t; +using std::atomic_int_least16_t; +using std::atomic_uint_least16_t; +using std::atomic_int_least32_t; +using std::atomic_uint_least32_t; +using std::atomic_int_least64_t; +using std::atomic_uint_least64_t; + +using std::atomic_int_fast8_t; +using std::atomic_uint_fast8_t; +using std::atomic_int_fast16_t; +using std::atomic_uint_fast16_t; +using std::atomic_int_fast32_t; +using std::atomic_uint_fast32_t; +using std::atomic_int_fast64_t; +using std::atomic_uint_fast64_t; + +using std::atomic_intptr_t; +using std::atomic_uintptr_t; + +using std::atomic_ssize_t; +using std::atomic_size_t; + +using std::atomic_ptrdiff_t; + +using std::atomic_intmax_t; +using std::atomic_uintmax_t; + + + using std::atomic; using std::memory_order; using std::memory_order_relaxed; diff --git a/main.cc b/main.cc index 0d1fa1c..127ffd1 100644 --- a/main.cc +++ b/main.cc @@ -141,9 +141,9 @@ static void parse_options(struct model_params *params, int argc, char **argv) {"enabled", required_argument, NULL, 'e'}, {"bound", required_argument, NULL, 'b'}, {"verbose", optional_argument, NULL, 'v'}, - {"uninitialized", required_argument, NULL, 'u'}, - {"analysis", required_argument, NULL, 't'}, - {"options", required_argument, NULL, 'o'}, + {"uninitialized", optional_argument, NULL, 'u'}, + {"analysis", optional_argument, NULL, 't'}, + {"options", optional_argument, NULL, 'o'}, {"maxexecutions", required_argument, NULL, 'x'}, {0, 0, 0, 0} /* Terminator */ }; @@ -231,8 +231,6 @@ static void install_trace_analyses(ModelExecution *execution) TraceAnalysis * ta=(*installedanalysis)[i]; ta->setExecution(execution); model->add_trace_analysis(ta); - /** Call the installation event for each installed plugin */ - ta->actionAtInstallation(); } } diff --git a/model.cc b/model.cc index 3bac903..8f0efcd 100644 --- a/model.cc +++ b/model.cc @@ -2,7 +2,6 @@ #include #include #include -#include #include "model.h" #include "action.h" @@ -23,18 +22,14 @@ ModelChecker *model; ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ params(params), - restart_flag(false), - exit_flag(false), scheduler(new Scheduler()), node_stack(new NodeStack()), execution(new ModelExecution(this, &this->params, scheduler, node_stack)), execution_number(1), diverge(NULL), earliest_diverge(NULL), - trace_analyses(), - inspect_plugin(NULL) + trace_analyses() { - memset(&stats,0,sizeof(struct execution_stats)); } /** @brief Destructor */ @@ -303,9 +298,6 @@ bool ModelChecker::next_execution() checkDataRaces(); run_trace_analyses(); - } else if (inspect_plugin && !execution->is_complete_execution() && - (execution->too_many_steps())) { - inspect_plugin->analyze(execution->get_action_trace()); } record_stats(); @@ -319,14 +311,6 @@ bool ModelChecker::next_execution() if (complete) earliest_diverge = NULL; - if (restart_flag) { - do_restart(); - return true; - } - - if (exit_flag) - return false; - if ((diverge = execution->get_next_backtrack()) == NULL) return false; @@ -346,8 +330,10 @@ bool ModelChecker::next_execution() /** @brief Run trace analyses on complete trace */ void ModelChecker::run_trace_analyses() { + IN_TRACE_ANALYSIS = true; for (unsigned int i = 0; i < trace_analyses.size(); i++) trace_analyses[i]->analyze(execution->get_action_trace()); + IN_TRACE_ANALYSIS = false; } /** @@ -400,9 +386,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) Thread *old = thread_current(); scheduler->set_current_thread(NULL); ASSERT(!old->get_pending()); - if (inspect_plugin != NULL) { - inspect_plugin->inspectModelAction(act); - } old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); @@ -432,35 +415,9 @@ bool ModelChecker::should_terminate_execution() return false; } -/** @brief Exit ModelChecker upon returning to the run loop of the - * model checker. */ -void ModelChecker::exit_model_checker() -{ - exit_flag = true; -} - -/** @brief Restart ModelChecker upon returning to the run loop of the - * model checker. */ -void ModelChecker::restart() -{ - restart_flag = true; -} - -void ModelChecker::do_restart() -{ - restart_flag = false; - diverge = NULL; - earliest_diverge = NULL; - reset_to_initial_state(); - node_stack->full_reset(); - memset(&stats,0,sizeof(struct execution_stats)); - execution_number = 1; -} - /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { - bool has_next; do { thrd_t user_thread; Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); @@ -508,17 +465,7 @@ void ModelChecker::run() t = execution->take_step(curr); } while (!should_terminate_execution()); - has_next = next_execution(); - if (inspect_plugin != NULL && !has_next) { - inspect_plugin->actionAtModelCheckingFinish(); - // Check if the inpect plugin set the restart flag - if (restart_flag) { - model_print("******* Model-checking RESTART: *******\n"); - has_next = true; - do_restart(); - } - } - } while (has_next); + } while (next_execution()); execution->fixup_release_sequences(); diff --git a/model.h b/model.h index 9448353..74cb4e1 100644 --- a/model.h +++ b/model.h @@ -47,15 +47,6 @@ public: void run(); - /** Restart the model checker, intended for pluggins. */ - void restart(); - - /** Exit the model checker, intended for pluggins. */ - void exit_model_checker(); - - /** Check the exit_flag. */ - bool get_exit_flag() const { return exit_flag; } - /** @returns the context for the main model-checking system thread */ ucontext_t * get_system_context() { return &system_context; } @@ -75,15 +66,12 @@ public: void assert_user_bug(const char *msg); const model_params params; - void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } - void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } + void add_trace_analysis(TraceAnalysis *a) { + trace_analyses.push_back(a); + } + MEMALLOC private: - /** Flag indicates whether to restart the model checker. */ - bool restart_flag; - /** Flag indicates whether to exit the model checker. */ - bool exit_flag; - /** The scheduler to use: tracks the running/ready Threads */ Scheduler * const scheduler; NodeStack * const node_stack; @@ -109,10 +97,6 @@ private: ModelVector trace_analyses; - /** @bref Implement restart. */ - void do_restart(); - /** @bref Plugin that can inspect new actions. */ - TraceAnalysis *inspect_plugin; /** @brief The cumulative execution stats */ struct execution_stats stats; void record_stats(); diff --git a/mymemory.cc b/mymemory.cc index 4182e09..8bb5b46 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -13,6 +13,8 @@ #define REQUESTS_BEFORE_ALLOC 1024 +bool IN_TRACE_ANALYSIS = false; + size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 }; int nextRequest = 0; int howManyFreed = 0; @@ -124,7 +126,7 @@ void model_free(void *ptr) /** Bootstrap allocation. Problem is that the dynamic linker calls require * calloc to work and calloc requires the dynamic linker to work. */ -#define BOOTSTRAPBYTES 131072 +#define BOOTSTRAPBYTES 4096 char bootstrapmemory[BOOTSTRAPBYTES]; size_t offset = 0; @@ -134,7 +136,7 @@ void * HandleEarlyAllocationRequest(size_t sz) sz = (sz + 7) & ~7; if (sz > (BOOTSTRAPBYTES-offset)) { - model_print("OUT OF BOOTSTRAP MEMORY. Increase the size of BOOTSTRAPBYTES in mymemory.cc\n"); + model_print("OUT OF BOOTSTRAP MEMORY\n"); exit(EXIT_FAILURE); } @@ -180,7 +182,7 @@ void *malloc(size_t size) { if (user_snapshot_space) { /* Only perform user allocations from user context */ - ASSERT(!model || thread_current()); + ASSERT(!model || thread_current() || IN_TRACE_ANALYSIS); return user_malloc(size); } else return HandleEarlyAllocationRequest(size); diff --git a/mymemory.h b/mymemory.h index a62ab83..461f7d1 100644 --- a/mymemory.h +++ b/mymemory.h @@ -47,14 +47,30 @@ return p; \ } +#ifdef __cplusplus +extern "C" { +#endif + +extern bool IN_TRACE_ANALYSIS; + void *model_malloc(size_t size); void *model_calloc(size_t count, size_t size); void model_free(void *ptr); +#ifdef __cplusplus +} /* extern "C" */ +#endif + +#ifdef __cplusplus +extern "C" { +#endif void * snapshot_malloc(size_t size); void * snapshot_calloc(size_t count, size_t size); void * snapshot_realloc(void *ptr, size_t size); void snapshot_free(void *ptr); +#ifdef __cplusplus +} /* extern "C" */ +#endif void * Thread_malloc(size_t size); void Thread_free(void *ptr); diff --git a/nodestack.cc b/nodestack.cc index bacd067..e5f4687 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -838,16 +838,6 @@ void NodeStack::pop_restofstack(int numAhead) node_list.back()->clear_backtracking(); } -/** Reset the node stack. */ -void NodeStack::full_reset() -{ - for (unsigned int i = 0; i < node_list.size(); i++) - delete node_list[i]; - node_list.clear(); - reset_execution(); - total_nodes = 1; -} - Node * NodeStack::get_head() const { if (node_list.empty() || head_idx < 0) diff --git a/nodestack.h b/nodestack.h index 6ae96be..f26100b 100644 --- a/nodestack.h +++ b/nodestack.h @@ -198,7 +198,6 @@ public: Node * get_next() const; void reset_execution(); void pop_restofstack(int numAhead); - void full_reset(); int get_total_nodes() { return total_nodes; } void print() const; diff --git a/params.h b/params.h index d5fd1cb..c5b617b 100644 --- a/params.h +++ b/params.h @@ -14,7 +14,7 @@ struct model_params { unsigned int enabledcount; unsigned int bound; unsigned int uninitvalue; - int maxexecutions; + unsigned int maxexecutions; /** @brief Maximum number of future values that can be sent to the same * read */ diff --git a/plugins.cc b/plugins.cc index 38493de..f3852bb 100644 --- a/plugins.cc +++ b/plugins.cc @@ -1,6 +1,6 @@ #include "plugins.h" #include "scanalysis.h" -#include "scfence.h" +#include "specanalysis.h" ModelVector * registered_analysis; ModelVector * installed_analysis; @@ -9,7 +9,7 @@ void register_plugins() { registered_analysis=new ModelVector(); installed_analysis=new ModelVector(); registered_analysis->push_back(new SCAnalysis()); - registered_analysis->push_back(new SCFence()); + registered_analysis->push_back(new SPECAnalysis()); } ModelVector * getRegisteredTraceAnalysis() { diff --git a/scfence/scfence.cc b/scfence/scfence.cc index 130dc3b..63408cb 100644 --- a/scfence/scfence.cc +++ b/scfence/scfence.cc @@ -35,7 +35,7 @@ void SCFence::setExecution(ModelExecution * execution) { } const char * SCFence::name() { - const char * name = "AUTOMO"; + const char * name = "SCFENCE"; return name; } diff --git a/spec-analysis/.gitignore b/spec-analysis/.gitignore new file mode 100644 index 0000000..e3b3c9f --- /dev/null +++ b/spec-analysis/.gitignore @@ -0,0 +1,12 @@ +# generic types +*.o +*.swp +*.swo +*.so +*~ +*.dot +.*.d +*.pdf + +# files in this directory +/tags diff --git a/spec-analysis/Makefile b/spec-analysis/Makefile new file mode 100644 index 0000000..02c24e9 --- /dev/null +++ b/spec-analysis/Makefile @@ -0,0 +1,7 @@ +# This make file is to be added by the Makefile at the main directory + +LOCAL_OBJS := specanalysis.o executiongraph.o specannotation.o methodcall.o + +SPEC_OBJS := $(LOCAL_OBJS:%=$(SPEC_DIR)/%) + +OBJECTS += $(SPEC_OBJS) diff --git a/spec-analysis/cdsspec.h b/spec-analysis/cdsspec.h new file mode 100644 index 0000000..db06189 --- /dev/null +++ b/spec-analysis/cdsspec.h @@ -0,0 +1,376 @@ +#ifndef _CDSSPEC_H +#define _CDSSPEC_H + +#include +#include +#include +#include +#include +#include +#include + +#include + +#include + +#include "mymemory.h" +//#include "common.h" +#include "methodcall.h" + +using namespace std; + +/** Macro for output (stole from common.h) */ +extern int model_out; +#define PRINT(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0) + +/** + A special kind of integer that has been embedded with a universal tag (ID) +*/ +typedef struct TagInt { + unsigned int tag; + int val; + + TagInt(unsigned int tag, int val) : tag(tag), val(val) { } + + TagInt(int val) : tag(0), val(val) { } +}TagInt; + +typedef SnapVector IntVector; +typedef SnapList IntList; +typedef SnapSet IntSet; + +template +class Map: public unordered_map { + public: + typedef unordered_map map; + + Map() : map() { } + + Value get(Key key) { + return (*this)[key]; + } + + void put(Key key, Value value) { + (*this)[key] = value; + } + + SNAPSHOTALLOC +}; + +class IntMap : public unordered_map { + public: + typedef unordered_map map; + + IntMap() : map() { } + + int get(int key) { + return (*this)[key]; + } + + void put(int key, int value) { + (*this)[key] = value; + } + + SNAPSHOTALLOC +}; + +typedef SnapVector DoubleVector; +typedef SnapList DoubleList; +typedef SnapSet DoubleSet; + +/********** Debugging functions **********/ +template +inline void printContainer(Container *container) { + if (!container || container->size() == 0) + PRINT("EMPTY"); + for (auto it = container->begin(); it != container->end(); it++) { + int item = *it; + PRINT("%d ", item); + } +} + +inline void printMap(IntMap *container) { + if (!container || container->size() == 0) + PRINT("EMPTY"); + for (auto it = container->begin(); it != container->end(); it++) { + pair item = *it; + PRINT("(%d, %d) ", item.first, item.second); + } +} + +/********** More general specification-related types and operations **********/ + +#define NewMethodSet new SnapSet + +#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */ +#define CAT_HELPER(a, b) a ## b +#define X(name) CAT(__##name, __LINE__) /* unique variable */ + +/** + This is a generic ForEach primitive for all the containers that support + using iterator to iterate. +*/ +#define ForEach(item, container) \ + auto X(_container) = (container); \ + auto X(iter) = X(_container)->begin(); \ + for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \ + X(_container)->end()) ? *X(iter) : 0) + +/** + This is a common macro that is used as a constant for the name of specific + variables. We basically have two usage scenario: + 1. In Subset operation, we allow users to specify a condition to extract a + subset. In that condition expression, we provide NAME, RET(type), ARG(type, + field) and STATE(field) to access each item's (method call) information. + 2. In general specification (in pre- & post- conditions and side effects), + we would automatically generate an assignment that assign the current + MethodCall* pointer to a variable namedd _M. With this, when we access the + state of the current method, we use STATE(field) (this is a reference + for read/write). +*/ +#define ITEM _M +#define _M ME + +#define S_RET __value->S_RET + +/** + This operation is specifically for Method set. For example, when we want to + construct an integer set from the state field "x" (which is an + integer) of the previous set of method calls (PREV), and the new set goes to + "readSet", we would call "MakeSet(int, PREV, readSet, STATE(x));". Then users + can use the "readSet" as an integer set (set) +*/ +#define MakeSet(type, oldset, newset, field) \ + auto newset = new SnapSet; \ + ForEach (_M, oldset) \ + newset->insert(field); \ + +/** + We provide a more general subset operation that takes a plain boolean + expression on each item (access by the name "ITEM") of the set, and put it + into a new set if the boolean expression (Guard) on that item holds. This is + used as the second arguments of the Subset operation. An example to extract + a subset of positive elements on an IntSet "s" would be "Subset(s, + GeneralGuard(int, ITEM > 0))" +*/ +#define GeneralGuard(type, expression) std::function \ + ([&](type ITEM) -> bool { return (expression);}) \ + +/** + This is a more specific guard designed for the Method (MethodCall*). It + basically wrap around the GeneralGuard with the type Method. An example to + extract the subset of method calls in the PREV set whose state "x" is + equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))" +*/ +#define Guard(expression) GeneralGuard(Method, expression) + +#define MostRecent(guard) mostRecent(_M, guard) + +/** + A general subset operation that takes a condition and returns all the item + for which the boolean guard holds. +*/ +inline SnapSet* mostRecent(Method method, std::function condition) { + SnapSet *res = new SnapSet; + // A list of potential nodes that are most recent + MethodList *toCheckList = new MethodList; + MethodSet prev = method->prev; + if (prev->empty()) // method is START node + return res; + else { + ForEach (_M, prev) + toCheckList->push_back(_M); + } + // Searching loop + while (!toCheckList->empty()) { + Method _M = toCheckList->front(); + toCheckList->pop_front(); + + if (condition(_M)) { + bool recencyFlag = true; + ForEach (m, res) { + if (MethodCall::belong(_M->allNext, m)) { + recencyFlag = false; + break; + } + } + if (recencyFlag) + res->insert(_M); + } + else { // Not what we want, keep going up the graph + prev = _M->prev; + if (!prev->empty()) { + ForEach (_M, prev) + toCheckList->push_back(_M); + } + } + } + return res; +} + + +/** + A general subset operation that takes a condition and returns all the item + for which the boolean guard holds. +*/ +template +inline SnapSet* Subset(SnapSet *original, std::function condition) { + SnapSet *res = new SnapSet; + ForEach (_M, original) { + if (condition(_M)) + res->insert(_M); + } + return res; +} + +/** + A general set operation that takes a condition and returns if there exists + any item for which the boolean guard holds. +*/ +template +inline bool HasItem(SnapSet *original, std::function condition) { + ForEach (_M, original) { + if (condition(_M)) + return true; + } + return false; +} + + + +/** + A general sublist operation that takes a condition and returns all the item + for which the boolean guard holds in the same order as in the old list. +*/ +template +inline list* Sublist(list *original, std::function condition) { + list *res = new list; + ForEach (_M, original) { + if (condition(_M)) + res->push_back(_M); + } + return res; +} + +/** + A general subvector operation that takes a condition and returns all the item + for which the boolean guard holds in the same order as in the old vector. +*/ +template +inline vector* Subvector(vector *original, std::function condition) { + vector *res = new vector; + ForEach (_M, original) { + if (condition(_M)) + res->push_back(_M); + } + return res; +} + +/** General for set, list & vector */ +#define Size(container) ((container)->size()) + +#define _BelongHelper(type) \ + template \ + inline bool Belong(type *container, T item) { \ + return std::find(container->begin(), \ + container->end(), item) != container->end(); \ + } + +_BelongHelper(SnapSet) +_BelongHelper(SnapVector) +_BelongHelper(SnapList) + +/** General set operations */ +template +inline SnapSet* Intersect(SnapSet *set1, SnapSet *set2) { + SnapSet *res = new SnapSet; + ForEach (item, set1) { + if (Belong(set2, item)) + res->insert(item); + } + return res; +} + +template +inline SnapSet* Union(SnapSet *s1, SnapSet *s2) { + SnapSet *res = new SnapSet(*s1); + ForEach (item, s2) + res->insert(item); + return res; +} + +template +inline SnapSet* Subtract(SnapSet *set1, SnapSet *set2) { + SnapSet *res = new SnapSet; + ForEach (item, set1) { + if (!Belong(set2, item)) + res->insert(item); + } + return res; +} + +template +inline void Insert(SnapSet *s, T item) { s->insert(item); } + +template +inline void Insert(SnapSet *s, SnapSet *others) { + ForEach (item, others) + s->insert(item); +} + +/* +inline MethodSet MakeSet(int count, ...) { + va_list ap; + MethodSet res; + + va_start (ap, count); + res = NewMethodSet; + for (int i = 0; i < count; i++) { + Method item = va_arg (ap, Method); + res->insert(item); + } + va_end (ap); + return res; +} +*/ + +/********** Method call related operations **********/ +#define Id(method) method->id +#define ID Id(_M) + +#define Name(method) method->name +#define NAME Name(_M) + +#define StructName(type) __struct_ ## type ## __ +#define Value(method, type, field) ((StructName(type)*) method->value)->field +#define Ret(method, type) Value(method, type, RET) +#define CRet(method, type) Value(method, type, C_RET) +#define Arg(method, type, arg) Value(method, type, arg) + +#define VALUE(type, field) Value(_M, type, field) +#define RET(type) VALUE(type, RET) +#define C_RET(type) VALUE(type, C_RET) +#define ARG(type, arg) VALUE(type, arg) + +#define State(method, field) ((StateStruct*) method->state)->field +#define STATE(field) State(_M, field) + +#define Prev(method) method->prev +#define PREV _M->prev + +#define Next(method) method->next +#define NEXT _M->next + +#define Concurrent(method) method->concurrent +#define CONCURRENT _M->concurrent + +#define AllPrev(method) method->allPrev +#define ALLPREV _M->allPrev + +#define AllNext(method) method->allNext +#define ALLNEXT _M->allNext + +/***************************************************************************/ +/***************************************************************************/ + +#endif diff --git a/spec-analysis/executiongraph.cc b/spec-analysis/executiongraph.cc new file mode 100644 index 0000000..fddd345 --- /dev/null +++ b/spec-analysis/executiongraph.cc @@ -0,0 +1,1611 @@ +#include +#include "executiongraph.h" +#include "action.h" +#include "cyclegraph.h" +#include "threads-model.h" +#include "clockvector.h" +#include "execution.h" +#include +#include +#include +#include "modeltypes.h" +#include "model-assert.h" +#include "time.h" + +/******************** PotentialOP ********************/ +PotentialOP::PotentialOP(ModelAction *op, CSTR label) : + operation(op), + label(label) +{ + +} + + +/******************** ExecutionGraph ********************/ +/********* ExecutionGraph (public functions) **********/ +/** + Initialze the necessary fields +*/ +ExecutionGraph::ExecutionGraph(ModelExecution *e, bool allowCyclic) : execution(e), allowCyclic(allowCyclic) { + methodList = new MethodList; + randomHistory = NULL; + + broken = false; + noOrderingPoint = false; + cyclic = false; + threadLists = new SnapVector; +} + +void ExecutionGraph::buildGraph(action_list_t *actions) { + buildThreadLists(actions); + + // First process the initialization annotation + bool hasInitAnno = false; + action_list_t::iterator iter = actions->begin(); + for (; iter != actions->end(); iter++) { + ModelAction *act = *iter; + SpecAnnotation *anno = getAnnotation(act); + if (!anno) + continue; + // Deal with the Initialization annotation + if (anno->type == INIT) { + hasInitAnno = true; + AnnoInit *annoInit = (AnnoInit*) anno->annotation; + processInitAnnotation(annoInit); + break; + } + } + if (!hasInitAnno) { + model_print("There is no initialization annotation\n"); + broken = true; + return; + } + + // Process the nodes for method calls of each thread + buildNodesFromThreads(); + // Establish the edges + buildEdges(); +} + +bool ExecutionGraph::isBroken() { + return broken; +} + +bool ExecutionGraph::isNoOrderingPoint() { + return noOrderingPoint; +} + +bool ExecutionGraph::hasCycle() { + if (cyclic) + return true; + if (randomHistory) + return false; + randomHistory = generateOneRandomHistory(); + return cyclic; +} + +void ExecutionGraph::resetBroken() { + broken = false; +} + +bool ExecutionGraph::checkAdmissibility() { + MethodList::iterator iter1, iter2; + bool admissible = true; + for (iter1 = methodList->begin(); iter1 != methodList->end(); iter1++) { + Method m1 = *iter1; + iter1++; + iter2 = iter1; + iter1--; + for (; iter2 != methodList->end(); iter2++) { + Method m2 = *iter2; + if (isReachable(m1, m2) || isReachable(m2, m1)) + continue; + + /* Now we need to check whether we have a commutativity rule that + * says the two method calls should be ordered */ + bool commute = true; + for (int i = 0; i < commuteRuleNum; i++) { + CommutativityRule rule = *(commuteRules + i); + /* Check whether condition is satisfied */ + if (!rule.isRightRule(m1, m2)) // Not this rule + continue; + else + commute = rule.checkCondition(m1, m2); + if (!commute) // The rule requires them to be ordered + break; + } + // We have a rule that require m1 and m2 to be ordered + if (!commute) { + admissible = false; + model_print("These two nodes should not commute:\n"); + model_print("\t"); + ModelAction *begin1 = m1->begin; + ModelAction *begin2 = m2->begin; + int tid1 = id_to_int(begin1->get_tid()); + int tid2 = id_to_int(begin2->get_tid()); + model_print("%s_%d (T%d)", m1->name, + begin1->get_seq_number(), tid1); + model_print(" <-> "); + model_print("%s_%d (T%d)", m2->name, + begin2->get_seq_number(), tid2); + model_print("\n"); + } + } + } + + return admissible; +} + +/** Checking cyclic graph specification */ +bool ExecutionGraph::checkCyclicGraphSpec(bool verbose) { + if (verbose) { + model_print("---- Start to check cyclic graph ----\n"); + } + + bool pass = false; + for (MethodList::iterator it = methodList->begin(); it != methodList->end(); + it++) { + Method m = *it; + if (isFakeMethod(m)) + continue; + + StateFunctions *funcs = NULL; + if (verbose) { + m->print(false, false); + model_print("\n"); + + funcs = funcMap->get(m->name); + ASSERT (funcs); + UpdateState_t printValue = (UpdateState_t) funcs->print->function; + if (printValue) { + model_print("\t********** Value Info **********\n"); + (*printValue)(m); + } + } + + // Cyclic graph only supports @PreCondition + funcs = funcMap->get(m->name); + ASSERT (funcs); + CheckState_t preCondition = (CheckState_t) + funcs->preCondition->function; + + // @PreCondition of Mehtod m + if (preCondition) { + pass = (*preCondition)(m, m); + + if (!pass) { + model_print("PreCondition is not satisfied. Problematic method" + " is as follow: \n"); + m->print(true, true); + if (verbose) { + model_print("---- Check cyclic graph END ----\n\n"); + } + return false; + } + } + } + + if (!pass) { + // Print out the graph + model_print("Problmatic execution graph: \n"); + print(true); + } else if (verbose) { + // Print out the graph in verbose + model_print("Execution graph: \n"); + print(true); + } + + if (verbose) { + model_print("---- Check cyclic graph END ----\n\n"); + } + return true; +} + + + + +/** To check "num" random histories */ +bool ExecutionGraph::checkRandomHistories(int num, bool stopOnFail, bool verbose) { + ASSERT (!cyclic); + bool pass = true; + int i; + for (i = 0; i < num; i++) { + MethodList *history = generateOneRandomHistory(); + pass &= checkStateSpec(history, verbose, i + 1); + if (!pass) { + // Print out the graph + model_print("Problmatic execution graph: \n"); + print(); + if (stopOnFail) { // Just stop on this + // Recycle + delete history; + if (verbose) + model_print("We totally checked %d histories.\n", i + 1); + return false; + } + } else if (verbose) { + // Print out the graph in verbose + model_print("Execution graph: \n"); + print(); + } + // Recycle + delete history; + } + + if (verbose) + model_print("We totally checked %d histories.\n", i); + return pass; +} + + +/** + To generate and check all possible histories. + + If stopOnFailure is true, we stop generating any history and end the + checking process. Verbose flag controls how the checking process is exposed. +*/ +bool ExecutionGraph::checkAllHistories(bool stopOnFailure, bool verbose) { + ASSERT (!cyclic); + MethodList *curList = new MethodList; + int numLiveNodes = methodList->size(); + int historyIndex = 1; + if (verbose) { + // Print out the graph in verbose + print(); + } + + // FIXME: make stopOnFailure always true + stopOnFailure = true; + bool pass = checkAllHistoriesHelper(curList, numLiveNodes, historyIndex, + stopOnFailure, verbose); + if (pass) { + for (MethodList::iterator it = methodList->begin(); it != + methodList->end(); it++) { + Method m = *it; + if (isFakeMethod(m)) + continue; + if (!m->justified) { + model_print("\t"); + m->print(false, false); + model_print(": unjustified\n"); + pass = false; + break; + } + } + } + + if (!pass && !verbose) { + // Print out the graph + print(); + } + if (verbose) + model_print("We totally checked %d histories.\n", historyIndex - 1); + return pass; +} + + +/********** Several public printing functions (ExecutionGraph) **********/ + +void ExecutionGraph::printOneHistory(MethodList *history, CSTR header) { + model_print("------------- %s (exec #%d) -------------\n", header, + execution->get_execution_number()); + int idx = 1; + for (MethodList::iterator it = history->begin(); it != history->end(); it++) { + Method m = *it; + model_print("%d. ", idx++); + m->print(false); + } + model_print("------------- %s (exec #%d) (end) -------------\n", + header, execution->get_execution_number()); +} + +void ExecutionGraph::printAllHistories(MethodListVector *histories) { + model_print("------------- All histories (exec #%d) -------------\n", + execution->get_execution_number()); + for (unsigned i = 0; i < histories->size(); i++) { + model_print("*********************** # %d ***********************\n", i + 1); + MethodList *history = (*histories)[i]; + int idx = 1; + for (MethodList::iterator it = history->begin(); it != history->end(); + it++) { + Method m = *it; + model_print("%d. ", idx++); + m->print(false); + } + if (i != histories->size() - 1) + model_print("\n"); + } + model_print("------------- All histories (exec #%d) (end) " + "-------------\n\n", execution->get_execution_number()); +} + +/** + By default we print only all the edges that are directly from this mehtod + call node. If passed allEdges == true, we will print all the edges that are + reachable (SC/hb after) the current node. +*/ +void ExecutionGraph::print(bool allEdges) { + model_print("\n"); + const char *extraStr = allEdges ? "All Edges" : ""; + model_print("------------------ Execution Graph -- %s (exec #%d)" + " ------------------\n", extraStr, execution->get_execution_number()); + for (MethodList::iterator iter = methodList->begin(); iter != + methodList->end(); iter++) { + Method m = *iter; + /* Print the info the this method */ + m->print(false); + /* Print the info the edges directly from this node */ + SnapSet *theSet = allEdges ? m->allNext : m->next; + for (SnapSet::iterator nextIter = theSet->begin(); nextIter != + theSet->end(); nextIter++) { + Method next = *nextIter; + model_print("\t--> "); + next->print(false); + } + } + model_print("------------------ End Graph (exec #%d)" + " ------------------\n", execution->get_execution_number()); + model_print("\n"); +} + +/** + By default we print only all the edges that are directly to this mehtod + call node. If passed allEdges == true, we will print all the edges that are + reachable (SC/hb before) from the current node. + + Only for debugging!! +*/ +void ExecutionGraph::PrintReverse(bool allEdges) { + model_print("\n"); + const char *extraStr = allEdges ? "All Edges" : ""; + model_print("------------------ Reverse Execution Graph -- %s (exec #%d)" + " ------------------\n", extraStr, execution->get_execution_number()); + for (MethodList::iterator iter = methodList->begin(); iter != + methodList->end(); iter++) { + Method m = *iter; + /* Print the info the this method */ + m->print(false); + /* Print the info the edges directly from this node */ + SnapSet *theSet = allEdges ? m->allPrev : m->prev; + for (SnapSet::iterator prevIter = theSet->begin(); prevIter != + theSet->end(); prevIter++) { + Method prev = *prevIter; + model_print("\t--> "); + prev->print(false); + } + } + model_print("------------------ End Reverse Graph (exec #%d)" + " ------------------\n", execution->get_execution_number()); + model_print("\n"); +} + + +/********** Internal member functions (ExecutionGraph) **********/ + +void ExecutionGraph::buildThreadLists(action_list_t *actions) { + int maxthreads = 0; + for (action_list_t::iterator it = actions->begin(); it != actions->end(); it++) { + ModelAction *act = *it; + int threadid = id_to_int(act->get_tid()); + if (threadid == 0) + continue; + if (threadid > maxthreads) { + threadLists->resize(threadid + 1); + maxthreads = threadid; + } + action_list_t *list = (*threadLists)[threadid]; + if (!list) { + list = new action_list_t; + (*threadLists)[threadid] = list; + } + list->push_back(act); + } +} + +/** + Outside of this function, we have already processed the INIT type of + annotation, and we focus on extracting all the method call nodes in the + current thread list. This routine basically iterates the list, finds the + INTERFACE_BEGIN annotation, call the function extractMethod(), and advance + the iterator. That is to say, we would only see INIT or INTERFACE_BEGIN + annotations; if not, the specification annotations are wrong (we mark the + graph is broken) +*/ +void ExecutionGraph::buildNodesFromThread(action_list_t *actions) { + action_list_t::iterator iter = actions->begin(); + + // FIXME: Just for the purpose of debugging + //printActions(actions, "BuildNodesFromThread"); + + // annoBegin == NULL means we are looking for the beginning annotation + while (iter != actions->end()) { + ModelAction *act = *iter; + SpecAnnotation *anno = getAnnotation(act); + if (!anno) { // Means this is not an annotation action + iter++; + continue; + } + if (anno->type == INTERFACE_BEGIN) { // Interface beginning anno + Method m = extractMethod(actions, iter); + if (m) { + // Get a complete method call node and store it + methodList->push_back(m); + } else { + broken = true; + model_print("Error with constructing a complete node.\n"); + return; + } + } else if (anno->type != INIT) { + broken = true; + model_print("Missing beginning annotation.\n"); + return; + } else { // This is an INIT annotation + iter++; + } + } +} + +void ExecutionGraph::buildNodesFromThreads() { + /* We start from the 1st real thread */ + for (unsigned i = 1; i < threadLists->size(); i++) { + buildNodesFromThread((*threadLists)[i]); + if (broken) // Early exit when detecting errors + return; + } +} + +/** + Find the previous non-annotation model action (ordering point from the + current iterator +*/ +ModelAction* ExecutionGraph::findPrevAction(action_list_t *actions, action_list_t::iterator + iter) { + while (iter != actions->begin()) { + iter--; + ModelAction *res = *iter; + if (res->get_type() != ATOMIC_ANNOTATION) + return res; + } + return NULL; +} + +/** + When called, the current iter points to a beginning annotation; when done, + the iter points to either the end of the list or the next INTERFACE_BEGIN + annotation. +*/ +Method ExecutionGraph::extractMethod(action_list_t *actions, action_list_t::iterator &iter) { + ModelAction *act = *iter; + SpecAnnotation *anno = getAnnotation(act); + ASSERT(anno && anno->type == INTERFACE_BEGIN); + + // Partially initialize the commit point node with the already known fields + AnnoInterfaceInfo *info = (AnnoInterfaceInfo*) anno->annotation; + Method m = new MethodCall(info->name, info->value, act); + + // Some declaration for potential ordering points and its check + CSTR label; + PotentialOP *potentialOP= NULL; + // A list of potential ordering points + PotentialOPList *popList = new PotentialOPList; + // Ordering point operation + ModelAction *op = NULL; + // Whether the potential ordering points were defined + bool hasAppeared = false; + + bool methodComplete = false; + int nestedLevel = 0; + for (iter++; iter != actions->end(); iter++) { + act = *iter; + SpecAnnotation *anno = getAnnotation(act); + if (!anno) + continue; + // Now we are dealing with one annotation + switch (anno->type) { + case POTENTIAL_OP: + //model_print("POTENTIAL_OP\n"); + label = (CSTR) anno->annotation; + op = findPrevAction(actions, iter); + if (!op) { + model_print("Potential ordering point annotation should" + "follow an atomic operation.\n"); + model_print("%s_%d\n", label, + act->get_seq_number()); + broken = true; + return NULL; + } + potentialOP = new PotentialOP(op, label); + popList->push_back(potentialOP); + break; + case OP_CHECK: + //model_print("OP_CHECK\n"); + label = (CSTR) anno->annotation; + // Check if corresponding potential ordering point has appeared. + hasAppeared = false; + // However, in the current version of spec, we take the most + // recent one in the list as the commit point (so we use + // reverse iterator) + for (PotentialOPList::reverse_iterator popIter = popList->rbegin(); + popIter != popList->rend(); popIter++) { + potentialOP = *popIter; + if (label == potentialOP->label) { + m->addOrderingPoint(potentialOP->operation); + hasAppeared = true; + break; // Done when find the "first" PCP + } + } + if (!hasAppeared) { + model_print("Ordering point check annotation should" + "have previous potential ordering point.\n"); + model_print("%s_%d\n", label, + act->get_seq_number()); + broken = true; + return NULL; + } + break; + case OP_DEFINE: + //model_print("CP_DEFINE_CHECK\n"); + op = findPrevAction(actions, iter); + if (!op) { + model_print("Ordering point define should " + "follow an atomic operation.\n"); + act->print(); + broken = true; + return NULL; + } + m->addOrderingPoint(op); + break; + case OP_CLEAR: + //model_print("OP_CLEAR\n"); + // Reset everything + // Clear the list of potential ordering points + popList->clear(); + // Clear the previous list of commit points + m->orderingPoints->clear(); + break; + case OP_CLEAR_DEFINE: + //model_print("OP_CLEAR_DEFINE\n"); + // Reset everything + popList->clear(); + m->orderingPoints->clear(); + // Define the ordering point + op = findPrevAction(actions, iter); + if (!op) { + model_print("Ordering point clear define should " + "follow an atomic operation.\n"); + act->print(); + broken = true; + return NULL; + } + m->addOrderingPoint(op); + break; + case INTERFACE_BEGIN: + nestedLevel++; + break; + case INTERFACE_END: + if (nestedLevel == 0) { + methodComplete = true; + } + else + nestedLevel--; + break; + default: + model_print("Unknown type!! We should never get here.\n"); + ASSERT(false); + return NULL; + } + if (methodComplete) // Get out of the loop when we have a complete node + break; + } + + ASSERT (iter == actions->end() || (getAnnotation(*iter) && + getAnnotation(*iter)->type == INTERFACE_END)); + if (iter != actions->end()) + iter++; + + delete popList; + // XXX: We just allow methods to have no specified ordering points. In that + // case, the method is concurrent with every other method call + if (m->orderingPoints->size() == 0) { + noOrderingPoint = true; + return m; + } else { + // Get a complete method call + return m; + } +} + +/** + A utility function to extract the actual annotation + pointer and return the actual annotation if this is an annotation action; + otherwise return NULL. +*/ +SpecAnnotation* ExecutionGraph::getAnnotation(ModelAction *act) { + if (act->get_type() != ATOMIC_ANNOTATION) + return NULL; + if (act->get_value() != SPEC_ANALYSIS) + return NULL; + SpecAnnotation *anno = (SpecAnnotation*) act->get_location(); + ASSERT (anno); + return anno; +} + +void ExecutionGraph::processInitAnnotation(AnnoInit *annoInit) { + // Assign state initial (and copy) function + NamedFunction *func = annoInit->initial; + ASSERT (func && func->type == INITIAL); + initial= annoInit->initial; + + func = annoInit->final; + ASSERT (func && func->type == FINAL); + final= annoInit->final; + + func = annoInit->copy; + ASSERT (func && func->type == COPY); + copy= annoInit->copy; + + func = annoInit->clear; + ASSERT (func && func->type == CLEAR); + clear= annoInit->clear; + + func = annoInit->printState; + ASSERT (func && func->type == PRINT_STATE); + printState = annoInit->printState; + + // Assign the function map (from interface name to state functions) + funcMap = annoInit->funcMap; + + // Initialize the commutativity rules array and size + commuteRules = annoInit->commuteRules; + commuteRuleNum = annoInit->commuteRuleNum; +} + +/** + After building up the graph (both the nodes and egdes are correctly built), + we also call this function to initialize the most recent justified node of + each method node. + + A justified method node of a method m is a method that is in the allPrev set + of m, and all other nodes in the allPrev set of m are either before or after + it. The most recent justified node is the most recent one in the hb/SC + order. +*/ +void ExecutionGraph::initializeJustifiedNode() { + MethodList::iterator it = methodList->begin(); + // Start from the second methods in the list --- skipping the START node + for (it++; it != methodList->end(); it++) { + Method m = *it; + // Walk all the way up, when we have multiple immediately previous + // choices, pick one and check if that node is a justified node --- its + // concurrent set should be disjoint with the whole set m->allPrev. If + // not, keep going up; otherwise, that node is the most recent justified + // node + + MethodSet prev = NULL; + Method justified = m; + do { + prev = justified->prev; + // At the very least we should have the START nodes + ASSERT (!prev->empty()); + + // setIt points to the very beginning of allPrev set + SnapSet::iterator setIt = prev->begin(); + justified = *setIt; + // Check whether justified is really the justified node + if (MethodCall::disjoint(justified->concurrent, m->allPrev)) + break; + } while (true); + + ASSERT (justified != m); + // Don't forget to set the method's field + m->justifiedMethod = justified; + + // Ensure we reset the justified field to be false in the beginning + m->justified = false; + } +} + + +/** + This is a very important interal function to build the graph. When called, + we assume that we have a list of method nodes built (extracted from the raw + execution), and this routine is responsible for building the connection + edges between them to yield an execution graph for checking +*/ +void ExecutionGraph::buildEdges() { + + MethodList::iterator iter1, iter2; + // First build the allPrev and allNext set (don't care if they are right + // previous or right next first) + for (iter1 = methodList->begin(); iter1 != methodList->end(); iter1++) { + Method m1 = *iter1; + iter1++; + iter2 = iter1; + iter1--; + for (; iter2 != methodList->end(); iter2++) { + Method m2 = *iter2; + int val = conflict(m1, m2); + if (val == 1) { + m1->allNext->insert(m2); + m2->allPrev->insert(m1); + } else if (val == -1) { + m2->allNext->insert(m1); + m1->allPrev->insert(m2); + } else if (val == SELF_CYCLE) { + if (allowCyclic) { + // m1 -> m2 + m1->allNext->insert(m2); + m2->allPrev->insert(m1); + // m2 -> m1 + m2->allNext->insert(m1); + m1->allPrev->insert(m2); + } + } + } + } + + // Initialize two special nodes (START & FINISH) + Method startMethod = new MethodCall(GRAPH_START); + Method finishMethod = new MethodCall(GRAPH_FINISH); + // Initialize startMethod and finishMethd + startMethod->allNext->insert(finishMethod); + finishMethod->allPrev->insert(startMethod); + for (MethodList::iterator iter = methodList->begin(); iter != + methodList->end(); iter++) { + Method m = *iter; + startMethod->allNext->insert(m); + m->allPrev->insert(startMethod); + m->allNext->insert(finishMethod); + finishMethod->allPrev->insert(m); + } + // Push these two special nodes to the beginning & end of methodList + methodList->push_front(startMethod); + methodList->push_back(finishMethod); + + // Now build the prev, next and concurrent sets + for (MethodList::iterator iter = methodList->begin(); iter != methodList->end(); + iter++) { + Method m = *iter; + // prev -- nodes in allPrev that are before none in allPrev + // next -- nodes in allNext that are after none in allNext (but we + // actually build this set together with building prev + SnapSet::iterator setIt; + for (setIt = m->allPrev->begin(); setIt != m->allPrev->end(); setIt++) { + Method prevMethod = *setIt; + if (MethodCall::disjoint(m->allPrev, prevMethod->allNext)) { + m->prev->insert(prevMethod); + prevMethod->next->insert(m); + } + } + + // concurrent -- all other nodes besides MYSELF, allPrev and allNext + for (MethodList::iterator concurIter = methodList->begin(); concurIter != + methodList->end(); concurIter++) { + Method concur = *concurIter; + if (concur != m && !MethodCall::belong(m->allPrev, concur) + && !MethodCall::belong(m->allNext, concur)) + m->concurrent->insert(concur); + } + } + + if (!cyclic) + AssertEdges(); + // Initialize the justified method of each method + if (!cyclic) + initializeJustifiedNode(); +} + +/** + This method call is used to check whether the edge sets of the nodes are + built correctly --- consistently. We should only use this routine after the + builiding of edges when debugging +*/ +void ExecutionGraph::AssertEdges() { + // Assume there is no self-cycle in execution (ordering points are fine) + ASSERT (!cyclic); + + MethodList::iterator it; + for (it = methodList->begin(); it != methodList->end(); it++) { + Method m = *it; + SnapSet::iterator setIt, setIt1; + int val = 0; + + // Soundness of sets + // 1. allPrev is sound + for (setIt = m->allPrev->begin(); setIt != m->allPrev->end(); setIt++) { + Method prevMethod = *setIt; + val = conflict(prevMethod, m); + ASSERT (val == 1); + } + // 2. allNext is sound + for (setIt = m->allNext->begin(); setIt != m->allNext->end(); setIt++) { + Method nextMethod = *setIt; + val = conflict(m, nextMethod); + ASSERT (val == 1); + } + // 3. concurrent is sound + for (setIt = m->concurrent->begin(); setIt != m->concurrent->end(); setIt++) { + Method concur = *setIt; + val = conflict(m, concur); + ASSERT (val == 0); + } + // 4. allPrev & allNext are complete + ASSERT (1 + m->allPrev->size() + m->allNext->size() + m->concurrent->size() + == methodList->size()); + // 5. prev is sound + for (setIt = m->prev->begin(); setIt != m->prev->end(); setIt++) { + Method prev = *setIt; + ASSERT (MethodCall::belong(m->allPrev, prev)); + for (setIt1 = m->allPrev->begin(); setIt1 != m->allPrev->end(); + setIt1++) { + Method middle = *setIt1; + if (middle == prev) + continue; + val = conflict(prev, middle); + // prev is before none + ASSERT (val != 1); + } + } + // 6. prev is complete + for (setIt = m->allPrev->begin(); setIt != m->allPrev->end(); setIt++) { + Method prev = *setIt; + if (MethodCall::belong(m->prev, prev)) + continue; + // Ensure none of other previous nodes should be in the prev set + bool hasMiddle = false; + for (setIt1 = m->allPrev->begin(); setIt1 != m->allPrev->end(); + setIt1++) { + Method middle = *setIt1; + if (middle == prev) + continue; + val = conflict(prev, middle); + if (val == 1) + hasMiddle = true; + } + ASSERT (hasMiddle); + } + + // 7. next is sound + for (setIt = m->next->begin(); setIt != m->next->end(); setIt++) { + Method next = *setIt; + ASSERT (MethodCall::belong(m->allNext, next)); + for (setIt1 = m->allNext->begin(); setIt1 != m->allNext->end(); + setIt1++) { + Method middle = *setIt1; + if (middle == next) + continue; + val = conflict(middle, next); + // next is after none + ASSERT (val != 1); + } + } + // 8. next is complete + for (setIt = m->allNext->begin(); setIt != m->allNext->end(); setIt++) { + Method next = *setIt; + if (MethodCall::belong(m->next, next)) + continue; + // Ensure none of other next nodes should be in the next set + bool hasMiddle = false; + for (setIt1 = m->allNext->begin(); setIt1 != m->allNext->end(); + setIt1++) { + Method middle = *setIt1; + if (middle == next) + continue; + val = conflict(middle, next); + if (val == 1) + hasMiddle = true; + } + ASSERT (hasMiddle); + } + } +} + +/** + The conflicting relation between two model actions by hb/SC. If act1 and + act2 commutes, it returns 0; Otherwise, if act1->act2, it returns 1; and if + act2->act1, it returns -1 +*/ +int ExecutionGraph::conflict(ModelAction *act1, ModelAction *act2) { + if (act1->happens_before(act2)) + return 1; + else if (act2->happens_before(act1)) + return -1; + + if (act1->is_seqcst() && act2->is_seqcst()) { + if (act1->get_seq_number() < act2->get_seq_number()) + return 1; + else + return -1; + } else + return 0; +} + +/** + If there is no conflict between the ordering points of m1 and m2, then it + returns 0; Otherwise, if m1->m2, it returns 1; and if m2->m1, it returns -1. + If some ordering points have inconsistent conflicting relation, we print out + an error message (Self-cycle) and set the broken flag and return +*/ +int ExecutionGraph::conflict(Method m1, Method m2) { + ASSERT (m1 != m2); + + if (isStartMethod(m1)) + return 1; + if (isFinishMethod(m2)) + return 1; + + action_list_t *OPs1= m1->orderingPoints; + action_list_t *OPs2= m2->orderingPoints; + // Method calls without ordering points are concurrent with any others + if (OPs1->empty() || OPs2->empty()) + return 0; + int val = 0; + action_list_t::iterator iter1, iter2; + for (iter1 = OPs1->begin(); iter1 != OPs1->end(); iter1++) { + ModelAction *act1 = *iter1; + for (iter2 = OPs2->begin(); iter2 != OPs2->end(); iter2++) { + ModelAction *act2 = *iter2; + int res = conflict(act1, act2); + if (res == 0) // Commuting actions + continue; + if (val == 0) + val = res; + else if (val != res) { // Self cycle + cyclic = true; + if (!allowCyclic) { + model_print("There is a self cycle between the following two " + "methods\n"); + m1->print(); + m2->print(); + broken = true; + } + return SELF_CYCLE; + } + } + } + return val; +} + +/** + Whether m2 is before m2 in the execution graph +*/ +bool ExecutionGraph::isReachable(Method m1, Method m2) { + return MethodCall::belong(m1->allNext, m2); +} + +MethodVector* ExecutionGraph::getRootNodes() { + MethodVector *vec = new MethodVector; + for (MethodList::iterator it = methodList->begin(); it != methodList->end(); + it++) { + Method m = *it; + if (!m->exist) + continue; + MethodSet prevMethods = m->allPrev; + if (prevMethods->size() == 0) { // Fast check (naturally a root node) + vec->push_back(m); + continue; + } + + // Also a root when all previous nodes no longer exist + bool isRoot = true; + for (SnapSet::iterator setIt = prevMethods->begin(); setIt != + prevMethods->end(); setIt++) { + Method prev = *setIt; + if (prev->exist) { // It does have an incoming edge + isRoot = false; + break; + } + } + // It does not have an incoming edge now + if (isRoot) + vec->push_back(m); + } + return vec; +} + +/** + Collects the set of method call nodes that do NOT have any following nodes + (the tail of the graph) +*/ +MethodVector* ExecutionGraph::getEndNodes() { + MethodVector *vec = new MethodVector; + for (MethodList::iterator it = methodList->begin(); it != methodList->end(); + it++) { + Method m = *it; + if (m->next->size() == 0) + vec->push_back(m); + } + return vec; +} + +/** + This is a helper function for generating all the topological sortings of the + execution graph. The idea of this function is recursively do the following + process: logically mark whether a method call node is alive or not + (initially all are alive), find a list of nodes that are root nodes (that + have no incoming edges), continuously pick one node in that list, add it to the curList + (which stores one topological sorting), and then recursively call itself to + resolve the rest. + + Arguments: + curList -> It represents a temporal result of a specific topological + sorting; keep in mind that before calling this function, pass an empty + list. + numLiveNodes -> The number of nodes that are logically alive (that have not + been selected and added in a specific topological sorting yet). We keep + such a number as an optimization since when numLinveNodes equals to 0, + we can backtrack. Initially it is the size of the method call list. + historyIndex -> The current history index. We should start with 1. + stopOnFailure -> Stop the checking once we see a failed history + verbose -> Whether the verbose mode is on +*/ +bool ExecutionGraph::checkAllHistoriesHelper(MethodList *curList, int + &numLiveNodes, int &historyIndex, bool stopOnFailure, bool verbose) { + if (cyclic) + return false; + + bool satisfied = true; + if (numLiveNodes == 0) { // Found one sorting, and we can backtrack + // Don't forget to increase the history number + satisfied = checkStateSpec(curList, verbose, historyIndex++); + // Don't forget to recycle + delete curList; + return satisfied; + } + + MethodVector *roots = getRootNodes(); + // Cycle exists (no root nodes but still have live nodes + if (roots->size() == 0) { + model_print("There is a cycle in this graph so we cannot generate" + " sequential histories\n"); + cyclic = true; + return false; + } + + for (unsigned i = 0; i < roots->size(); i++) { + Method m = (*roots)[i]; + m->exist = false; + numLiveNodes--; + // Copy the whole current list and use that copy for the next recursive + // call (because we will need the same copy for other iterations at the + // same level of recursive calls) + MethodList *newList = new MethodList(*curList); + newList->push_back(m); + + bool oneSatisfied = checkAllHistoriesHelper(newList, numLiveNodes, + historyIndex, stopOnFailure, verbose); + // Stop the checking once failure or cycle detected + if (!oneSatisfied && (cyclic || stopOnFailure)) { + delete curList; + delete roots; + return false; + } + satisfied &= oneSatisfied; + // Recover + m->exist = true; + numLiveNodes++; + } + delete curList; + delete roots; + return satisfied; +} + +/** To check one generated history */ +bool ExecutionGraph::checkHistory(MethodList *history, int historyIndex, bool + verbose) { + bool pass = checkStateSpec(history, verbose, historyIndex); + if (!pass) { + // Print out the graph + model_print("Problmatic execution graph: \n"); + print(); + } else if (verbose) { + // Print out the graph in verbose + model_print("Execution graph: \n"); + print(); + } + return pass; +} + +/** Generate one random topological sorting */ +MethodList* ExecutionGraph::generateOneRandomHistory() { + MethodList *res = new MethodList; + int liveNodeNum = methodList->size(); + generateOneRandomHistoryHelper(res, liveNodeNum); + if (cyclic) { + delete res; + return NULL; + } + // Reset the liveness of each method + for (MethodList::iterator it = methodList->begin(); it != methodList->end(); + it++) { + Method m = *it; + m->exist = true; + } + return res; +} + +/** + The helper function to generate one random topological sorting +*/ +void ExecutionGraph::generateOneRandomHistoryHelper(MethodList + *curList, int &numLiveNodes) { + if (cyclic) + return; + + if (numLiveNodes == 0) { // Found one sorting, and we can return + // Don't forget to recycle + return; + } + + MethodVector *roots = getRootNodes(); + // Cycle exists (no root nodes but still have live nodes + if (roots->size() == 0) { + model_print("There is a cycle in this graph so we cannot generate" + " sequential histories\n"); + cyclic = true; + return; + } + + srand (time(NULL)); + int pick = rand() % roots->size(); + Method m = (*roots)[pick]; + + m->exist = false; + numLiveNodes--; + curList->push_back(m); + + delete roots; + generateOneRandomHistoryHelper(curList, numLiveNodes); +} + +Method ExecutionGraph::getStartMethod() { + return methodList->front(); +} + +Method ExecutionGraph::getFinishMethod() { + return methodList->back(); +} + +/** + Print out the ordering points and dynamic calling info (return value & + arguments) of all the methods in the methodList +*/ +void ExecutionGraph::printAllMethodInfo(bool verbose) { + model_print("------------------ Method Info (exec #%d)" + " ------------------\n", execution->get_execution_number()); + for (MethodList::iterator iter = methodList->begin(); iter != + methodList->end(); iter++) { + Method m = *iter; + printMethodInfo(m, verbose); + } + model_print("------------------ End Info (exec #%d)" + " ------------------\n\n", execution->get_execution_number()); +} + +/** + Print out the ordering points and dynamic calling info (return value & + arguments). +*/ +void ExecutionGraph::printMethodInfo(Method m, bool verbose) { + StateFunctions *funcs = NULL; + m->print(verbose, true); + + if (isFakeMethod(m)) + return; + + funcs = funcMap->get(m->name); + ASSERT (funcs); + UpdateState_t printValue = (UpdateState_t) funcs->print->function; + + model_print("\t********** Value Info **********\n"); + if (printValue) { + (*printValue)(m); + } else { + model_print("\tNothing printed..\n"); + } +} + + +/** Clear the states of the method call */ +void ExecutionGraph::clearStates() { + UpdateState_t clearFunc = (UpdateState_t) clear->function; + for (MethodList::iterator it = methodList->begin(); it != methodList->end(); + it++) { + Method m = *it; + if (m->state) { + (*clearFunc)(m); + } + } +} + + +/** + Checking the state specification (in sequential order) +*/ +bool ExecutionGraph::checkStateSpec(MethodList *history, bool verbose, int + historyIndex) { + if (verbose) { + if (historyIndex > 0) + model_print("---- Start to check history #%d ----\n", historyIndex); + else + model_print("---- Start to check history ----\n"); + } + + // @Transition can also return a boolean. For example when a steal() and + // take() in the deque both gets the last element, then we can see a bug in + // the evaluating the list of @Transitions for a following operation. + bool satisfied = true; + + // @Initial state (with a fake starting node) + Method startMethod = getStartMethod(); + UpdateState_t initialFunc = (UpdateState_t) initial->function; + UpdateState_t printStateFunc = (UpdateState_t) printState->function; + UpdateState_t clearFunc = (UpdateState_t) clear->function; + + // We execute the equivalent sequential data structure with the state of the + // startMethod node + (*initialFunc)(startMethod); + if (verbose) { + startMethod->print(false, true); + model_print("\t@Initial on START\n"); + if (printStateFunc) { // If user has defined the print-out function + model_print("\t********** State Info **********\n"); + (*printStateFunc)(startMethod); + } + } + + StateFunctions *funcs = NULL; + /** Execute each method call in the history */ + for (MethodList::iterator it = history->begin(); it != history->end(); + it++) { + Method m = *it; + if (isFakeMethod(m)) + continue; + + StateTransition_t transition = NULL; + + if (verbose) { + m->print(false, true); + funcs = funcMap->get(m->name); + ASSERT (funcs); + UpdateState_t printValue = (UpdateState_t) funcs->print->function; + if (printValue) { + model_print("\t********** Value Info **********\n"); + (*printValue)(m); + } + } + + funcs = funcMap->get(m->name); + ASSERT (funcs); + + CheckState_t preCondition = (CheckState_t) + funcs->preCondition->function; + // @PreCondition of Mehtod m + if (preCondition) { + satisfied = (*preCondition)(startMethod, m); + + if (!satisfied) { + model_print("PreCondition is not satisfied. Problematic method" + " is as follow: \n"); + m->print(true, true); + printOneHistory(history, "Failed History"); + if (verbose) { + if (historyIndex > 0) + model_print("---- Check history #%d END ----\n\n", + historyIndex); + else + model_print("---- Check history END ----\n\n"); + } + break; + } + } + + // After checking the PreCondition, we run the transition on the + // startMethod node to update its state + transition = (StateTransition_t) funcs->transition->function; + // @Transition on the state of startMethod + satisfied = (*transition)(startMethod, m); + if (!satisfied) { // Error in evaluating @Transition + model_print("Transition returns false. Problematic method" + " is as follow: \n"); + m->print(true, true); + printOneHistory(history, "Failed History"); + if (verbose) { + if (historyIndex > 0) + model_print("---- Check history #%d END ----\n\n", + historyIndex); + else + model_print("---- Check history END ----\n\n"); + } + break; + } + + if (verbose) { + model_print("\t@Transition on itself\n"); + if (printStateFunc) { + model_print("\t********** State Info **********\n"); + (*printStateFunc)(startMethod); + } + } + + // @PostCondition of Mehtod m + CheckState_t postCondition = (CheckState_t) + funcs->postCondition->function; + if (postCondition) { + satisfied = (*postCondition)(startMethod, m); + + if (!satisfied) { + model_print("PostCondition is not satisfied. Problematic method" + " is as follow: \n"); + m->print(true, true); + printOneHistory(history, "Failed History"); + if (verbose) { + if (historyIndex > 0) + model_print("---- Check history #%d END ----\n\n", + historyIndex); + else + model_print("---- Check history END ----\n\n"); + } + break; + } + } + } + + // Clear out the states created when checking + (*clearFunc)(startMethod); + + if (satisfied && verbose) { + printOneHistory(history, "Passed History"); + // Print the history in verbose mode + if (historyIndex > 0) + model_print("---- Check history #%d END ----\n\n", historyIndex); + else + model_print("---- Check history END ----\n\n"); + } + + if (verbose) { + if (historyIndex > 0) + model_print("---- Start to check justifying subhistory #%d ----\n", historyIndex); + else + model_print("---- Start to check justifying subhistory ----\n"); + + } + for (MethodList::iterator it = history->begin(); it != history->end(); + it++) { + Method m = *it; + if (isFakeMethod(m)) + continue; + // Check justifying subhistory + if (!m->justified) { + funcs = funcMap->get(m->name); + CheckState_t justifyingPrecondition = (CheckState_t) + funcs->justifyingPrecondition->function; + CheckState_t justifyingPostcondition = (CheckState_t) + funcs->justifyingPostcondition->function; + if (!justifyingPrecondition && !justifyingPostcondition ) { + // No need to check justifying conditions + m->justified = true; + if (verbose) { + model_print("\tMethod call "); + m->print(false, false); + model_print(": automatically justified.\n"); + } + } else { + bool justified = checkJustifyingSubhistory(history, m, verbose, historyIndex); + if (justified) { + // Set the "justified" flag --- no need to check again for cur + m->justified = true; + if (verbose) { + model_print("\tMethod call "); + m->print(false, false); + model_print(": is justified\n"); + } + } else { + if (verbose) { + model_print("\tMethod call "); + m->print(false, false); + model_print(": has NOT been justified yet\n"); + } + } + } + } else { + if (verbose) { + model_print("\tMethod call "); + m->print(false, false); + model_print(": is justified\n"); + } + } + } + if (verbose) { + if (historyIndex > 0) + model_print("---- Start to check justifying subhistory #%d END ----\n\n", historyIndex); + else + model_print("---- Start to check justifying subhistory # END ----\n\n"); + + } + + return satisfied; +} + +bool ExecutionGraph::checkJustifyingSubhistory(MethodList *history, Method + cur, bool verbose, int historyIndex) { + if (verbose) { + model_print("\tMethod call "); + cur->print(false, false); + model_print(": is being justified\n"); + } + + // @Transition can also return a boolean. For example when a steal() and + // take() in the deque both gets the last element, then we can see a bug in + // the evaluating the list of @Transitions for a following operation. + bool satisfied = true; + + // @Initial state (with a fake starting node) + Method startMethod = getStartMethod(); + UpdateState_t initialFunc = (UpdateState_t) initial->function; + UpdateState_t printStateFunc = (UpdateState_t) printState->function; + UpdateState_t printVauleFunc = NULL; + UpdateState_t clearFunc = (UpdateState_t) clear->function; + + // We execute the equivalent sequential data structure with the state of the + // current method call + (*initialFunc)(cur); + if (verbose) { + startMethod->print(false, true); + model_print("\t@Initial on "); + cur->print(false, true); + if (printStateFunc) { // If user has defined the print-out function + model_print("\t********** State Info **********\n"); + (*printStateFunc)(cur); + } + } + + StateFunctions *funcs = NULL; + StateTransition_t transition = NULL; + /** Execute each method call in the justifying subhistory till cur */ + for (MethodList::iterator it = history->begin(); it != history->end(); it++) { + Method m = *it; + if (m == cur) + break; + if (isFakeMethod(m)) + continue; + + // Ignore method calls that are not in my justifying subhistory + if (!MethodCall::belong(cur->allPrev, m)) + continue; + + + if (verbose) { + m->print(false, true); + funcs = funcMap->get(m->name); + ASSERT (funcs); + UpdateState_t printValue = (UpdateState_t) funcs->print->function; + if (printValue) { + model_print("\t********** Value Info **********\n"); + (*printValue)(m); + } + } + + funcs = funcMap->get(m->name); + ASSERT (funcs); + transition = (StateTransition_t) + funcs->transition->function; + + // In checking justifying behaviors, we don't check precondition & + // postcondition for other method calls + + // @Transition on the state of the "cur" method call + satisfied = (*transition)(cur, m); + if (!satisfied) { // Error in evaluating @Transition + if (verbose) { + model_print("\tFailed @Transition before\n"); + } + // Clear out the states created when checking + (*clearFunc)(startMethod); + return false; + } else { + if (verbose) { + model_print("\t@Transition on itself\n"); + if (printStateFunc) { + model_print("\t********** State Info **********\n"); + (*printStateFunc)(startMethod); + } + } + } + } + + // For justifying subhistory, we only check the @JustifyingPrecondition & + // @JustifyingPostcondition for the last method call (the one we are + // checking) + + // First check the @JustifyingPrecondition + funcs = funcMap->get(cur->name); + if (satisfied) { + // Check the justifying preondition on cur + CheckState_t justifyingPrecondition = (CheckState_t) + funcs->justifyingPrecondition->function; + if (justifyingPrecondition) { + // @JustifyingPrecondition of Mehtod cur + satisfied = (*justifyingPrecondition)(cur, cur); + } + if (!satisfied) { + if (verbose) { + model_print("\tFailed @JustifyingPrecondition\n"); + } + // Clear out the states created when checking + (*clearFunc)(startMethod); + return false; + } + } + + // Then execute the @Transition + transition = (CheckState_t) funcs->transition->function; + // @Transition on the state of the "cur" method call + satisfied = (*transition)(cur, cur); + if (!satisfied) { // Error in evaluating @Transition + if (verbose) { + model_print("\tFailed @Transition on itself\n"); + } + // Clear out the states created when checking + (*clearFunc)(startMethod); + return false; + } + if (verbose) { + model_print("\t@Transition on itself\n"); + if (printStateFunc) { + model_print("\t********** State Info **********\n"); + (*printStateFunc)(startMethod); + } + } + + // Finally check the @JustifyingPostcondition + if (satisfied) { + // Check the justifying preondition on cur + funcs = funcMap->get(cur->name); + CheckState_t justifyingPostcondition = (CheckState_t) + funcs->justifyingPostcondition->function; + if (justifyingPostcondition) { + // @JustifyingPostcondition of Mehtod cur + satisfied = (*justifyingPostcondition)(cur, cur); + } + } + + // Clear out the states created when checking + (*clearFunc)(startMethod); + return satisfied; +} + + +/** + To take a list of actions and print it out in a nicer way +*/ +void ExecutionGraph::printActions(action_list_t *actions, const char *header) { + model_print("%s\n", header); + model_print("---------- Thread List (Begin) ---------\n"); + for (action_list_t::iterator it = actions->begin(); it != actions->end(); + it++) { + ModelAction *act = *it; + SpecAnnotation *anno = getAnnotation(act); + if (anno) { + model_print("%s -> ", specAnnoType2Str(anno->type)); + } + act->print(); + } + model_print("---------- Thread List (End) ---------\n"); +} + +void ExecutionGraph::printOneSubhistory(MethodList *history, Method cur, CSTR header) { + model_print("------------- %s (exec #%d) -------------\n", header, + execution->get_execution_number()); + int idx = 1; + for (MethodList::iterator it = history->begin(); it != history->end(); it++) { + Method m = *it; + if (!MethodCall::belong(cur->allPrev, m)) + continue; + model_print("%d. ", idx++); + m->print(false); + } + model_print("------------- %s (exec #%d) (end) -------------\n", + header, execution->get_execution_number()); +} + diff --git a/spec-analysis/executiongraph.h b/spec-analysis/executiongraph.h new file mode 100644 index 0000000..870fd60 --- /dev/null +++ b/spec-analysis/executiongraph.h @@ -0,0 +1,338 @@ +#ifndef _EXECUTIONGRAPH_H +#define _EXECUTIONGRAPH_H + +#include + +#include "hashtable.h" +#include "specannotation.h" +#include "mymemory.h" +#include "modeltypes.h" +#include "action.h" +#include "common.h" +#include "execution.h" + +#include "methodcall.h" +#include "specannotation.h" + + +const int SELF_CYCLE = 0xfffe; + +/** + Record the a potential commit point information, including the potential + commit point label number and the corresponding operation +*/ +typedef struct PotentialOP { + ModelAction *operation; + CSTR label; + + PotentialOP(ModelAction *op, CSTR name); + + SNAPSHOTALLOC +} PotentialOP; + +class Graph; + + +typedef SnapList PotentialOPList; + +/** + This represents the execution graph at the method call level. Each node is a + MethodCall type that has the runtime info (return value & arguments) and the + state info the method call. The edges in this graph are the hb/SC edges + dereived from the ordering points of the method call. Those edges + information are stoed in the PREV and NEXT set of MethodCall struct. +*/ +class ExecutionGraph { + public: + ExecutionGraph(ModelExecution *e, bool allowCyclic); + + /********** Public class interface for the core checking engine **********/ + /** + Build the graph for an execution. It should returns true when the graph + is correctly built + */ + void buildGraph(action_list_t *actions); + + /** Check whether this is a broken execution */ + bool isBroken(); + + /** Check whether this is an execution that has method calls without + * ordering points */ + bool isNoOrderingPoint(); + + /** + Check whether this is a cyclic execution graph, meaning that the graph + has an cycle derived from the ordering points' hb/SC relation + */ + bool hasCycle(); + + /** Reset the internal graph "broken" state to okay again */ + void resetBroken(); + + /** Check whether the execution is admmisible */ + bool checkAdmissibility(); + + /** Checking cyclic graph specification */ + bool checkCyclicGraphSpec(bool verbose); + + /** Check whether a number of random history is correct */ + bool checkRandomHistories(int num = 1, bool stopOnFail = true, bool verbose = false); + + /** Check whether all histories are correct */ + bool checkAllHistories(bool stopOnFailure = true, bool verbose = false); + + /********** A few public printing functions for DEBUGGING **********/ + + /** + Print out the ordering points and dynamic calling info (return value & + arguments) of all the methods in the methodList + */ + void printAllMethodInfo(bool verbose); + + /** Print a random sorting */ + void printOneHistory(MethodList *list, CSTR header = "A random history"); + + /** Print all the possible sortings */ + void printAllHistories(MethodListVector *sortings); + + /** Print out the graph for the purpose of debugging */ + void print(bool allEdges = false); + + /** + Print out the graph in reverse order (with previous edges) for the + purpose of debugging + */ + void PrintReverse(bool allEdges); + + SNAPSHOTALLOC + + private: + /** The corresponding execution */ + ModelExecution *execution; + + /** All the threads each in a separate list of actions */ + SnapVector *threadLists; + + /** A plain list of all method calls (Method) in this execution */ + MethodList *methodList; + + /** + A list that represents some random history. The reason we have this here + is that before checking anything, we have to check graph acyclicity, and + that requires us to check whether we can generate a topological sorting. + Therefore, when we check it, we store that random result here. + */ + MethodList *randomHistory; + + /** Whether this is a broken graph */ + bool broken; + + /** Whether this graph has method calls that have no ordering points */ + bool noOrderingPoint; + + /** Whether there is a cycle in the graph */ + bool cyclic; + + /** Whether users expect us to check cyclic graph */ + bool allowCyclic; + + + /** The state initialization function */ + NamedFunction *initial; + + /** FIXME: The final check function; we might delete this */ + NamedFunction *final; + + /** The state copy function */ + NamedFunction *copy; + + /** The state clear function */ + NamedFunction *clear; + + /** The state print-out function */ + NamedFunction *printState; + + /** The map from interface label name to the set of spec functions */ + StateFuncMap *funcMap; + + /** The commutativity rule array and its size */ + CommutativityRule *commuteRules; + int commuteRuleNum; + + /********** Internal member functions **********/ + + /** + Simply build a vector of lists of thread actions. Such info will be very + useful for later constructing the execution graph + */ + void buildThreadLists(action_list_t *actions); + + /** Build the nodes from a thread list */ + void buildNodesFromThread(action_list_t *actions); + + /** Build the nodes from all the thread lists */ + void buildNodesFromThreads(); + + + /** + Find the previous non-annotation model action (ordering point from the + current iterator + */ + ModelAction* findPrevAction(action_list_t *actions, action_list_t::iterator + iter); + + /** + Extract a MethodCall node starting from the current iterator, and the + iter iterator will be advanced to the next INTERFACE_BEGIN annotation. + When called, the iter must point to an INTERFACE_BEGIN annotation + */ + Method extractMethod(action_list_t *actions, action_list_t::iterator &iter); + + /** + Process the initialization annotation block to initialize the + commutativity rule info and the checking function info + */ + void processInitAnnotation(AnnoInit *annoInit); + + /** + A utility function to extract the actual annotation + pointer and return the actual annotation if this is an annotation action; + otherwise return NULL. + */ + SpecAnnotation* getAnnotation(ModelAction *act); + + /** + After building up the graph (both the nodes and egdes are correctly + built), we also call this function to initialize the most recent + justified node of each method node. + + A justified method node of a method m is a method that is in the allPrev + set of m, and all other nodes in the allPrev set of m are either before + or after it. The most recent justified node is the most recent one in + the hb/SC order. + */ + void initializeJustifiedNode(); + + /** + After extracting the MethodCall info for each method call, we use this + function to build the edges (a few different sets of edges that + represent the edge of the execution graph (PREV, NEXT & CONCURRENT...) + */ + void buildEdges(); + + /** + This method call is used to check whether the edge sets of the nodes are + built correctly --- consistently. We should only use this routine after the + builiding of edges when debugging + */ + void AssertEdges(); + + /** + The conflicting relation between two model actions by hb/SC. If act1 and + act2 commutes, it returns 0; Otherwise, if act1->act2, it returns 1; and + if act2->act1, it returns -1 + */ + int conflict(ModelAction *act1, ModelAction *act2); + + /** + If there is no conflict between the ordering points of m1 and m2, then + it returns 0; Otherwise, if m1->m2, it returns 1; and if m2->m1, it + returns -1. If some ordering points have inconsistent conflicting + relation, we print out an error message (Self-cycle) and set the broken + flag and return + */ + int conflict(Method m1, Method m2); + + /** + Check whether m1 is before m2 in hb/SC; Reachability <=> m1 -hb/SC-> m2. + We need to call this method when checking admissibility properties + */ + bool isReachable(Method m1, Method m2); + + /** + Find the list of nodes that do not have any incoming edges (root nodes). + Be careful that when generating histories, this function will also + consider whether a method node logicall exists. + */ + MethodVector* getRootNodes(); + + /** + Find the list of nodes that do not have any outgoing edges (end nodes) + */ + MethodVector* getEndNodes(); + + /** + A helper function for generating and check all sequential histories. Before calling this function, initialize an empty + MethodList , and pass it as curList. Also pass the size of the method + list as the numLiveNodes. + + If you only want to stop the checking process when finding one failed + history, pass true to stopOnFailure. + */ + bool checkAllHistoriesHelper(MethodList *curList, int &numLiveNodes, int + &historyNum, bool stopOnFailure, bool verbose); + + + /** Check whether a specific history is correct */ + bool checkHistory(MethodList *history, int historyIndex, bool verbose = false); + + /** Generate one random topological sorting */ + MethodList* generateOneRandomHistory(); + + /** + The helper function to generate one random topological sorting + */ + void generateOneRandomHistoryHelper(MethodList + *curList, int &numLiveNodes); + + /** Return the fake nodes -- START & END */ + Method getStartMethod(); + Method getFinishMethod(); + + /** Whether method call node m is a fake node */ + inline bool isFakeMethod(Method m) { + return isStartMethod(m) || isFinishMethod(m); + } + + /** Whether method call node m is a starting node */ + inline bool isStartMethod(Method m) { + return m->name == GRAPH_START; + } + + /** Whether method call node m is a finish node */ + inline bool isFinishMethod(Method m) { + return m->name == GRAPH_FINISH; + } + + /** + Print out the ordering points and dynamic calling info (return value & + arguments). + */ + void printMethodInfo(Method m, bool verbose); + + /** Clear the states of the method call */ + void clearStates(); + + /** + Check the state specifications (PreCondition & PostCondition & state + transition and evaluation) based on the graph (called after + admissibility check). The verbose option controls whether we print a + detailed list of checking functions that we have called + */ + bool checkStateSpec(MethodList *history, bool verbose, int historyNum); + + /** + Check the justifying subhistory with respect to history of m. + */ + bool checkJustifyingSubhistory(MethodList *subhistory, Method cur, + bool verbose, int historyIndex); + + /** Print a problematic thread list */ + void printActions(action_list_t *actions, const char *header = "The problematic thread list:"); + + /** Print one jusifying subhistory of method call cur */ + void printOneSubhistory(MethodList *history, Method cur, + CSTR header); +}; + +#endif diff --git a/spec-analysis/include/specannotation-api.h b/spec-analysis/include/specannotation-api.h new file mode 100644 index 0000000..aee4196 --- /dev/null +++ b/spec-analysis/include/specannotation-api.h @@ -0,0 +1,38 @@ +#ifndef _SPECANNOTATION_API_H +#define _SPECANNOTATION_API_H + +#define NEW_SIZE(type, size) (type*) malloc(size) +#define NEW(type) NEW_SIZE(type, sizeof(type)) + +struct MethodCall; +typedef struct MethodCall *Method; +typedef const char *CSTR; + +struct AnnoInterfaceInfo; +typedef struct AnnoInterfaceInfo AnnoInterfaceInfo; + +#ifdef __cplusplus +extern "C" { +#endif + +struct AnnoInterfaceInfo* _createInterfaceBeginAnnotation(CSTR name); + +void _setInterfaceBeginAnnotationValue(struct AnnoInterfaceInfo *info, void *value); + +void _createInterfaceEndAnnotation(CSTR name); + +void _createOPDefineAnnotation(); + +void _createPotentialOPAnnotation(CSTR label); + +void _createOPCheckAnnotation(CSTR label); + +void _createOPClearAnnotation(); + +void _createOPClearDefineAnnotation(); + +#ifdef __cplusplus +}; +#endif + +#endif diff --git a/spec-analysis/methodcall.cc b/spec-analysis/methodcall.cc new file mode 100644 index 0000000..84c35ba --- /dev/null +++ b/spec-analysis/methodcall.cc @@ -0,0 +1,125 @@ +#include +#include "common.h" +#include "threads-model.h" +#include "methodcall.h" +#include "spec_common.h" + +CSTR GRAPH_START = "START_NODE"; +CSTR GRAPH_FINISH = "FINISH_NODE"; + +const unsigned int METHOD_ID_MAX = 0xffffffff; +const unsigned int METHOD_ID_MIN = 0; + +MethodCall::MethodCall(CSTR name, void *value, ModelAction *begin) : + name(name), value(value), prev(new SnapSet), next(new + SnapSet), concurrent(new SnapSet), justifiedMethod(NULL), + justified(false), end(NULL), orderingPoints(new action_list_t), allPrev(new + SnapSet), allNext(new SnapSet), exist(true) { + if (name == GRAPH_START) { + this->begin = NULL; + id = METHOD_ID_MIN; + tid = 1; // Considered to be the main thread + } else if (name == GRAPH_FINISH) { + this->begin = NULL; + id = METHOD_ID_MAX; + tid = 1; // Considered to be the main thread + } else { + this->begin = begin; + ASSERT (begin); + id = begin->get_seq_number(); + tid = id_to_int(begin->get_tid()); + } +} + +void MethodCall::addPrev(Method m) { prev->insert(m); } + +void MethodCall::addNext(Method m) { next->insert(m); } + +void MethodCall::addConcurrent(Method m) { concurrent->insert(m); } + +void MethodCall::addOrderingPoint(ModelAction *act) { + bool hasIt = orderingPoints->end() != std::find(orderingPoints->begin(), + orderingPoints->end(), act); + if (!hasIt) + orderingPoints->push_back(act); +} + + +bool MethodCall::before(Method another) { + return belong(allNext, another); +} + +bool MethodCall::belong(MethodSet s, Method m) { + return s->end() != std::find(s->begin(), s->end(), m); +} + +bool MethodCall::identical(MethodSet s1, MethodSet s2) { + if (s1->size() != s2->size()) + return false; + SnapSet::iterator it; + for (it = s1->begin(); it != s1->end(); it++) { + Method m1 = *it; + if (belong(s2, m1)) + return false; + } + return true; +} + +/** + Put the union of src and dest to dest. +*/ +void MethodCall::Union(MethodSet dest, MethodSet src) { + SnapSet::iterator it; + for (it = src->begin(); it != src->end(); it++) { + Method m = *it; + dest->insert(m); + } +} + +MethodSet MethodCall::intersection(MethodSet s1, MethodSet s2) { + MethodSet res = new SnapSet; + SnapSet::iterator it; + for (it = s1->begin(); it != s1->end(); it++) { + Method m = *it; + if (belong(s2, m)) + res->insert(m); + } + return res; +} + +bool MethodCall::disjoint(MethodSet s1, MethodSet s2) { + SnapSet::iterator it; + for (it = s1->begin(); it != s1->end(); it++) { + Method m = *it; + if (belong(s2, m)) + return false; + } + return true; +} + +void MethodCall::print(bool printOP, bool breakAtEnd) { + if (name == GRAPH_START) { + model_print("%s", GRAPH_START); + if (breakAtEnd) + model_print("\n"); + return; + } + if (name == GRAPH_FINISH) { + model_print("%s", GRAPH_FINISH); + if (breakAtEnd) + model_print("\n"); + return; + } + model_print("%u.%s(T%d)", id, name, id_to_int(begin->get_tid())); + if (breakAtEnd) + model_print("\n"); + if (!printOP) + return; + int i = 1; + for (action_list_t::iterator it = orderingPoints->begin(); it != + orderingPoints->end(); it++) { + ModelAction *op = *it; + model_print("\t-> %d. ", i++); + op->print(); + } +} diff --git a/spec-analysis/methodcall.h b/spec-analysis/methodcall.h new file mode 100644 index 0000000..a88b651 --- /dev/null +++ b/spec-analysis/methodcall.h @@ -0,0 +1,114 @@ +#ifndef _METHODCALL_H +#define _METHODCALL_H + +#include "stl-model.h" +#include "action.h" +#include "spec_common.h" + +class MethodCall; + +typedef MethodCall *Method; +typedef SnapSet *MethodSet; +typedef SnapList action_list_t; + +typedef SnapList MethodList; +typedef SnapVector MethodVector; +typedef SnapVector MethodListVector; + +/** + This is the core class on which the whole checking process will be + executing. With the original execution (with the raw annotation + information), we construct an execution graph whose nodes represent method + calls, and whose edges represent the hb/SC relation between the ordering + points of method calls. In that graph, the MethodCall class acts as the node + that contains the core information for checking --- the name of the + interface, the value (return value and arguments), the state of the current + method call, and a set of previous, next and concurrent method calls. + + Plus, this class contains extra info about the ordering points, a set of all + method calls that are hb/SC before me (for evaluating the state), and also + some other helping internal member variable for generating checking schemes. +*/ +class MethodCall { + public: + unsigned int id; // The method call id (the seq_num of the begin action) + int tid; // The thread id + CSTR name; // The interface label name + void *value; // The pointer that points to the struct that have the return + // value and the arguments + void *state; // The pointer that points to the struct that represents + // the state + MethodSet prev; // Method calls that are hb right before me + MethodSet next; // Method calls that are hb right after me + MethodSet concurrent; // Method calls that are concurrent with me + + Method justifiedMethod; // The method before me and is not concurrent with + // any other mehtods in my allPrev set + + /** + This indicates if the non-deterministic behaviors of this method call + has been justified by any of its justifying subhistory. If so, we do not + need to check on its justifying subhistory. Initially it is false. + */ + bool justified; + + MethodCall(CSTR name, void *value = NULL, ModelAction *begin = NULL); + + void addPrev(Method m); + + void addNext(Method m); + + void addConcurrent(Method m); + + void addOrderingPoint(ModelAction *act); + + bool before(Method another); + + static bool belong(MethodSet s, Method m); + + static bool identical(MethodSet s1, MethodSet s2); + + /** Put the union of src and dest to dest */ + static void Union(MethodSet dest, MethodSet src); + + static MethodSet intersection(MethodSet s1, MethodSet s2); + + static bool disjoint(MethodSet s1, MethodSet s2); + + /** + Print the method all name with the seq_num of the begin annotation and + its thread id. + + printOP == true -> Add each line with the ordering point operation's + print() + + breakAtEnd == true -> Add a line break at the end of the print; + otherwise, the print will be a string without line breaker when printOP + is false. + */ + void print(bool printOP = true, bool breakAtEnd = true); + + /** + FIXME: The end action is not really used or necessary here, maybe we + should clean this + */ + ModelAction *begin; + ModelAction *end; + action_list_t *orderingPoints; + + /** + Keep a set of all methods that are hb/SC before&after me to calculate my + state + */ + MethodSet allPrev; + MethodSet allNext; + + /** Logically exist (for generating all possible topological sortings) */ + bool exist; + + SNAPSHOTALLOC +}; + + + +#endif diff --git a/spec-analysis/spec_common.h b/spec-analysis/spec_common.h new file mode 100644 index 0000000..b8c3a46 --- /dev/null +++ b/spec-analysis/spec_common.h @@ -0,0 +1,47 @@ +#ifndef _SPEC_COMMON_H +#define _SPEC_COMMON_H + +#include +#include +#include "mymemory.h" + +/** Comment this out if you don't want unnecessary debugging printing out */ +#define CDSSPEC_DEBUG + +#ifdef CDSSPEC_DEBUG +#define debug_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0) +#else +#define debug_print(fmt, ...) do { } while (0) +#endif + +#define SPEC_ANALYSIS 1 + +/** Null function pointer */ +#define NULL_FUNC NULL + +#define NEW_SIZE(type, size) (type*) malloc(size) +#define NEW(type) NEW_SIZE(type, sizeof(type)) + +#define EQ(str1, str2) (strcmp(str1, str2) == 0) + +extern const unsigned int METHOD_ID_MAX; +extern const unsigned int METHOD_ID_MIN; + +typedef const char *CSTR; + +extern CSTR GRAPH_START; +extern CSTR GRAPH_FINISH; + +/** Define a snapshotting set for CDSChecker backend analysis */ +template +class SnapSet : public std::set<_Tp, std::less<_Tp>, SnapshotAlloc<_Tp> > +{ + public: + typedef std::set<_Tp, std::less<_Tp>, SnapshotAlloc<_Tp> > set; + + SnapSet() : set() { } + + SNAPSHOTALLOC +}; + +#endif diff --git a/spec-analysis/specanalysis.cc b/spec-analysis/specanalysis.cc new file mode 100644 index 0000000..e5a1f2c --- /dev/null +++ b/spec-analysis/specanalysis.cc @@ -0,0 +1,226 @@ +#include "specanalysis.h" +#include "action.h" +#include "cyclegraph.h" +#include "threads-model.h" +#include "clockvector.h" +#include "execution.h" +#include +#include +#include "modeltypes.h" +#include "executiongraph.h" + + +SPECAnalysis::SPECAnalysis() +{ + execution = NULL; + stats = (struct spec_stats*) model_calloc(1, sizeof(struct spec_stats)); + print_always = false; + print_inadmissible = true; + quiet = false; + checkCyclic = false; + stopOnFail = false; + checkRandomNum = 0; +} + +SPECAnalysis::~SPECAnalysis() { +} + +void SPECAnalysis::setExecution(ModelExecution * execution) { + this->execution = execution; +} + +const char * SPECAnalysis::name() { + const char * name = "SPEC"; + return name; +} + +void SPECAnalysis::finish() { + model_print("\n"); + model_print(">>>>>>>> SPECAnalysis finished <<<<<<<<\n"); + + model_print("Total execution checked: %d\n", stats->bugfreeCnt); + model_print("Detected by CDSChecker: %d\n", stats->buggyCnt); + model_print("Broken graph: %d\n", stats->brokenCnt); + model_print("Cyclic graph: %d\n", stats->cyclicCnt); + model_print("Inadmissible executions: %d\n", stats->inadmissibilityCnt); + model_print("Failed executions: %d\n", stats->failedCnt); + + if (stats->cyclicCnt > 0 && checkCyclic) { + model_print("Warning: You have cycle in your execution graphs.\n"); + } + + if (stats->failedCnt == 0) { + model_print("Yay! All executions have passed the specification.\n"); + if (stats->brokenCnt > 0) + model_print("However! You have executions with a broken graph.\n"); + if (stats->cyclicCnt > 0) { + model_print("Warning: You have cyclic execution graphs!\n"); + if (checkCyclic) { + model_print("Make sure that's what you expect.\n"); + } + } + if (stats->inadmissibilityCnt > 0) + model_print("However! You have inadmissible executions.\n"); + if (stats->noOrderingPointCnt > 0 && print_always) + model_print("You have execution graphs that have no ordering points.\n"); + + } +} + +bool SPECAnalysis::isCheckRandomHistories(char *opt, int &num) { + char *p = opt; + bool res = false; + if (*p == 'c') { + p++; + if (*p == 'h') { + p++; + if (*p == 'e') { + p++; + if (*p == 'c') { + p++; + if (*p == 'k') { + res = true; + p++; + } + } + } + } + } + if (res) { + // p now should point to '-' + if (*p == '-') { + p++; + num = atoi(p); + if (num > 0) + return true; + } + return false; + } + return res; +} + +bool SPECAnalysis::option(char * opt) { + if (strcmp(opt, "verbose")==0) { + print_always=true; + return false; + } else if (strcmp(opt, "no-admissible")==0) { + print_inadmissible = false; + return false; + } else if (strcmp(opt, "quiet")==0) { + quiet = true; + return false; + } else if (strcmp(opt, "check-cyclic") == 0) { + checkCyclic = true; + return false; + } else if (strcmp(opt, "stop-on-fail")==0) { + stopOnFail = true; + return false; + } else if (isCheckRandomHistories(opt, checkRandomNum)) { + return false; + } else if (strcmp(opt, "help") != 0) { + model_print("Unrecognized option: %s\n", opt); + } + + model_print("SPEC Analysis options\n" + "By default SPEC outputs the graphs of those failed execution\n" + "verbose -- print graphs of any traces\n" + "quiet -- do not print out graphs\n" + "inadmissible-quiet -- print the inadmissible\n" + "check-one -- only check one random possible topological" + "sortings (check all possible by default)\n" + ); + model_print("\n"); + + return true; +} + +void SPECAnalysis::analyze(action_list_t *actions) { + /* Count the number traces */ + stats->traceCnt++; + if (execution->have_bug_reports()) { + /* Count the number traces */ + stats->buggyCnt++; + return; + } + + /* Count the number bug-free traces */ + stats->bugfreeCnt++; + + // FIXME: Make checkCyclic false by default + ExecutionGraph *graph = new ExecutionGraph(execution, checkCyclic); + graph->buildGraph(actions); + if (graph->isBroken()) { + stats->brokenCnt++; + if (print_always && !quiet) { // By default not printing + model_print("Execution #%d has a broken graph.\n\n", + execution->get_execution_number()); + } + return; + } + + if (print_always) { + model_print("------------------ Checking execution #%d" + " ------------------\n", execution->get_execution_number()); + } + + // Count how many executions that have no-ordering-point method calls + if (graph->isNoOrderingPoint()) { + stats->noOrderingPointCnt++; + } + + if (!graph->checkAdmissibility()) { + /* One more inadmissible trace */ + stats->inadmissibilityCnt++; + if (print_inadmissible && !quiet) { + model_print("Execution #%d is NOT admissible\n", + execution->get_execution_number()); + graph->print(); + if (print_always) + graph->printAllMethodInfo(true); + } + return; + } + + bool pass = false; + if (graph->hasCycle()) { + /* One more trace with a cycle */ + stats->cyclicCnt++; + if (!checkCyclic) { + if (!quiet) + graph->print(); + if (print_always && !quiet) { // By default not printing + model_print("Execution #%d has a cyclic graph.\n\n", + execution->get_execution_number()); + } + } else { + if (print_always && !quiet) { + model_print("Checking cyclic execution #%d...\n", + execution->get_execution_number()); + } + pass = graph->checkCyclicGraphSpec(print_always && !quiet); + } + } else if (checkRandomNum > 0) { // Only a few random histories + if (print_always && !quiet) + model_print("Check %d random histories...\n", checkRandomNum); + pass = graph->checkRandomHistories(checkRandomNum, true, print_always && !quiet); + } else { // Check all histories + if (print_always && !quiet) + model_print("Check all histories...\n"); + pass = graph->checkAllHistories(true, print_always && !quiet); + } + + if (!pass) { + /* One more failed trace */ + stats->failedCnt++; + model_print("Execution #%d failed.\n\n", + execution->get_execution_number()); + } else { + /* One more passing trace */ + stats->passCnt++; + + if (print_always && !quiet) { // By default not printing + model_print("Execution #%d passed.\n\n", + execution->get_execution_number()); + } + } +} diff --git a/spec-analysis/specanalysis.h b/spec-analysis/specanalysis.h new file mode 100644 index 0000000..1c77156 --- /dev/null +++ b/spec-analysis/specanalysis.h @@ -0,0 +1,77 @@ +#ifndef _SPECANALYSIS_H +#define _SPECANALYSIS_H + +#include + +#include "traceanalysis.h" +#include "mymemory.h" +#include "modeltypes.h" +#include "action.h" + +struct spec_stats { + /** The number of traces that have passed the checking */ + unsigned passCnt; + + /** The number of inadmissible traces */ + unsigned inadmissibilityCnt; + + /** The number of all checked traces */ + unsigned traceCnt; + + /** The number of traces with a cyclic graph */ + unsigned cyclicCnt; + + /** The number of traces with broken graphs */ + unsigned brokenCnt; + + /** The number of traces with graphs that has no ordering points */ + unsigned noOrderingPointCnt; + + /** The number of traces that failed */ + unsigned failedCnt; + + /** The number of buggy and bug-free traces (by CDSChecker) */ + unsigned buggyCnt; + unsigned bugfreeCnt; +}; + +class SPECAnalysis : public TraceAnalysis { + public: + SPECAnalysis(); + ~SPECAnalysis(); + + virtual void setExecution(ModelExecution * execution); + virtual void analyze(action_list_t *actions); + virtual const char * name(); + virtual bool option(char *); + virtual void finish(); + + /** Some stats */ + spec_stats *stats; + + SNAPSHOTALLOC + private: + /** The execution */ + ModelExecution *execution; + + /** A few useful options */ + /* Print out the graphs of all executions */ + bool print_always; + /* Print out the graphs of the inadmissible traces */ + bool print_inadmissible; + /* Never print out the graphs of any traces */ + bool quiet; + /* Whether we still want to check cyclic executions */ + bool checkCyclic; + /* Stop checking when seeing one failed history */ + bool stopOnFail; + /* The number of random histories to be checked; If 0, we check all possible + * histories */ + int checkRandomNum; + + /** Whether this is a "check-12" like option */ + bool isCheckRandomHistories(char *opt, int &num); +}; + + +#endif diff --git a/spec-analysis/specannotation.cc b/spec-analysis/specannotation.cc new file mode 100644 index 0000000..84a9795 --- /dev/null +++ b/spec-analysis/specannotation.cc @@ -0,0 +1,96 @@ +#include +#include "specannotation.h" +#include "cdsannotate.h" + +/********** Annotations **********/ + +SpecAnnotation::SpecAnnotation(SpecAnnoType type, const void *anno) : type(type), + annotation(anno) { } + + +CommutativityRule::CommutativityRule(CSTR method1, CSTR method2, CSTR rule, + CheckCommutativity_t condition) : method1(method1), + method2(method2), rule(rule), condition(condition) {} + +bool CommutativityRule::isRightRule(Method m1, Method m2) { + return (m1->name == method1 && m2->name == method2) || + (m1->name == method2 && m2->name == method1); +} + +bool CommutativityRule::checkCondition(Method m1, Method m2) { + if (m1->name == method1 && m2->name == method2) + return (*condition)(m1, m2); + else if (m1->name == method2 && m2->name == method1) + return (*condition)(m2, m1); + else // The checking should only be called on the right rule + ASSERT(false); + return false; +} + +NamedFunction::NamedFunction(CSTR name, CheckFunctionType type, void *function) : name(name), + type(type), function(function) { } + +StateFunctions::StateFunctions(NamedFunction *transition, NamedFunction + *preCondition, NamedFunction * justifyingPrecondition, + NamedFunction *justifyingPostcondition, + NamedFunction *postCondition, NamedFunction *print) : transition(transition), + preCondition(preCondition), justifyingPrecondition(justifyingPrecondition), + justifyingPostcondition(justifyingPostcondition), + postCondition(postCondition), print(print) { } + + +AnnoInit::AnnoInit(NamedFunction *initial, NamedFunction *final, NamedFunction + *copy, NamedFunction *clear, NamedFunction *printState, CommutativityRule + *commuteRules, int ruleNum) : initial(initial), final(final), copy(copy), + clear(clear), printState(printState), commuteRules(commuteRules), + commuteRuleNum(ruleNum) +{ + funcMap = new StateFuncMap; +} + + +void AnnoInit::addInterfaceFunctions(CSTR name, StateFunctions *funcs) { + funcMap->put(name, funcs); +} + +AnnoInterfaceInfo::AnnoInterfaceInfo(CSTR name) : name(name), value(NULL) { } + + +/********** Universal functions for rewriting the program **********/ + +AnnoInterfaceInfo* _createInterfaceBeginAnnotation(CSTR name) { + AnnoInterfaceInfo *info = new AnnoInterfaceInfo(name); + // Create and instrument with the INTERFACE_BEGIN annotation + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INTERFACE_BEGIN, info)); + return info; +} + +void _createInterfaceEndAnnotation(CSTR name) { + // Create and instrument with the INTERFACE_END annotation + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INTERFACE_END, (void*) name)); +} + + +void _setInterfaceBeginAnnotationValue(AnnoInterfaceInfo *info, void *value) { + info->value = value; +} + +void _createOPDefineAnnotation() { + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_DEFINE, NULL)); +} + +void _createPotentialOPAnnotation(CSTR label) { + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(POTENTIAL_OP, label)); +} + +void _createOPCheckAnnotation(CSTR label) { + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CHECK, label)); +} + +void _createOPClearAnnotation() { + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR, NULL)); +} + +void _createOPClearDefineAnnotation() { + cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR_DEFINE, NULL)); +} diff --git a/spec-analysis/specannotation.h b/spec-analysis/specannotation.h new file mode 100644 index 0000000..5ab80ef --- /dev/null +++ b/spec-analysis/specannotation.h @@ -0,0 +1,230 @@ +#ifndef _SPECANNOTATION_H +#define _SPECANNOTATION_H + +#include "modeltypes.h" +#include "model-assert.h" +#include "methodcall.h" +#include "action.h" +#include "spec_common.h" +#include "hashtable.h" + +using namespace std; + +/** + We can only pass a void* pointer from the real program execution to the + checking engine, so we need to wrap the key information into that pointer. + We use the SpecAnntotation struct to represent that info. Different types + here mean different annotations. + + FIXME: Currently we actually do not need to have the INTERFACE_END types. We + basically wrap the MethodCall* pointer of the method call in the + INTERFACE_BEGIN type of annotation. +*/ +typedef enum SpecAnnoType { + INIT, POTENTIAL_OP, OP_DEFINE, OP_CHECK, OP_CLEAR, OP_CLEAR_DEFINE, + INTERFACE_BEGIN, INTERFACE_END +} SpecAnnoType; + +inline CSTR specAnnoType2Str(SpecAnnoType type) { + switch (type) { + case INIT: + return "INIT"; + case POTENTIAL_OP: + return "POTENTIAL_OP"; + case OP_DEFINE: + return "OP_DEFINE"; + case OP_CHECK: + return "OP_CHECK"; + case OP_CLEAR: + return "OP_CLEAR"; + case OP_CLEAR_DEFINE: + return "OP_CLEAR_DEFINE"; + case INTERFACE_BEGIN: + return "INTERFACE_BEGIN"; + case INTERFACE_END: + return "INTERFACE_END"; + default: + return "UNKNOWN_TYPE"; + } +} + +typedef +struct SpecAnnotation { + SpecAnnoType type; + const void *annotation; + + SpecAnnotation(SpecAnnoType type, const void *anno); + +} SpecAnnotation; + +typedef bool (*CheckCommutativity_t)(Method, Method); +/** + The first method is the target (to update its state), and the second method + is the method that should be executed (to access its method call info (ret + & args) +*/ +typedef bool (*StateTransition_t)(Method, Method); +typedef bool (*CheckState_t)(Method, Method); +typedef void (*UpdateState_t)(Method); +// Copy the second state to the first state +typedef void (*CopyState_t)(Method, Method); + +/** + This struct contains a commutativity rule: two method calls represented by + two unique integers and a function that takes two "info" pointers (with the + return value and the arguments) and returns a boolean to represent whether + the two method calls are commutable. +*/ +typedef +struct CommutativityRule { + CSTR method1; + CSTR method2; + + /** The plain text of the rule (debugging purpose) */ + CSTR rule; + CheckCommutativity_t condition; + + CommutativityRule(CSTR method1, CSTR method2, CSTR rule, + CheckCommutativity_t condition); + + bool isRightRule(Method m1, Method m2); + + bool checkCondition(Method m1, Method m2); + +} CommutativityRule; + +typedef enum CheckFunctionType { + INITIAL, COPY, CLEAR, FINAL, PRINT_STATE, TRANSITION, PRE_CONDITION, + JUSTIFYING_PRECONDITION, SIDE_EFFECT, JUSTIFYING_POSTCONDITION, + POST_CONDITION, PRINT_VALUE +} CheckFunctionType; + +typedef struct NamedFunction { + CSTR name; + CheckFunctionType type; + void *function; + + /** + StateTransition_t transition; + CheckState_t preCondition; + CheckState_t postCondition; + */ + NamedFunction(CSTR name, CheckFunctionType type, void *function); +} NamedFunction; + +typedef +struct StateFunctions { + NamedFunction *transition; + NamedFunction *preCondition; + NamedFunction *justifyingPrecondition; + NamedFunction *justifyingPostcondition; + NamedFunction *postCondition; + NamedFunction *print; + + StateFunctions(NamedFunction *transition, NamedFunction *preCondition, + NamedFunction *justifyingPrecondition, + NamedFunction *justifyingPostcondition, + NamedFunction *postCondition, NamedFunction *print); + +} StateFunctions; + +/** A map from a constant c-string to its set of checking functions */ +typedef HashTable StateFuncMap; + +typedef +struct AnnoInit { + /** + For the initialization of a state; We actually assume there are two + special nodes --- INITIAL & FINAL. They actually have a special + MethodCall class representing these two nodes, and their interface name + would be INITIAL and FINAL. For the initial function, we actually also + use it as the state copy function when evaluating the state of other + method calls + + UpdateState_t --> initial + */ + NamedFunction *initial; + + /** + TODO: Currently we just have this "final" field, which was supposed to + be a final checking function after all method call nodes have been + executed on the graph. However, before we think it through, this might + potentially be a violation of composability + + CheckState_t --> final; + */ + NamedFunction *final; + + /** + For copying out an existing state from a previous method call + + CopyState_t --> copy + */ + NamedFunction *copy; + + /** + For clearing out an existing state object + + UpdateState_t --> delete + */ + NamedFunction *clear; + + + /** + For printing out the state + + UpdateState_t --> printState + */ + NamedFunction *printState; + + /** For the state functions. We can conveniently access to the set of state + * functions with a hashmap */ + StateFuncMap *funcMap; + + /** For commutativity rules */ + CommutativityRule *commuteRules; + int commuteRuleNum; + + AnnoInit(NamedFunction *initial, NamedFunction *final, NamedFunction *copy, + NamedFunction *clear, NamedFunction *printState, CommutativityRule + *commuteRules, int ruleNum); + + void addInterfaceFunctions(CSTR name, StateFunctions *funcs); + +} AnnoInit; + +typedef +struct AnnoInterfaceInfo { + CSTR name; + void *value; + + AnnoInterfaceInfo(CSTR name); +} AnnoInterfaceInfo; + +/********** Universal functions for rewriting the program **********/ + +#ifdef __cplusplus +extern "C" { +#endif + +AnnoInterfaceInfo* _createInterfaceBeginAnnotation(CSTR name); + +void _createInterfaceEndAnnotation(CSTR name); + +void _setInterfaceBeginAnnotationValue(AnnoInterfaceInfo *info, void *value); + +void _createOPDefineAnnotation(); + +void _createPotentialOPAnnotation(CSTR label); + +void _createOPCheckAnnotation(CSTR label); + +void _createOPClearAnnotation(); + +void _createOPClearDefineAnnotation(); + +#ifdef __cplusplus +}; +#endif + +#endif diff --git a/test/Makefile b/test/Makefile index 9d7acb0..8f19b46 100644 --- a/test/Makefile +++ b/test/Makefile @@ -11,13 +11,14 @@ include $(DIR)/Makefile DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS)))) CPPFLAGS += -I$(BASE) -I$(BASE)/include +CFLAGS += -I$(BASE) -I$(BASE)/include all: $(OBJECTS) -include $(DEPS) %.o: %.c - $(CC) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME) + $(CC) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CFLAGS) -L$(BASE) -l$(LIB_NAME) %.o: %.cc $(CXX) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME) diff --git a/test/iriw.cc b/test/iriw.cc deleted file mode 100644 index fddbf1a..0000000 --- a/test/iriw.cc +++ /dev/null @@ -1,66 +0,0 @@ -/** - * @file iriw.cc - * @brief Independent read and independent write test - */ - -#include -#include -#include - -#include "wildcard.h" -#include "model-assert.h" - -using namespace std; - -atomic_int x, y; -int r1, r2, r3, r4; /* "local" variables */ - -static void a(void *obj) -{ - x.store(1, memory_order_seq_cst); -} - -static void b(void *obj) -{ - y.store(1, memory_order_seq_cst); -} - -static void c(void *obj) -{ - r1 = x.load(memory_order_acquire); - r2 = y.load(memory_order_seq_cst); -} - -static void d(void *obj) -{ - r3 = y.load(memory_order_acquire); - r4 = x.load(memory_order_seq_cst); -} - - -int user_main(int argc, char **argv) -{ - thrd_t t1, t2, t3, t4; - - atomic_init(&x, 0); - atomic_init(&y, 0); - - printf("Main thread: creating 4 threads\n"); - thrd_create(&t1, (thrd_start_t)&a, NULL); - thrd_create(&t2, (thrd_start_t)&b, NULL); - thrd_create(&t3, (thrd_start_t)&c, NULL); - thrd_create(&t4, (thrd_start_t)&d, NULL); - - thrd_join(t1); - thrd_join(t2); - thrd_join(t3); - thrd_join(t4); - printf("Main thread is finished\n"); - - /* - * This condition should not be hit if the execution is SC */ - bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0); - printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4); - MODEL_ASSERT(!sc); - return 0; -} diff --git a/test/iriw_wildcard.cc b/test/iriw_wildcard.cc deleted file mode 100644 index 5c52455..0000000 --- a/test/iriw_wildcard.cc +++ /dev/null @@ -1,66 +0,0 @@ -/** - * @file iriw.cc - * @brief Independent read and independent write test - */ - -#include -#include -#include - -#include "wildcard.h" -#include "model-assert.h" - -using namespace std; - -atomic_int x, y; -int r1, r2, r3, r4; /* "local" variables */ - -static void a(void *obj) -{ - x.store(1, wildcard(1)); -} - -static void b(void *obj) -{ - y.store(1, wildcard(2)); -} - -static void c(void *obj) -{ - r1 = x.load(wildcard(3)); - r2 = y.load(wildcard(4)); -} - -static void d(void *obj) -{ - r3 = y.load(wildcard(5)); - r4 = x.load(wildcard(6)); -} - - -int user_main(int argc, char **argv) -{ - thrd_t t1, t2, t3, t4; - - atomic_init(&x, 0); - atomic_init(&y, 0); - - printf("Main thread: creating 4 threads\n"); - thrd_create(&t1, (thrd_start_t)&a, NULL); - thrd_create(&t2, (thrd_start_t)&b, NULL); - thrd_create(&t3, (thrd_start_t)&c, NULL); - thrd_create(&t4, (thrd_start_t)&d, NULL); - - thrd_join(t1); - thrd_join(t2); - thrd_join(t3); - thrd_join(t4); - printf("Main thread is finished\n"); - - /* - * This condition should not be hit if the execution is SC */ - bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0); - //MODEL_ASSERT(!sc); - - return 0; -} diff --git a/threads.cc b/threads.cc index a06af84..a0bc029 100644 --- a/threads.cc +++ b/threads.cc @@ -16,13 +16,13 @@ /** Allocate a stack for a new thread. */ static void * stack_allocate(size_t size) { - return Thread_malloc(size); + return snapshot_malloc(size); } /** Free a stack for a terminated thread. */ static void stack_free(void *stack) { - Thread_free(stack); + snapshot_free(stack); } /** diff --git a/traceanalysis.h b/traceanalysis.h index d363150..df3356a 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -2,7 +2,6 @@ #define TRACE_ANALYSIS_H #include "model.h" - class TraceAnalysis { public: /** setExecution is called once after installation with a reference to @@ -31,20 +30,6 @@ class TraceAnalysis { virtual void finish() = 0; - /** This method is used to inspect the normal/abnormal model - * action. */ - virtual void inspectModelAction(ModelAction *act) {} - - /** This method will be called by when a plugin is installed by the - * model checker. */ - virtual void actionAtInstallation() {} - - /** This method will be called when the model checker finishes the - * executions; With this method, the model checker can alter the - * state of the plugin and then the plugin can choose whether or not - * restart the model checker. */ - virtual void actionAtModelCheckingFinish() {} - SNAPSHOTALLOC }; #endif