From: Brian Demsky Date: Thu, 15 Nov 2012 02:15:04 +0000 (-0800) Subject: merge X-Git-Tag: oopsla2013~539^2 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=45206350b4022732229f8a48a3c7b08885e874a7;hp=caa1df880547acce2804221c8e6995170a5121eb;p=model-checker.git merge Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker Conflicts: config.h model.cc --- diff --git a/README b/README new file mode 100644 index 0000000..12a02ff --- /dev/null +++ b/README @@ -0,0 +1,59 @@ +**************************************** +CDSChecker Readme +**************************************** + +This is an evaluation-only version of CDSChecker. Please do not distribute. + +CDSChecker compiles as a dynamically-linked shared library by simply running +'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM +(clang/clang++) and GCC. + +Test programs should use the standard C11/C++11 library headers +(/, , , ) and must +name their main routine as user_main(int, char**) rather than main(int, char**). +We only support C11 thread syntax (thrd_t, etc. from ). + +Test programs may also use our included happens-before race detector by +including and utilizing the appropriate functions +(store_{8,16,32,64}() and load_{8,16,32,64}()) for loading/storing data from/to +from non-atomic shared memory. + +Test programs should be compiled against our shared library (libmodel.so) using +the headers in the include/ directory. Then the shared library must be made +available to the dynamic linker, using the LD_LIBRARY_PATH environment +variable, for instance. + +Sample run instructions: + +$ make +$ export LD_LIBRARY_PATH=. +$ ./test/userprog.o # Runs simple test program +$ ./test/userprog.o -h # Prints help information +Usage: [MC_OPTIONS] -- [PROGRAM ARGUMENTS] + +Options: +-h Display this help message and exit +-m Maximum times a thread can read from the same write + while other writes exist. Default: 0 +-M Maximum number of future values that can be sent to + the same read. Default: 0 +-s Maximum actions that the model checker will wait for + a write from the future past the expected number of + actions. Default: 100 +-S Future value expiration sloppiness. Default: 10 +-f Specify a fairness window in which actions that are + enabled sufficiently many times should receive + priority for execution. Default: 0 +-e Enabled count. Default: 1 +-b Upper length bound. Default: 0 +-- Program arguments follow. + + +Note that we also provide a series of benchmarks (distributed separately), +which can be placed under the benchmarks/ directory. After building CDSChecker, +you can build and run the benchmarks as follows: + + cd benchmarks + make + ./run.sh barrier/barrier -f 10 -m 2 # runs barrier test with fairness/memory liveness + ./bench.sh # run all benchmarks twice, with timing results; all logged to diff --git a/config.h b/config.h index 9488542..aacbb81 100644 --- a/config.h +++ b/config.h @@ -48,6 +48,10 @@ /* Size of stack to allocate for a thread. */ #define STACK_SIZE (1024 * 1024) +/** How many shadow tables of memory to preallocate for data race detector. */ #define SHADOWBASETABLES 4 +/** Enable debugging assertions (via ASSERT()) */ +#define CONFIG_ASSERT + #endif diff --git a/datarace.cc b/datarace.cc index 732d6ff..ac364d7 100644 --- a/datarace.cc +++ b/datarace.cc @@ -32,7 +32,7 @@ void * table_calloc(size_t size) { /** This function looks up the entry in the shadow table corresponding to a * given address.*/ -static uint64_t * lookupAddressEntry(void * address) { +static uint64_t * lookupAddressEntry(const void * address) { struct ShadowTable *currtable=root; #if BIT48 currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT]; @@ -91,7 +91,7 @@ static void expandRecord(uint64_t * shadow) { } /** This function is called when we detect a data race.*/ -static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) { +static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) { struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace)); race->oldthread=oldthread; race->oldclock=oldclock; @@ -226,7 +226,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) } /** This function does race detection on a read for an expanded record. */ -void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) { +void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) { struct RaceRecord * record=(struct RaceRecord *) (*shadow); /* Check for datarace against last write. */ @@ -284,7 +284,7 @@ void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, Cl } /** This function does race detection on a read. */ -void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) { +void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) { uint64_t * shadow=lookupAddressEntry(location); uint64_t shadowval=*shadow; diff --git a/datarace.h b/datarace.h index 627b8cc..2fb1a7f 100644 --- a/datarace.h +++ b/datarace.h @@ -36,14 +36,14 @@ struct DataRace { bool isnewwrite; /* Address of data race. */ - void *address; + const void *address; }; #define MASK16BIT 0xffff void initRaceDetector(); void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock); -void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock); +void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock); bool checkDataRaces(); void printRace(struct DataRace *race); diff --git a/include/librace.h b/include/librace.h index 591b292..cabf066 100644 --- a/include/librace.h +++ b/include/librace.h @@ -16,10 +16,10 @@ extern "C" { void store_32(void *addr, uint32_t val); void store_64(void *addr, uint64_t val); - uint8_t load_8(void *addr); - uint16_t load_16(void *addr); - uint32_t load_32(void *addr); - uint64_t load_64(void *addr); + uint8_t load_8(const void *addr); + uint16_t load_16(const void *addr); + uint32_t load_32(const void *addr); + uint64_t load_64(const void *addr); #ifdef __cplusplus } diff --git a/librace.cc b/librace.cc index 3c56d96..95b97aa 100644 --- a/librace.cc +++ b/librace.cc @@ -54,7 +54,7 @@ void store_64(void *addr, uint64_t val) (*(uint64_t *)addr) = val; } -uint8_t load_8(void *addr) +uint8_t load_8(const void *addr) { DEBUG("addr = %p\n", addr); thread_id_t tid=thread_current()->get_id(); @@ -63,40 +63,40 @@ uint8_t load_8(void *addr) return *((uint8_t *)addr); } -uint16_t load_16(void *addr) +uint16_t load_16(const void *addr) { DEBUG("addr = %p\n", addr); thread_id_t tid=thread_current()->get_id(); ClockVector * cv=model->get_cv(tid); raceCheckRead(tid, addr, cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv); return *((uint16_t *)addr); } -uint32_t load_32(void *addr) +uint32_t load_32(const void *addr) { DEBUG("addr = %p\n", addr); thread_id_t tid=thread_current()->get_id(); ClockVector * cv=model->get_cv(tid); raceCheckRead(tid, addr, cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+2), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+3), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+2), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+3), cv); return *((uint32_t *)addr); } -uint64_t load_64(void *addr) +uint64_t load_64(const void *addr) { DEBUG("addr = %p\n", addr); thread_id_t tid=thread_current()->get_id(); ClockVector * cv=model->get_cv(tid); raceCheckRead(tid, addr, cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+1), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+2), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+3), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+4), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+5), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+6), cv); - raceCheckRead(tid, (void *)(((uintptr_t)addr)+7), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+1), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+2), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+3), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+4), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+5), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+6), cv); + raceCheckRead(tid, (const void *)(((uintptr_t)addr)+7), cv); return *((uint64_t *)addr); } diff --git a/model.cc b/model.cc index 94620ea..922a0d6 100644 --- a/model.cc +++ b/model.cc @@ -18,6 +18,17 @@ ModelChecker *model; +/** + * Structure for holding small ModelChecker members that should be snapshotted + */ +struct model_snapshot_members { + ModelAction *current_action; + unsigned int next_thread_id; + modelclock_t used_sequence_numbers; + Thread *nextThread; + ModelAction *next_backtrack; +}; + /** @brief Constructor */ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ @@ -255,10 +266,11 @@ bool ModelChecker::is_deadlocked() const { bool blocking_threads = false; for (unsigned int i = 0; i < get_num_threads(); i++) { - Thread *t = get_thread(int_to_id(i)); - if (scheduler->is_enabled(t) != THREAD_DISABLED) + thread_id_t tid = int_to_id(i); + if (is_enabled(tid)) return false; - else if (!t->is_model_thread() && t->get_pending()) + Thread *t = get_thread(tid); + if (!t->is_model_thread() && t->get_pending()) blocking_threads = true; } return blocking_threads; @@ -294,7 +306,7 @@ bool ModelChecker::next_execution() pending_rel_seqs->size()); - if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) { + if (isfinalfeasible() || DBG_ENABLED()) { checkDataRaces(); print_summary(); } @@ -863,6 +875,16 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { return true; } +/** + * Stores the ModelAction for the current thread action. Call this + * immediately before switching from user- to system-context to pass + * data between them. + * @param act The ModelAction created by the user-thread action + */ +void ModelChecker::set_current_action(ModelAction *act) { + priv->current_action = act; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -1535,7 +1557,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, ModelAction *last = get_last_action(int_to_id(i)); Thread *th = get_thread(int_to_id(i)); if ((last && rf->happens_before(last)) || - !scheduler->is_enabled(th) || + !is_enabled(th) || th->is_complete()) future_ordered = true; @@ -2177,6 +2199,26 @@ Thread * ModelChecker::get_thread(ModelAction *act) const return get_thread(act->get_tid()); } +/** + * @brief Check if a Thread is currently enabled + * @param t The Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(Thread *t) const +{ + return scheduler->is_enabled(t); +} + +/** + * @brief Check if a Thread is currently enabled + * @param tid The ID of the Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(thread_id_t tid) const +{ + return scheduler->is_enabled(tid); +} + /** * Switch from a user-context to the "master thread" context (a.k.a. system * context). This switch is made with the intention of exploring a particular diff --git a/model.h b/model.h index 6d702b0..6e7f224 100644 --- a/model.h +++ b/model.h @@ -23,6 +23,7 @@ class CycleGraph; class Promise; class Scheduler; class Thread; +struct model_snapshot_members; /** @brief Shorthand for a list of release sequence heads */ typedef std::vector< const ModelAction *, ModelAlloc > rel_heads_list_t; @@ -50,18 +51,7 @@ struct model_params { struct PendingFutureValue { ModelAction *writer; - ModelAction * act; -}; - -/** - * Structure for holding small ModelChecker members that should be snapshotted - */ -struct model_snapshot_members { - ModelAction *current_action; - unsigned int next_thread_id; - modelclock_t used_sequence_numbers; - Thread *nextThread; - ModelAction *next_backtrack; + ModelAction *act; }; /** @brief Records information regarding a single pending release sequence */ @@ -97,6 +87,9 @@ public: Thread * get_thread(thread_id_t tid) const; Thread * get_thread(ModelAction *act) const; + bool is_enabled(Thread *t) const; + bool is_enabled(thread_id_t tid) const; + thread_id_t get_next_id(); unsigned int get_num_threads() const; Thread * get_current_thread(); @@ -122,7 +115,6 @@ public: void set_bad_synchronization() { bad_synchronization = true; } const model_params params; - Scheduler * get_scheduler() { return scheduler;} Node * get_curr_node(); MEMALLOC @@ -142,13 +134,7 @@ private: void wake_up_sleeping_actions(ModelAction * curr); modelclock_t get_next_seq_num(); - /** - * Stores the ModelAction for the current thread action. Call this - * immediately before switching from user- to system-context to pass - * data between them. - * @param act The ModelAction created by the user-thread action - */ - void set_current_action(ModelAction *act) { priv->current_action = act; } + void set_current_action(ModelAction *act); Thread * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); diff --git a/promise.cc b/promise.cc index 68290ee..90591eb 100644 --- a/promise.cc +++ b/promise.cc @@ -11,11 +11,10 @@ bool Promise::increment_threads(thread_id_t tid) { return false; synced_thread[id]=true; - enabled_type_t * enabled=model->get_scheduler()->get_enabled(); unsigned int sync_size=synced_thread.size(); int promise_tid=id_to_int(read->get_tid()); for(unsigned int i=1;iget_num_threads();i++) { - if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && (enabled[i] != THREAD_DISABLED)) { + if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && model->is_enabled(int_to_id(i))) { return false; } } @@ -23,10 +22,9 @@ bool Promise::increment_threads(thread_id_t tid) { } bool Promise::check_promise() { - enabled_type_t * enabled=model->get_scheduler()->get_enabled(); unsigned int sync_size=synced_thread.size(); for(unsigned int i=1;iget_num_threads();i++) { - if ((i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED)) { + if ((i >= sync_size || !synced_thread[i]) && model->is_enabled(int_to_id(i))) { return false; } } diff --git a/schedule.cc b/schedule.cc index 93379c2..26217d0 100644 --- a/schedule.cc +++ b/schedule.cc @@ -35,13 +35,29 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) { /** * @brief Check if a Thread is currently enabled + * + * Check if a Thread is currently enabled. "Enabled" includes both + * THREAD_ENABLED and THREAD_SLEEP_SET. * @param t The Thread to check * @return True if the Thread is currently enabled */ bool Scheduler::is_enabled(Thread *t) const { - int id = id_to_int(t->get_id()); - return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED); + return is_enabled(t->get_id()); +} + +/** + * @brief Check if a Thread is currently enabled + * + * Check if a Thread is currently enabled. "Enabled" includes both + * THREAD_ENABLED and THREAD_SLEEP_SET. + * @param tid The ID of the Thread to check + * @return True if the Thread is currently enabled + */ +bool Scheduler::is_enabled(thread_id_t tid) const +{ + int i = id_to_int(tid); + return (i >= enabled_len) ? false : (enabled[i] != THREAD_DISABLED); } enabled_type_t Scheduler::get_enabled(Thread *t) { diff --git a/schedule.h b/schedule.h index 7267059..da91fdd 100644 --- a/schedule.h +++ b/schedule.h @@ -36,6 +36,7 @@ public: enabled_type_t get_enabled(Thread *t); void update_sleep_set(Node *n); bool is_enabled(Thread *t) const; + bool is_enabled(thread_id_t tid) const; SNAPSHOTALLOC private: