From: Peizhao Ou Date: Tue, 24 Oct 2017 01:48:09 +0000 (-0700) Subject: Adds back the necessary bugfix from previous commit "01f8364" that were accidentally... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=refs%2Fheads%2Fppopp17-artifact;p=model-checker.git Adds back the necessary bugfix from previous commit "01f8364" that were accidentally overwritten --- diff --git a/.gitignore b/.gitignore index 8df9862..2d24b55 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,5 @@ /doc/docs /benchmarks /README.html +/cdsspec-compiler/classes +/cdsspec-compiler/src/edu/uci/eecs/utilParser diff --git a/common.h b/common.h index 62c16f4..7be72d7 100644 --- a/common.h +++ b/common.h @@ -9,8 +9,9 @@ #include "config.h" extern int model_out; +extern int switch_alloc; -#define model_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0) +#define model_print(fmt, ...) do { switch_alloc = 1; dprintf(model_out, fmt, ##__VA_ARGS__); switch_alloc = 0; } while (0) #ifdef CONFIG_DEBUG #define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0) diff --git a/execution.cc b/execution.cc index eaf245d..2a7e0da 100644 --- a/execution.cc +++ b/execution.cc @@ -34,6 +34,7 @@ struct model_snapshot_members { too_many_reads(false), no_valid_reads(false), bad_synchronization(false), + bad_sc_read(false), asserted(false) { } @@ -53,6 +54,7 @@ struct model_snapshot_members { bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; + bool bad_sc_read; bool asserted; SNAPSHOTALLOC @@ -202,6 +204,13 @@ 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)); @@ -1306,6 +1315,12 @@ 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; @@ -1385,6 +1400,8 @@ 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) @@ -1415,6 +1432,7 @@ 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(); } @@ -1583,9 +1601,6 @@ 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) @@ -1619,12 +1634,6 @@ 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 @@ -1756,9 +1765,10 @@ 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) - continue; - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + 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; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && diff --git a/execution.h b/execution.h index fd117ab..8c8031c 100644 --- a/execution.h +++ b/execution.h @@ -117,7 +117,7 @@ public: action_list_t * get_action_trace() { return &action_trace; } CycleGraph * const get_mo_graph() { return mo_graph; } - + int get_execution_number() const; SNAPSHOTALLOC @@ -134,6 +134,7 @@ 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 2d48989..4b5d1c2 100644 --- a/impatomic.cc +++ b/impatomic.cc @@ -26,11 +26,15 @@ 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 b58486d..bb6e3d6 100644 --- a/include/cdsannotate.h +++ b/include/cdsannotate.h @@ -2,13 +2,6 @@ #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 1b9ce6b..b4273ee 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -2330,23 +2330,28 @@ inline bool atomic_compare_exchange_strong inline void* atomic_fetch_add_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) { - 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__; } + 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__; +} -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__ ) -{ - 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__; } +{ 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__; +} inline void* atomic_fetch_sub ( volatile atomic_address* __a__, ptrdiff_t __m__ ) diff --git a/main.cc b/main.cc index 127ffd1..502f499 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", optional_argument, NULL, 'u'}, - {"analysis", optional_argument, NULL, 't'}, - {"options", optional_argument, NULL, 'o'}, + {"uninitialized", required_argument, NULL, 'u'}, + {"analysis", required_argument, NULL, 't'}, + {"options", required_argument, NULL, 'o'}, {"maxexecutions", required_argument, NULL, 'x'}, {0, 0, 0, 0} /* Terminator */ }; @@ -231,6 +231,8 @@ static void install_trace_analyses(ModelExecution *execution) TraceAnalysis * ta=(*installedanalysis)[i]; ta->setExecution(execution); model->add_trace_analysis(ta); + /** Call the installation event for each installed plugin */ + ta->actionAtInstallation(); } } @@ -268,6 +270,18 @@ int main(int argc, char **argv) main_argc = argc; main_argv = argv; + /* + * If this printf statement is removed, CDSChecker will fail on an + * assert on some versions of glibc. The first time printf is + * called, it allocated internal buffers. We can't easily snapshot + * libc since we also use it. + */ + + printf("CDSChecker\n" + "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n" + "Distributed under the GPLv2\n" + "Written by Brian Norris and Brian Demsky\n\n"); + /* Configure output redirection for the model-checker */ redirect_output(); diff --git a/model.cc b/model.cc index 8f0efcd..3bac903 100644 --- a/model.cc +++ b/model.cc @@ -2,6 +2,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -22,14 +23,18 @@ ModelChecker *model; ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ params(params), + restart_flag(false), + exit_flag(false), scheduler(new Scheduler()), node_stack(new NodeStack()), execution(new ModelExecution(this, &this->params, scheduler, node_stack)), execution_number(1), diverge(NULL), earliest_diverge(NULL), - trace_analyses() + trace_analyses(), + inspect_plugin(NULL) { + memset(&stats,0,sizeof(struct execution_stats)); } /** @brief Destructor */ @@ -298,6 +303,9 @@ bool ModelChecker::next_execution() checkDataRaces(); run_trace_analyses(); + } else if (inspect_plugin && !execution->is_complete_execution() && + (execution->too_many_steps())) { + inspect_plugin->analyze(execution->get_action_trace()); } record_stats(); @@ -311,6 +319,14 @@ bool ModelChecker::next_execution() if (complete) earliest_diverge = NULL; + if (restart_flag) { + do_restart(); + return true; + } + + if (exit_flag) + return false; + if ((diverge = execution->get_next_backtrack()) == NULL) return false; @@ -330,10 +346,8 @@ 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; } /** @@ -386,6 +400,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) Thread *old = thread_current(); scheduler->set_current_thread(NULL); ASSERT(!old->get_pending()); + if (inspect_plugin != NULL) { + inspect_plugin->inspectModelAction(act); + } old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); @@ -415,9 +432,35 @@ bool ModelChecker::should_terminate_execution() return false; } +/** @brief Exit ModelChecker upon returning to the run loop of the + * model checker. */ +void ModelChecker::exit_model_checker() +{ + exit_flag = true; +} + +/** @brief Restart ModelChecker upon returning to the run loop of the + * model checker. */ +void ModelChecker::restart() +{ + restart_flag = true; +} + +void ModelChecker::do_restart() +{ + restart_flag = false; + diverge = NULL; + earliest_diverge = NULL; + reset_to_initial_state(); + node_stack->full_reset(); + memset(&stats,0,sizeof(struct execution_stats)); + execution_number = 1; +} + /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { + bool has_next; do { thrd_t user_thread; Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); @@ -465,7 +508,17 @@ void ModelChecker::run() t = execution->take_step(curr); } while (!should_terminate_execution()); - } while (next_execution()); + has_next = next_execution(); + if (inspect_plugin != NULL && !has_next) { + inspect_plugin->actionAtModelCheckingFinish(); + // Check if the inpect plugin set the restart flag + if (restart_flag) { + model_print("******* Model-checking RESTART: *******\n"); + has_next = true; + do_restart(); + } + } + } while (has_next); execution->fixup_release_sequences(); diff --git a/model.h b/model.h index 74cb4e1..9448353 100644 --- a/model.h +++ b/model.h @@ -47,6 +47,15 @@ public: void run(); + /** Restart the model checker, intended for pluggins. */ + void restart(); + + /** Exit the model checker, intended for pluggins. */ + void exit_model_checker(); + + /** Check the exit_flag. */ + bool get_exit_flag() const { return exit_flag; } + /** @returns the context for the main model-checking system thread */ ucontext_t * get_system_context() { return &system_context; } @@ -66,12 +75,15 @@ public: void assert_user_bug(const char *msg); const model_params params; - void add_trace_analysis(TraceAnalysis *a) { - trace_analyses.push_back(a); - } - + void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } + void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } MEMALLOC private: + /** Flag indicates whether to restart the model checker. */ + bool restart_flag; + /** Flag indicates whether to exit the model checker. */ + bool exit_flag; + /** The scheduler to use: tracks the running/ready Threads */ Scheduler * const scheduler; NodeStack * const node_stack; @@ -97,6 +109,10 @@ private: ModelVector trace_analyses; + /** @bref Implement restart. */ + void do_restart(); + /** @bref Plugin that can inspect new actions. */ + TraceAnalysis *inspect_plugin; /** @brief The cumulative execution stats */ struct execution_stats stats; void record_stats(); diff --git a/mymemory.cc b/mymemory.cc index 8bb5b46..e8ec080 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -13,11 +13,10 @@ #define REQUESTS_BEFORE_ALLOC 1024 -bool IN_TRACE_ANALYSIS = false; - size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 }; int nextRequest = 0; int howManyFreed = 0; +int switch_alloc = 0; #if !USE_MPROTECT_SNAPSHOT static mspace sStaticSpace = NULL; #endif @@ -126,7 +125,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 4096 +#define BOOTSTRAPBYTES 131072 char bootstrapmemory[BOOTSTRAPBYTES]; size_t offset = 0; @@ -136,7 +135,7 @@ void * HandleEarlyAllocationRequest(size_t sz) sz = (sz + 7) & ~7; if (sz > (BOOTSTRAPBYTES-offset)) { - model_print("OUT OF BOOTSTRAP MEMORY\n"); + model_print("OUT OF BOOTSTRAP MEMORY. Increase the size of BOOTSTRAPBYTES in mymemory.cc\n"); exit(EXIT_FAILURE); } @@ -181,8 +180,11 @@ static void * user_malloc(size_t size) void *malloc(size_t size) { if (user_snapshot_space) { + if (switch_alloc) { + return model_malloc(size); + } /* Only perform user allocations from user context */ - ASSERT(!model || thread_current() || IN_TRACE_ANALYSIS); + ASSERT(!model || thread_current()); return user_malloc(size); } else return HandleEarlyAllocationRequest(size); @@ -191,8 +193,12 @@ void *malloc(size_t size) /** @brief Snapshotting free implementation for user programs */ void free(void * ptr) { - if (!DontFree(ptr)) + if (!DontFree(ptr)) { + if (switch_alloc) { + return model_free(ptr); + } mspace_free(user_snapshot_space, ptr); + } } /** @brief Snapshotting realloc implementation for user programs */ diff --git a/mymemory.h b/mymemory.h index 461f7d1..a62ab83 100644 --- a/mymemory.h +++ b/mymemory.h @@ -47,30 +47,14 @@ 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 e5f4687..bacd067 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -838,6 +838,16 @@ void NodeStack::pop_restofstack(int numAhead) node_list.back()->clear_backtracking(); } +/** Reset the node stack. */ +void NodeStack::full_reset() +{ + for (unsigned int i = 0; i < node_list.size(); i++) + delete node_list[i]; + node_list.clear(); + reset_execution(); + total_nodes = 1; +} + Node * NodeStack::get_head() const { if (node_list.empty() || head_idx < 0) diff --git a/nodestack.h b/nodestack.h index f26100b..6ae96be 100644 --- a/nodestack.h +++ b/nodestack.h @@ -198,6 +198,7 @@ public: Node * get_next() const; void reset_execution(); void pop_restofstack(int numAhead); + void full_reset(); int get_total_nodes() { return total_nodes; } void print() const; diff --git a/spec-analysis/cdsspec.h b/spec-analysis/cdsspec.h index db06189..37f2f5c 100644 --- a/spec-analysis/cdsspec.h +++ b/spec-analysis/cdsspec.h @@ -31,7 +31,7 @@ typedef struct TagInt { int val; TagInt(unsigned int tag, int val) : tag(tag), val(val) { } - + TagInt(int val) : tag(0), val(val) { } }TagInt; @@ -40,12 +40,9 @@ typedef SnapList IntList; typedef SnapSet IntSet; template -class Map: public unordered_map { +class Map: public unordered_map, + std::equal_to, SnapshotAlloc>> { public: - typedef unordered_map map; - - Map() : map() { } - Value get(Key key) { return (*this)[key]; } @@ -54,25 +51,10 @@ class Map: public unordered_map { (*this)[key] = value; } - SNAPSHOTALLOC + 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 Map IntMap; typedef SnapVector DoubleVector; typedef SnapList DoubleList; diff --git a/test-cdsspec/run-all.sh b/test-cdsspec/run-all.sh index 76c59e6..c3145d6 100755 --- a/test-cdsspec/run-all.sh +++ b/test-cdsspec/run-all.sh @@ -1,19 +1,26 @@ -#!/bin/bash -# +#!/bin/bash -e -BENCHS=(ms-queue linuxrwlocks mcs-lock chase-lev-deque-bugfix treiber-stack - ticket-lock seqlock read-copy-update concurrent-hashmap spsc-bugfix mpmc-queue) +BENCHS=( + 'ms-queue'\ + 'linuxrwlocks' \ + 'mcs-lock' \ + 'chase-lev-deque-bugfix' \ + 'ticket-lock' \ + 'seqlock' \ + 'read-copy-update' \ + 'spsc-bugfix' \ + 'mpmc-queue' + 'concurrent-hashmap' \ +) -echo ${BENCHS[*]} -for i in ${BENCHS[*]}; do - echo "---------- Start to run $i ----------" - tests=$(ls $i/testcase[1-9]) - if [ -e "$i/main" ]; then - tests=($tests "$i/main") - fi - if [ -e "$i/testcase" ]; then - tests=($tests "$i/testcase") - fi +for bench in ${BENCHS[@]}; do + echo "---------- Start to run ${bench} ----------" + # Clear the test cases. + tests=() + tests=$(ls ${bench}/testcase[1-9] 2>/dev/null || true) + + [ -e "${bench}/main" ] && tests+=("${bench}/main") + [ -e "${bench}/testcase" ] && tests+=("${bench}/testcase") for j in ${tests[*]}; do ./run.sh $j -m2 -y -u3 -tSPEC diff --git a/threads.cc b/threads.cc index a0bc029..a06af84 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 snapshot_malloc(size); + return Thread_malloc(size); } /** Free a stack for a terminated thread. */ static void stack_free(void *stack) { - snapshot_free(stack); + Thread_free(stack); } /** diff --git a/traceanalysis.h b/traceanalysis.h index df3356a..d363150 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -2,6 +2,7 @@ #define TRACE_ANALYSIS_H #include "model.h" + class TraceAnalysis { public: /** setExecution is called once after installation with a reference to @@ -30,6 +31,20 @@ class TraceAnalysis { virtual void finish() = 0; + /** This method is used to inspect the normal/abnormal model + * action. */ + virtual void inspectModelAction(ModelAction *act) {} + + /** This method will be called by when a plugin is installed by the + * model checker. */ + virtual void actionAtInstallation() {} + + /** This method will be called when the model checker finishes the + * executions; With this method, the model checker can alter the + * state of the plugin and then the plugin can choose whether or not + * restart the model checker. */ + virtual void actionAtModelCheckingFinish() {} + SNAPSHOTALLOC }; #endif