From: Brian Demsky Date: Thu, 15 Nov 2012 04:55:23 +0000 (-0800) Subject: Merge branch 'master' of /home/git/model-checker X-Git-Tag: oopsla2013~539 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=44118f596eb7cd9b4b0b5037fbbf958db001accc;hp=58381d5994f91544f907e1066a02befda11da7c1;p=model-checker.git Merge branch 'master' of /home/git/model-checker --- 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/common.cc b/common.cc index b274989..f4aa7ec 100644 --- a/common.cc +++ b/common.cc @@ -2,6 +2,8 @@ #include #include +#include + #include "common.h" #include "model.h" #include "stacktrace.h" @@ -40,3 +42,13 @@ void assert_hook(void) { printf("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__); } + +void model_assert(bool expr, const char *file, int line) +{ + if (!expr) { + printf(" [BUG] Program has hit assertion in file %s at line %d\n", + file, line); + model->set_assert(); + model->switch_to_master(NULL); + } +} diff --git a/common.h b/common.h index 50410ea..81b2672 100644 --- a/common.h +++ b/common.h @@ -20,6 +20,7 @@ void assert_hook(void); +#ifdef CONFIG_ASSERT #define ASSERT(expr) \ do { \ if (!(expr)) { \ @@ -30,6 +31,10 @@ do { \ exit(EXIT_FAILURE); \ } \ } while (0) +#else +#define ASSERT(expr) \ + do { } while (0) +#endif /* CONFIG_ASSERT */ #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__) diff --git a/config.h b/config.h index 971ea27..891dfd7 100644 --- a/config.h +++ b/config.h @@ -9,6 +9,10 @@ /* #ifndef CONFIG_DEBUG #define CONFIG_DEBUG #endif + + #ifndef CONFIG_ASSERT + #define CONFIG_ASSERT + #endif */ /** Turn on support for dumping cyclegraphs as dot files at each @@ -44,5 +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 270e523..ac364d7 100644 --- a/datarace.cc +++ b/datarace.cc @@ -5,29 +5,45 @@ #include #include "mymemory.h" #include "clockvector.h" +#include "config.h" struct ShadowTable *root; std::vector unrealizedraces; +void *memory_base; +void *memory_top; + /** This function initialized the data race detector. */ void initRaceDetector() { root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1); + memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable)*SHADOWBASETABLES, 1); + memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable)*SHADOWBASETABLES; +} + +void * table_calloc(size_t size) { + if ((((char *)memory_base)+size)>memory_top) { + return snapshot_calloc(size, 1); + } else { + void *tmp=memory_base; + memory_base=((char *)memory_base)+size; + return tmp; + } } /** 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]; if (currtable==NULL) { - currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1)); + currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = table_calloc(sizeof(struct ShadowTable))); } #endif struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT]; if (basetable==NULL) { - basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1)); + basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable))); } return &basetable->array[((uintptr_t)address)&MASK16BIT]; } @@ -75,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; @@ -210,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. */ @@ -268,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/include/model-assert.h b/include/model-assert.h new file mode 100644 index 0000000..a091e15 --- /dev/null +++ b/include/model-assert.h @@ -0,0 +1,15 @@ +#ifndef __MODEL_ASSERT_H__ +#define __MODEL_ASSERT_H__ + +#if __cplusplus +extern "C" { +#endif + +void model_assert(bool expr, const char *file, int line); +#define MODEL_ASSERT(expr) model_assert((expr), __FILE__, __LINE__) + +#if __cplusplus +} +#endif + +#endif /* __MODEL_ASSERT_H__ */ 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/main.cc b/main.cc index 8a17a18..fb4acbe 100644 --- a/main.cc +++ b/main.cc @@ -20,6 +20,8 @@ static void param_defaults(struct model_params * params) { params->fairwindow = 0; params->enabledcount = 1; params->bound = 0; + params->maxfuturevalues = 0; + params->expireslop = 10; } static void print_usage(struct model_params *params) { @@ -33,21 +35,24 @@ static void print_usage(struct model_params *params) { "-h Display this help message and exit\n" "-m Maximum times a thread can read from the same write\n" " while other writes exist. Default: %d\n" +"-M Maximum number of future values that can be sent to\n" +" the same read. Default: %d\n" "-s Maximum actions that the model checker will wait for\n" " a write from the future past the expected number of\n" " actions. Default: %d\n" +"-S Future value expiration sloppiness. Default: %u\n" "-f Specify a fairness window in which actions that are\n" " enabled sufficiently many times should receive\n" " priority for execution. Default: %d\n" "-e Enabled count. Default: %d\n" "-b Upper length bound. Default: %d\n" "-- Program arguments follow.\n\n", -params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount, params->bound); +params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound); exit(EXIT_SUCCESS); } static void parse_options(struct model_params *params, int *argc, char ***argv) { - const char *shortopts = "hm:s:f:e:b:"; + const char *shortopts = "hm:M:s:S:f:e:b:"; int opt; bool error = false; while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) { @@ -58,6 +63,9 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) case 's': params->maxfuturedelay = atoi(optarg); break; + case 'S': + params->expireslop = atoi(optarg); + break; case 'f': params->fairwindow = atoi(optarg); break; @@ -70,13 +78,18 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) case 'm': params->maxreads = atoi(optarg); break; + case 'M': + params->maxfuturevalues = atoi(optarg); + break; default: /* '?' */ error = true; break; } } - (*argc) -= optind; - (*argv) += optind; + (*argv)[optind - 1] = (*argv)[0]; + (*argc) -= (optind - 1); + (*argv) += (optind - 1); + optind = 1; if (error) print_usage(params); diff --git a/model.cc b/model.cc index 78907f1..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 */ @@ -101,7 +112,7 @@ thread_id_t ModelChecker::get_next_id() } /** @return the number of user threads created during this execution */ -unsigned int ModelChecker::get_num_threads() +unsigned int ModelChecker::get_num_threads() const { return priv->next_thread_id; } @@ -244,6 +255,27 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { } } +/** + * Check if we are in a deadlock. Should only be called at the end of an + * execution, although it should not give false positives in the middle of an + * execution (there should be some ENABLED thread). + * + * @return True if program is in a deadlock; false otherwise + */ +bool ModelChecker::is_deadlocked() const +{ + bool blocking_threads = false; + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + if (is_enabled(tid)) + return false; + Thread *t = get_thread(tid); + if (!t->is_model_thread() && t->get_pending()) + blocking_threads = true; + } + return blocking_threads; +} + /** * Queries the model-checker for more executions to explore and, if one * exists, resets the model-checker state to execute a new execution. @@ -257,6 +289,8 @@ bool ModelChecker::next_execution() num_executions++; + if (is_deadlocked()) + printf("ERROR: DEADLOCK\n"); if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) @@ -272,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(); } @@ -841,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 @@ -1513,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; @@ -2000,17 +2044,14 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) /* Don't consider more than one seq_cst write if we are a seq_cst read. */ if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - - if (curr->get_sleep_flag() && ! curr->is_seqcst()) { - if (sleep_can_read_from(curr, act)) - curr->get_node()->add_read_from(act); - } else + if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) { + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); + } curr->get_node()->add_read_from(act); + } } /* Include at most one act per-thread that "happens before" curr */ @@ -2158,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 59a0759..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; @@ -37,22 +38,20 @@ struct model_params { unsigned int fairwindow; unsigned int enabledcount; unsigned int bound; + + /** @brief Maximum number of future values that can be sent to the same + * read */ + int maxfuturevalues; + + /** @brief Only generate a new future value/expiration pair if the + * expiration time exceeds the existing one by more than the slop + * value */ + unsigned int expireslop; }; 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 */ @@ -88,8 +87,11 @@ 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(); + unsigned int get_num_threads() const; Thread * get_current_thread(); int switch_to_master(ModelAction *act); @@ -106,13 +108,13 @@ public: void finish_execution(); bool isfeasibleprefix(); void set_assert() {asserted=true;} + bool is_deadlocked() const; /** @brief Alert the model-checker that an incorrectly-ordered * synchronization was made */ void set_bad_synchronization() { bad_synchronization = true; } const model_params params; - Scheduler * get_scheduler() { return scheduler;} Node * get_curr_node(); MEMALLOC @@ -132,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/nodestack.cc b/nodestack.cc index 743cb86..b4f75e0 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -192,26 +192,39 @@ bool Node::misc_empty() { /** - * Adds a value from a weakly ordered future write to backtrack to. + * Adds a value from a weakly ordered future write to backtrack to. This + * operation may "fail" if the future value has already been run (within some + * sloppiness window of this expiration), or if the futurevalues set has + * reached its maximum. + * @see model_params.maxfuturevalues + * * @param value is the value to backtrack to. + * @return True if the future value was successully added; false otherwise */ bool Node::add_future_value(uint64_t value, modelclock_t expiration) { - int suitableindex=-1; + int idx = -1; /* Highest index where value is found */ for (unsigned int i = 0; i < future_values.size(); i++) { if (future_values[i].value == value) { - if (future_values[i].expiration>=expiration) + if (expiration <= future_values[i].expiration) return false; - if (future_index < ((int) i)) { - suitableindex=i; - } + idx = i; } } - - if (suitableindex!=-1) { - future_values[suitableindex].expiration=expiration; + if (idx > future_index) { + /* Future value hasn't been explored; update expiration */ + future_values[idx].expiration = expiration; return true; + } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) { + /* Future value has been explored and is within the "sloppy" window */ + return false; } - struct future_value newfv={value, expiration}; + + /* Limit the size of the future-values set */ + if (model->params.maxfuturevalues > 0 && + (int)future_values.size() >= model->params.maxfuturevalues) + return false; + + struct future_value newfv = {value, expiration}; future_values.push_back(newfv); return true; } 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: diff --git a/snapshot-interface.cc b/snapshot-interface.cc index 47fafa5..51fe2f0 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -3,7 +3,6 @@ #include #include #include -#include #include #include #include @@ -13,10 +12,11 @@ #include #include "common.h" - +/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g., + * /.../model-checker/test/userprog.o) */ #define MYBINARYNAME "model" #define MYLIBRARYNAME "libmodel.so" -#define MAPFILE_FORMAT "/proc/%d/maps" +#define MAPFILE "/proc/self/maps" SnapshotStack * snapshotObject; @@ -68,28 +68,37 @@ static void SnapshotGlobalSegments(){ pclose(map); } #else + +static void get_binary_name(char *buf, size_t len) +{ + if (readlink("/proc/self/exe", buf, len) == -1) { + perror("readlink"); + exit(EXIT_FAILURE); + } +} + /** The SnapshotGlobalSegments function computes the memory regions * that may contain globals and then configures the snapshotting * library to snapshot them. */ static void SnapshotGlobalSegments(){ - int pid = getpid(); - char buf[9000], filename[100]; + char buf[9000]; + char binary_name[800]; FILE *map; - sprintf(filename, MAPFILE_FORMAT, pid); - map = fopen(filename, "r"); + map = fopen(MAPFILE, "r"); if (!map) { perror("fopen"); exit(EXIT_FAILURE); } + get_binary_name(binary_name, sizeof(binary_name)); while (fgets(buf, sizeof(buf), map)) { char regionname[200] = ""; char r, w, x, p; void *begin, *end; sscanf(buf, "%p-%p %c%c%c%c %*x %*x:%*x %*u %200s\n", &begin, &end, &r, &w, &x, &p, regionname); - if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) { + if (w == 'w' && (strstr(regionname, binary_name) || strstr(regionname, MYLIBRARYNAME))) { size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE; if (len != 0) addMemoryRegionToSnapShot(begin, len); diff --git a/snapshotimp.h b/snapshotimp.h index 2e4929d..b03d285 100644 --- a/snapshotimp.h +++ b/snapshotimp.h @@ -9,7 +9,6 @@ #include #include #include -#include #include #define SHARED_MEMORY_DEFAULT (100 * ((size_t)1 << 20)) // 100mb for the shared memory #define STACK_SIZE_DEFAULT (((size_t)1 << 20) * 20) // 20 mb out of the above 100 mb for my stack diff --git a/test/deadlock.cc b/test/deadlock.cc new file mode 100644 index 0000000..3b26bec --- /dev/null +++ b/test/deadlock.cc @@ -0,0 +1,46 @@ +#include +#include +#include + +#include "librace.h" + +std::mutex *x; +std::mutex *y; +uint32_t shared = 0; + +static void a(void *obj) +{ + x->lock(); + y->lock(); + printf("shared = %u\n", load_32(&shared)); + y->unlock(); + x->unlock(); +} + +static void b(void *obj) +{ + y->lock(); + x->lock(); + store_32(&shared, 16); + printf("write shared = 16\n"); + x->unlock(); + y->unlock(); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + + x = new std::mutex(); + y = new std::mutex(); + + printf("Thread %d: creating 2 threads\n", thrd_current()); + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + + thrd_join(t1); + thrd_join(t2); + printf("Thread %d is finished\n", thrd_current()); + + return 0; +}