From 6e0d0a36ea0f00925308504a44c7b690a9a1d6b7 Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 8 Jan 2019 11:50:41 -0800 Subject: [PATCH] change cds checker to accomdate llvm pass --- #cmodelint.cc# | 74 +++ #main.cc# | 288 ++++++++++ Makefile | 3 +- action.cc | 14 +- action.h | 6 + cmodelint.cc | 225 ++++++++ execution.cc | 1 + include/cmodelint.h | 62 +++ include/impatomic.h | 3 +- include/librace.h | 10 + include/memoryorder.h | 4 +- include/{stdatomic.h => stdatomic2.h} | 0 librace.cc | 49 ++ model.cc | 9 +- snapshot.cc | 2 +- test/memo/double-read-fv | Bin 0 -> 8992 bytes test/memo/fences | Bin 0 -> 9040 bytes test/memo/original | 737 ++++++++++++++++++++++++++ test/memo/output | 687 ++++++++++++++++++++++++ test/memo/rmw2prog | Bin 0 -> 8968 bytes test/memo/script.sh | 19 + test/memo/userprog | Bin 0 -> 9056 bytes test/rmw2prog.c | 31 +- test/userprog.c | 7 +- 24 files changed, 2209 insertions(+), 22 deletions(-) create mode 100644 #cmodelint.cc# create mode 100644 #main.cc# rename include/{stdatomic.h => stdatomic2.h} (100%) create mode 100755 test/memo/double-read-fv create mode 100755 test/memo/fences create mode 100644 test/memo/original create mode 100644 test/memo/output create mode 100755 test/memo/rmw2prog create mode 100755 test/memo/script.sh create mode 100755 test/memo/userprog diff --git a/#cmodelint.cc# b/#cmodelint.cc# new file mode 100644 index 00000000..b67194f2 --- /dev/null +++ b/#cmodelint.cc# @@ -0,0 +1,74 @@ +#include "model.h" +#include "action.h" +#include "cmodelint.h" +#include "threads-model.h" + +memory_order orders[6] = { + memory_order_relaxed, memory_order_consume, memory_order_acquire, + memory_order_release, memory_order_acq_rel, memory_order_seq_cst +}; + +/** Performs a read action.*/ +uint64_t model_read_action(void * obj, memory_order ord) { + return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj)); +} + +uint64_t model_read_action_helper(void * obj, int index) { + return model->switch_to_master(new ModelAction(ATOMIC_READ, orders[index], obj)); +} +:q! + +/** Performs a write action.*/ +void model_write_action(void * obj, memory_order ord, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val)); +} + +void model_write_action_helper(void * obj, int index, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[index], obj, val)); +} + +/** Performs an init action. */ +void model_init_action(void * obj, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val)); +} +// do not need a helper function + +/** + * Performs the read part of a RMW action. The next action must either be the + * write part of the RMW action or an explicit close out of the RMW action w/o + * a write. + */ +uint64_t model_rmwr_action(void *obj, memory_order ord) { + return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj)); +} + +uint64_t model_rmwr_action_helper(void *obj, int index) { + return model->switch_to_master(new ModelAction(ATOMIC_RMWR, orders[index], obj)); +} + +/** Performs the write part of a RMW action. */ +void model_rmw_action(void *obj, memory_order ord, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val)); +} + +void model_rmw_action_helper(void *obj, int index, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_RMW, orders[index], obj, val)); +} + +/** Closes out a RMW action without doing a write. */ +void model_rmwc_action(void *obj, memory_order ord) { + model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj)); +} + +void model_rmwc_action_helper(void *obj, int index) { + model->switch_to_master(new ModelAction(ATOMIC_RMWC, orders[index], obj)); +} + +/** Issues a fence operation. */ +void model_fence_action(memory_order ord) { + model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION)); +} + +void model_fence_action_helper(int index) { + model->switch_to_master(new ModelAction(ATOMIC_FENCE, orders[index], FENCE_LOCATION)); +} diff --git a/#main.cc# b/#main.cc# new file mode 100644 index 00000000..d4ab75bf --- /dev/null +++ b/#main.cc# @@ -0,0 +1,288 @@ +/** @file main.cc + * @brief Entry point for the model checker. + */ + +#include +#include +#include + +#include "common.h" +#include "output.h" + +#include "datarace.h" + +/* global "model" object */ +#include "model.h" +#include "params.h" +#include "snapshot-interface.h" + +static void param_defaults(struct model_params *params) +{ + params->maxreads = 0; + params->maxfuturedelay = 6; + params->fairwindow = 0; + params->yieldon = false; + params->yieldblock = false; + params->enabledcount = 1; + params->bound = 0; + params->maxfuturevalues = 0; + params->expireslop = 4; + params->verbose = !!DBG_ENABLED(); + params->uninitvalue = 0; + params->maxexecutions = 0; +} + +static void print_usage(const char *program_name, struct model_params *params) +{ + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); + /* Reset defaults before printing */ + param_defaults(params); + + model_print( +"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" +"Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n" +"\n" +"MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n" +"provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n" +"\n" +"Model-checker options:\n" +"-h, --help Display this help message and exit\n" +"-m, --liveness=NUM Maximum times a thread can read from the same write\n" +" while other writes exist.\n" +" Default: %d\n" +"-M, --maxfv=NUM Maximum number of future values that can be sent to\n" +" the same read.\n" +" Default: %d\n" +"-s, --maxfvdelay=NUM Maximum actions that the model checker will wait for\n" +" a write from the future past the expected number\n" +" of actions.\n" +" Default: %d\n" +"-S, --fvslop=NUM Future value expiration sloppiness.\n" +" Default: %u\n" +"-y, --yield Enable CHESS-like yield-based fairness support\n" +" (requires thrd_yield() in test program).\n" +" Default: %s\n" +"-Y, --yieldblock Prohibit an execution from running a yield.\n" +" Default: %s\n" +"-f, --fairness=WINDOW Specify a fairness window in which actions that are\n" +" enabled sufficiently many times should receive\n" +" priority for execution (not recommended).\n" +" Default: %d\n" +"-e, --enabled=COUNT Enabled count.\n" +" Default: %d\n" +"-b, --bound=MAX Upper length bound.\n" +" Default: %d\n" +"-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n" +" 0 is quiet; 1 shows valid executions; 2 is noisy;\n" +" 3 is noisier.\n" +" Default: %d\n" +"-u, --uninitialized=VALUE Return VALUE any load which may read from an\n" +" uninitialized atomic.\n" +" Default: %u\n" +"-t, --analysis=NAME Use Analysis Plugin.\n" +"-o, --options=NAME Option for previous analysis plugin. \n" +"-x, --maxexec=NUM Maximum number of executions.\n" +" Default: %u\n" +" -o help for a list of options\n" +" -- Program arguments follow.\n\n", + program_name, + params->maxreads, + params->maxfuturevalues, + params->maxfuturedelay, + params->expireslop, + params->yieldon ? "enabled" : "disabled", + params->yieldblock ? "enabled" : "disabled", + params->fairwindow, + params->enabledcount, + params->bound, + params->verbose, + params->uninitvalue, + params->maxexecutions); + model_print("Analysis plugins:\n"); + for(unsigned int i=0;isize();i++) { + TraceAnalysis * analysis=(*registeredanalysis)[i]; + model_print("%s\n", analysis->name()); + } + exit(EXIT_SUCCESS); +} + +bool install_plugin(char * name) { + ModelVector * registeredanalysis=getRegisteredTraceAnalysis(); + ModelVector * installedanalysis=getInstalledTraceAnalysis(); + + for(unsigned int i=0;isize();i++) { + TraceAnalysis * analysis=(*registeredanalysis)[i]; + if (strcmp(name, analysis->name())==0) { + installedanalysis->push_back(analysis); + return false; + } + } + model_print("Analysis %s Not Found\n", name); + return true; +} + +static void parse_options(struct model_params *params, int argc, char **argv) +{ + const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:x:v::"; + const struct option longopts[] = { + {"help", no_argument, NULL, 'h'}, + {"liveness", required_argument, NULL, 'm'}, + {"maxfv", required_argument, NULL, 'M'}, + {"maxfvdelay", required_argument, NULL, 's'}, + {"fvslop", required_argument, NULL, 'S'}, + {"fairness", required_argument, NULL, 'f'}, + {"yield", no_argument, NULL, 'y'}, + {"yieldblock", no_argument, NULL, 'Y'}, + {"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'}, + {"maxexecutions", required_argument, NULL, 'x'}, + {0, 0, 0, 0} /* Terminator */ + }; + int opt, longindex; + bool error = false; + while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) { + switch (opt) { + case 'h': + print_usage(argv[0], params); + break; + case 'x': + params->maxexecutions = atoi(optarg); + break; + case 's': + params->maxfuturedelay = atoi(optarg); + break; + case 'S': + params->expireslop = atoi(optarg); + break; + case 'f': + params->fairwindow = atoi(optarg); + break; + case 'e': + params->enabledcount = atoi(optarg); + break; + case 'b': + params->bound = atoi(optarg); + break; + case 'm': + params->maxreads = atoi(optarg); + break; + case 'M': + params->maxfuturevalues = atoi(optarg); + break; + case 'v': + params->verbose = optarg ? atoi(optarg) : 1; + break; + case 'u': + params->uninitvalue = atoi(optarg); + break; + case 'y': + params->yieldon = true; + break; + case 't': + if (install_plugin(optarg)) + error = true; + break; + case 'o': + { + ModelVector * analyses = getInstalledTraceAnalysis(); + if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg)) + error = true; + } + break; + case 'Y': + params->yieldblock = true; + break; + default: /* '?' */ + error = true; + break; + } + } + + /* Pass remaining arguments to user program */ + params->argc = argc - (optind - 1); + params->argv = argv + (optind - 1); + + /* Reset program name */ + params->argv[0] = argv[0]; + + /* Reset (global) optind for potential use by user program */ + optind = 1; + + if (error) + print_usage(argv[0], params); +} + +int main_argc; +char **main_argv; + +static void install_trace_analyses(ModelExecution *execution) +{ + ModelVector * installedanalysis=getInstalledTraceAnalysis(); + for(unsigned int i=0;isize();i++) { + TraceAnalysis * ta=(*installedanalysis)[i]; + ta->setExecution(execution); + model->add_trace_analysis(ta); + /** Call the installation event for each installed plugin */ + ta->actionAtInstallation(); + } +} + +/** The model_main function contains the main model checking loop. */ +static void model_main() +{ + struct model_params params; + + param_defaults(¶ms); + register_plugins(); + + parse_options(¶ms, main_argc, main_argv); + + //Initialize race detector + initRaceDetector(); + + snapshot_stack_init(); + + model = new ModelChecker(params); // L: Model thread is created +// install_trace_analyses(model->get_execution()); L: disable plugin + + snapshot_record(0); + model->run(); + delete model; + + DEBUG("Exiting\n"); +} + +/** + * Main function. Just initializes snapshotting library and the + * snapshotting library calls the model_main function. + */ +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(); + + /* Let's jump in quickly and start running stuff */ + snapshot_system_init(10000, 1024, 1024, 4000, &model_main); +} diff --git a/Makefile b/Makefile index cf4a493b..3c512854 100644 --- a/Makefile +++ b/Makefile @@ -62,8 +62,7 @@ tags: ctags -R PHONY += tests -tests: $(LIB_SO) - $(MAKE) -C $(TESTS_DIR) +tests: $(LIB_SO) # $(MAKE) -C $(TESTS_DIR) BENCH_DIR := benchmarks diff --git a/action.cc b/action.cc index d4c6253c..c913b74c 100644 --- a/action.cc +++ b/action.cc @@ -482,13 +482,23 @@ Node * ModelAction::get_node() const void ModelAction::set_read_from(const ModelAction *act) { ASSERT(act); + reads_from = act; reads_from_promise = NULL; - if (act->is_uninitialized()) - model->assert_bug("May read from uninitialized atomic:\n" + + if (act->is_uninitialized()) { // WL + uint64_t val = *((uint64_t *) location); + ModelAction * act_initialized = (ModelAction *)act; + act_initialized->set_value(val); + reads_from = (const ModelAction *)act_initialized; + +// disabled by WL, because LLVM IR is unable to detect atomic init +/* model->assert_bug("May read from uninitialized atomic:\n" " action %d, thread %d, location %p (%s, %s)", seq_number, id_to_int(tid), location, get_type_str(), get_mo_str()); +*/ + } } /** diff --git a/action.h b/action.h index c8ad85bc..d1f4fffd 100644 --- a/action.h +++ b/action.h @@ -23,6 +23,7 @@ namespace std { using std::memory_order; using std::memory_order_relaxed; +using std::memory_order_consume; using std::memory_order_acquire; using std::memory_order_release; using std::memory_order_acq_rel; @@ -185,6 +186,11 @@ public: bool may_read_from(const ModelAction *write) const; bool may_read_from(const Promise *promise) const; MEMALLOC + +// Added by WL + void set_value(uint64_t val) { + value = val; + } private: const char * get_type_str() const; diff --git a/cmodelint.cc b/cmodelint.cc index 16325811..15d6151b 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -1,8 +1,14 @@ +#include #include "model.h" #include "action.h" #include "cmodelint.h" #include "threads-model.h" +memory_order orders[6] = { + memory_order_relaxed, memory_order_consume, memory_order_acquire, + memory_order_release, memory_order_acq_rel, memory_order_seq_cst +}; + /** Performs a read action.*/ uint64_t model_read_action(void * obj, memory_order ord) { return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj)); @@ -41,3 +47,222 @@ void model_rmwc_action(void *obj, memory_order ord) { void model_fence_action(memory_order ord) { model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION)); } + +// --------------------- helper functions -------------------------------- +uint64_t model_rmwr_action_helper(void *obj, int atomic_index) { + return model->switch_to_master(new ModelAction(ATOMIC_RMWR, orders[atomic_index], obj)); +} + +void model_rmw_action_helper(void *obj, int atomic_index, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_RMW, orders[atomic_index], obj, val)); +} + +void model_rmwc_action_helper(void *obj, int atomic_index) { + model->switch_to_master(new ModelAction(ATOMIC_RMWC, orders[atomic_index], obj)); +} + +void model_fence_action_helper(int atomic_index) { + model->switch_to_master(new ModelAction(ATOMIC_FENCE, orders[atomic_index], FENCE_LOCATION)); +} + +// cds atomic loads +uint8_t cds_atomic_load8(void * obj, int atomic_index) { + return (uint8_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) ); +} +uint16_t cds_atomic_load16(void * obj, int atomic_index) { + return (uint16_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) ); +} +uint32_t cds_atomic_load32(void * obj, int atomic_index) { + return (uint32_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) ); +} +uint64_t cds_atomic_load64(void * obj, int atomic_index) { + return model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)); +} + +// cds atomic stores +void cds_atomic_store8(void * obj, int atomic_index, uint8_t val) { + model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val)); +} +void cds_atomic_store16(void * obj, int atomic_index, uint16_t val) { + model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val)); +} +void cds_atomic_store32(void * obj, int atomic_index, uint32_t val) { + model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val)); +} +void cds_atomic_store64(void * obj, int atomic_index, uint64_t val) { + model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, val)); +} + +/* +#define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val ) \ +({ \ + uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index); \ + uint##size##_t _copy = _old; \ + _copy __op__ ( uint##size##_t ) _val; \ + model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy); \ + return _old; \ +})*/ + +#define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val ) \ +({ \ + uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index); \ + uint##size##_t _copy = _old; \ + uint##size##_t _val = val; \ + _copy __op__ _val; \ + model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy); \ + return _old; \ +}) + +// cds atomic exchange +uint8_t cds_atomic_exchange8(void* addr, int atomic_index, uint8_t val) { + _ATOMIC_RMW_( = , 8, addr, atomic_index, val); +} +uint16_t cds_atomic_exchange16(void* addr, int atomic_index, uint16_t val) { + _ATOMIC_RMW_( = , 16, addr, atomic_index, val); +} +uint32_t cds_atomic_exchange32(void* addr, int atomic_index, uint32_t val) { + _ATOMIC_RMW_( = , 32, addr, atomic_index, val); +} +uint64_t cds_atomic_exchange64(void* addr, int atomic_index, uint64_t val) { + _ATOMIC_RMW_( = , 64, addr, atomic_index, val); +} + +// cds atomic fetch add +uint8_t cds_atomic_fetch_add8(void* addr, int atomic_index, uint8_t val) { + _ATOMIC_RMW_( += , 8, addr, atomic_index, val); +} +uint16_t cds_atomic_fetch_add16(void* addr, int atomic_index, uint16_t val) { + _ATOMIC_RMW_( += , 16, addr, atomic_index, val); +} +uint32_t cds_atomic_fetch_add32(void* addr, int atomic_index, uint32_t val) { + _ATOMIC_RMW_( += , 32, addr, atomic_index, val); +} +uint64_t cds_atomic_fetch_add64(void* addr, int atomic_index, uint64_t val) { + _ATOMIC_RMW_( += , 64, addr, atomic_index, val); +} + +// cds atomic fetch sub +uint8_t cds_atomic_fetch_sub8(void* addr, int atomic_index, uint8_t val) { + _ATOMIC_RMW_( -= , 8, addr, atomic_index, val); +} +uint16_t cds_atomic_fetch_sub16(void* addr, int atomic_index, uint16_t val) { + _ATOMIC_RMW_( -= , 16, addr, atomic_index, val); +} +uint32_t cds_atomic_fetch_sub32(void* addr, int atomic_index, uint32_t val) { + _ATOMIC_RMW_( -= , 32, addr, atomic_index, val); +} +uint64_t cds_atomic_fetch_sub64(void* addr, int atomic_index, uint64_t val) { + _ATOMIC_RMW_( -= , 64, addr, atomic_index, val); +} + +// cds atomic fetch and +uint8_t cds_atomic_fetch_and8(void* addr, int atomic_index, uint8_t val) { + _ATOMIC_RMW_( &= , 8, addr, atomic_index, val); +} +uint16_t cds_atomic_fetch_and16(void* addr, int atomic_index, uint16_t val) { + _ATOMIC_RMW_( &= , 16, addr, atomic_index, val); +} +uint32_t cds_atomic_fetch_and32(void* addr, int atomic_index, uint32_t val) { + _ATOMIC_RMW_( &= , 32, addr, atomic_index, val); +} +uint64_t cds_atomic_fetch_and64(void* addr, int atomic_index, uint64_t val) { + _ATOMIC_RMW_( &= , 64, addr, atomic_index, val); +} + +// cds atomic fetch or +uint8_t cds_atomic_fetch_or8(void* addr, int atomic_index, uint8_t val) { + _ATOMIC_RMW_( |= , 8, addr, atomic_index, val); +} +uint16_t cds_atomic_fetch_or16(void* addr, int atomic_index, uint16_t val) { + _ATOMIC_RMW_( |= , 16, addr, atomic_index, val); +} +uint32_t cds_atomic_fetch_or32(void* addr, int atomic_index, uint32_t val) { + _ATOMIC_RMW_( |= , 32, addr, atomic_index, val); +} +uint64_t cds_atomic_fetch_or64(void* addr, int atomic_index, uint64_t val) { + _ATOMIC_RMW_( |= , 64, addr, atomic_index, val); +} + +// cds atomic fetch xor +uint8_t cds_atomic_fetch_xor8(void* addr, int atomic_index, uint8_t val) { + _ATOMIC_RMW_( ^= , 8, addr, atomic_index, val); +} +uint16_t cds_atomic_fetch_xor16(void* addr, int atomic_index, uint16_t val) { + _ATOMIC_RMW_( ^= , 16, addr, atomic_index, val); +} +uint32_t cds_atomic_fetch_xor32(void* addr, int atomic_index, uint32_t val) { + _ATOMIC_RMW_( ^= , 32, addr, atomic_index, val); +} +uint64_t cds_atomic_fetch_xor64(void* addr, int atomic_index, uint64_t val) { + _ATOMIC_RMW_( ^= , 64, addr, atomic_index, val); +} + +// cds atomic compare and exchange +// In order to accomodate the LLVM PASS, the return values are not true or false. + +#define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_ +#define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index) \ +({ \ + uint##size##_t _desired = desired; \ + uint##size##_t _expected = expected; \ + uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index); \ + if (_old == _expected ) { \ + model_rmw_action_helper(addr, atomic_index, (uint64_t) _desired ); return _expected; } \ + else { \ + model_rmwc_action_helper(addr, atomic_index); _expected = _old; return _old; } \ +}) + +// expected is supposed to be a pointer to an address, but the CmpOperand +// extracted from LLVM IR is an integer type. + +uint8_t cds_atomic_compare_exchange8(void* addr, uint8_t expected, + uint8_t desired, int atomic_index_succ, int atomic_index_fail ) { + _ATOMIC_CMPSWP_(8, addr, expected, desired, atomic_index_succ ); +} +uint16_t cds_atomic_compare_exchange16(void* addr, uint16_t expected, + uint16_t desired, int atomic_index_succ, int atomic_index_fail ) { + _ATOMIC_CMPSWP_(16, addr, expected, desired, atomic_index_succ ); +} +uint32_t cds_atomic_compare_exchange32(void* addr, uint32_t expected, + uint32_t desired, int atomic_index_succ, int atomic_index_fail ) { + _ATOMIC_CMPSWP_(32, addr, expected, desired, atomic_index_succ ); +} +uint64_t cds_atomic_compare_exchange64(void* addr, uint64_t expected, + uint64_t desired, int atomic_index_succ, int atomic_index_fail ) { + _ATOMIC_CMPSWP_(64, addr, expected, desired, atomic_index_succ ); +} + +// cds atomic thread fence + +void cds_atomic_thread_fence(int atomic_index) { + model->switch_to_master(new ModelAction(ATOMIC_FENCE, orders[atomic_index], FENCE_LOCATION)); +} + +/* +#define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ ) \ + ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \ + __typeof__(__e__) __q__ = (__e__); \ + __typeof__(__m__) __v__ = (__m__); \ + bool __r__; \ + __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \ + if (__t__ == * __q__ ) { \ + model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \ + else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \ + __r__; }) + +#define _ATOMIC_FENCE_( __x__ ) \ + ({ model_fence_action(__x__);}) +*/ + +/* + +#define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \ + ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \ + __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \ + __typeof__(__m__) __v__ = (__m__); \ + __typeof__((__a__)->__f__) __copy__= __old__; \ + __copy__ __o__ __v__; \ + model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); \ + __old__ = __old__; Silence clang (-Wunused-value) \ + }) +*/ diff --git a/execution.cc b/execution.cc index 0fcf4e8d..869833c2 100644 --- a/execution.cc +++ b/execution.cc @@ -1132,6 +1132,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * * @return True if this read established synchronization */ + bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf) { ASSERT(rf); diff --git a/include/cmodelint.h b/include/cmodelint.h index 24c5f6fb..1c456b89 100644 --- a/include/cmodelint.h +++ b/include/cmodelint.h @@ -20,6 +20,68 @@ void model_rmw_action(void *obj, memory_order ord, uint64_t val); void model_rmwc_action(void *obj, memory_order ord); void model_fence_action(memory_order ord); +// void model_init_action_helper(void * obj, uint64_t val); +uint64_t model_rmwr_action_helper(void *obj, int atomic_index); +void model_rmw_action_helper(void *obj, int atomic_index, uint64_t val); +void model_rmwc_action_helper(void *obj, int atomic_index); +void model_fence_action_helper(int atomic_index); + +// WL +uint8_t cds_atomic_load8(void * obj, int atomic_index); +uint16_t cds_atomic_load16(void * obj, int atomic_index); +uint32_t cds_atomic_load32(void * obj, int atomic_index); +uint64_t cds_atomic_load64(void * obj, int atomic_index); + +void cds_atomic_store8(void * obj, int atomic_index, uint8_t val); +void cds_atomic_store16(void * obj, int atomic_index, uint16_t val); +void cds_atomic_store32(void * obj, int atomic_index, uint32_t val); +void cds_atomic_store64(void * obj, int atomic_index, uint64_t val); + + +// cds atomic exchange +uint8_t cds_atomic_exchange8(void* addr, int atomic_index, uint8_t val); +uint16_t cds_atomic_exchange16(void* addr, int atomic_index, uint16_t val); +uint32_t cds_atomic_exchange32(void* addr, int atomic_index, uint32_t val); +uint64_t cds_atomic_exchange64(void* addr, int atomic_index, uint64_t val); +// cds atomic fetch add +uint8_t cds_atomic_fetch_add8(void* addr, int atomic_index, uint8_t val); +uint16_t cds_atomic_fetch_add16(void* addr, int atomic_index, uint16_t val); +uint32_t cds_atomic_fetch_add32(void* addr, int atomic_index, uint32_t val); +uint64_t cds_atomic_fetch_add64(void* addr, int atomic_index, uint64_t val); +// cds atomic fetch sub +uint8_t cds_atomic_fetch_sub8(void* addr, int atomic_index, uint8_t val); +uint16_t cds_atomic_fetch_sub16(void* addr, int atomic_index, uint16_t val); +uint32_t cds_atomic_fetch_sub32(void* addr, int atomic_index, uint32_t val); +uint64_t cds_atomic_fetch_sub64(void* addr, int atomic_index, uint64_t val); +// cds atomic fetch and +uint8_t cds_atomic_fetch_and8(void* addr, int atomic_index, uint8_t val); +uint16_t cds_atomic_fetch_and16(void* addr, int atomic_index, uint16_t val); +uint32_t cds_atomic_fetch_and32(void* addr, int atomic_index, uint32_t val); +uint64_t cds_atomic_fetch_and64(void* addr, int atomic_index, uint64_t val); +// cds atomic fetch or +uint8_t cds_atomic_fetch_or8(void* addr, int atomic_index, uint8_t val); +uint16_t cds_atomic_fetch_or16(void* addr, int atomic_index, uint16_t val); +uint32_t cds_atomic_fetch_or32(void* addr, int atomic_index, uint32_t val); +uint64_t cds_atomic_fetch_or64(void* addr, int atomic_index, uint64_t val); +// cds atomic fetch xor +uint8_t cds_atomic_fetch_xor8(void* addr, int atomic_index, uint8_t val); +uint16_t cds_atomic_fetch_xor16(void* addr, int atomic_index, uint16_t val); +uint32_t cds_atomic_fetch_xor32(void* addr, int atomic_index, uint32_t val); +uint64_t cds_atomic_fetch_xor64(void* addr, int atomic_index, uint64_t val); + +// cds atomic compare and exchange (strong) + +uint8_t cds_atomic_compare_exchange8(void* addr, uint8_t expected, + uint8_t desire, int atomic_index_succ, int atomic_index_fail ); +uint16_t cds_atomic_compare_exchange16(void* addr, uint16_t expected, + uint16_t desire, int atomic_index_succ, int atomic_index_fail ); +uint32_t cds_atomic_compare_exchange32(void* addr, uint32_t expected, + uint32_t desire, int atomic_index_succ, int atomic_index_fail ); +uint64_t cds_atomic_compare_exchange64(void* addr, uint64_t expected, + uint64_t desire, int atomic_index_succ, int atomic_index_fail ); + +// cds atomic thread fence +void cds_atomic_thread_fence(int atomic_index); #if __cplusplus } diff --git a/include/impatomic.h b/include/impatomic.h index b4273eee..100ad0d6 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -1,3 +1,4 @@ +#include /** * @file impatomic.h * @brief Common header for C11/C++11 atomics @@ -118,7 +119,7 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile __typeof__(__m__) __v__ = (__m__); \ bool __r__; \ __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \ - if (__t__ == * __q__ ) { \ + if (__t__ == * __q__ ) {; \ model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \ else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \ __r__; }) diff --git a/include/librace.h b/include/librace.h index cabf0661..83e05d92 100644 --- a/include/librace.h +++ b/include/librace.h @@ -21,6 +21,16 @@ extern "C" { uint32_t load_32(const void *addr); uint64_t load_64(const void *addr); + void cds_store8(void *addr); + void cds_store16(void *addr); + void cds_store32(void *addr); + void cds_store64(void *addr); + + void cds_load8(const void *addr); + void cds_load16(const void *addr); + void cds_load32(const void *addr); + void cds_load64(const void *addr); + #ifdef __cplusplus } #endif diff --git a/include/memoryorder.h b/include/memoryorder.h index ba0dafd6..704d15e7 100644 --- a/include/memoryorder.h +++ b/include/memoryorder.h @@ -14,8 +14,8 @@ namespace std { typedef enum memory_order { - memory_order_relaxed, memory_order_acquire, memory_order_release, - memory_order_acq_rel, memory_order_seq_cst + memory_order_relaxed, memory_order_consume, memory_order_acquire, + memory_order_release, memory_order_acq_rel, memory_order_seq_cst } memory_order; diff --git a/include/stdatomic.h b/include/stdatomic2.h similarity index 100% rename from include/stdatomic.h rename to include/stdatomic2.h diff --git a/librace.cc b/librace.cc index 2c36054b..5dafc6ff 100644 --- a/librace.cc +++ b/librace.cc @@ -92,3 +92,52 @@ uint64_t load_64(const void *addr) raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 7)); return *((uint64_t *)addr); } + +// helper functions used by CdsPass +// The CdsPass implementation does not replace normal load/stores with cds load/stores, +// but inserts cds load/stores to check dataraces. Thus, the cds load/stores do not +// return anything. + +void cds_store8(void *addr) +{ + DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val); + thread_id_t tid = thread_current()->get_id(); + raceCheckWrite(tid, addr); +} + +void cds_store16(void *addr) +{ + DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val); + thread_id_t tid = thread_current()->get_id(); + raceCheckWrite(tid, addr); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1)); +} + +void cds_store32(void *addr) +{ + DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val); + thread_id_t tid = thread_current()->get_id(); + raceCheckWrite(tid, addr); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 2)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 3)); +} + +void cds_store64(void *addr) +{ + DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val); + thread_id_t tid = thread_current()->get_id(); + raceCheckWrite(tid, addr); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 2)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 3)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 4)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 5)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 6)); + raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 7)); +} + +void cds_load8(const void *addr) { load_8(addr); } +void cds_load16(const void *addr) { load_16(addr); } +void cds_load32(const void *addr) { load_32(addr); } +void cds_load64(const void *addr) { load_64(addr); } \ No newline at end of file diff --git a/model.cc b/model.cc index bfb6d22f..ccc109a7 100644 --- a/model.cc +++ b/model.cc @@ -512,11 +512,14 @@ void ModelChecker::run() if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ){ if (act->is_write()){ std::memory_order order = act->get_mo(); - if (order == std::memory_order_relaxed || order == std::memory_order_release) { + if (order == std::memory_order_relaxed || \ + order == std::memory_order_release) { t = th; break; } - } else if (act->get_type() == THREAD_CREATE || act->get_type() == THREAD_START || act->get_type() == THREAD_FINISH) { + } else if (act->get_type() == THREAD_CREATE || \ + act->get_type() == THREAD_START || \ + act->get_type() == THREAD_FINISH) { t = th; break; } @@ -539,7 +542,7 @@ void ModelChecker::run() has_next = next_execution(); i++; - } while (i<250); // while (has_next); + } while (i<100); // while (has_next); execution->fixup_release_sequences(); diff --git a/snapshot.cc b/snapshot.cc index 66faacd8..7deaeff4 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -110,7 +110,7 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused) model_print("For debugging, place breakpoint at: %s:%d\n", __FILE__, __LINE__); // print_trace(); // Trace printing may cause dynamic memory allocation - exit(EXIT_FAILURE); + exit(EXIT_FAILURE); } void* addr = ReturnPageAlignedAddress(si->si_addr); diff --git a/test/memo/double-read-fv b/test/memo/double-read-fv new file mode 100755 index 0000000000000000000000000000000000000000..eb48204d10241050447205de8bea491e8e2a8714 GIT binary patch literal 8992 zcmeHMZ)_aJ6`#BFpR)t!3nX9?)U0UIIutKwZWZ9hbn+9J_P>7Nhomp1JOoHQs7sFe&YC~Em&T0rMuihRW@p|#5$fr3yIhQln|+NTr&KE(vYw0$ZRV`N+E@)! z*cNsxs{*7F{uM4kYSoCY3D-ouLeB%V0{+|F7SQHac!lV#77Q&|g(5_X?d6Lisuo>d zXR$;XlQ@8O7%TH}7U+;w5p+nzF)1k7A&YkP!meKE6I~R65vBfN-|)X*`0IBoz#*?7 zVV(S$r>Ki%-&>}R^~qY!0#$g0XgRwFz>fFNGW*o0Uug7+_R5V5qwx?_beG*3jSRQ8 z+!@syqmfwZaO2^&*2dNrIT@FmdB4#=>h9_t;4RTOO2A?NHo!m50hGTK`S91%SC(Ih z?CyH~&zspVYhLW=MH#+IdT%GrOD=DPvK=ve73<;u()jjsfB5J3AMXggx_tTD58nFl z6F++V_b1=?z4Mp%=q-a*VL1=%4TTWrzE=jn9&m|k6h3fXmclOqUdsPdW$-{5KRspe zLuLH@v3e*^Tjz1ZD7pR|YVw3(Mfmq~k9KVGPIq)|)zNrX*1aR!HB=!ra z@-hj}8{iF|s!}XKJb%OSI<`T~>zokg(?nc1qA-P+rj1R+V_MP-CrnLa+U`SIpD`9m znnt1{8crsSB-6V4_h`D25ODvVj%Yk)^oNI|h9xU0NhOVhHW7}*m==jeOlFQJbZsPI zgiXV$KO6_yh@RBKW_%(t0wKf`#$C;JC>jszfM}!OfkD(GIO$v2WFitXMmGayu_U+`YAl(IYeK$P9q56`+S3e=DvN8!?97Rt8W z$YU3m7C7IIJa%pA9Ov&w9*1UWmh;WX=<->KyAeJ zrB1K;)bv}2HlIaT*xmJmb129zg7Pu$fA9kKa#SY%d6W;R-~AVNaQ>PH9H{9P^?c@j z)pb#Q`I@;g=WQK%tJ}f`FIep#y)Odsv()+lFwDdtu)&L!2LN(?$XlB8!v{{CzMrKk z-}wR9<($2b2HAzdrN_V~9}lAN&Xn|#kJWT)WxisY4gq3;>bR(?b6a6hu*|Z|?rYg> z(~Ies)RRXt>hmjNUrL8w&rIeei|X_HU;weCLzgoLK%&kZ$)rPn&1|yji|Nop#)tK} zkZ_(3{R#YE`GorqT}oeqd80tbbAt!{5%Ee*t7`hlnmR|(W<1#VYC5zs6Iw}!uG%C^ z;4mG^%!Hu%<(bsgnSo_>?qI${Q(XQgG$svR5dQs^|M}3>uRs@O2EZQ;Mh5kpR_8-2 zw{y{ot*L_`0zZCy>(=`Zem!^~n9c?Vg8e-wxAj&?(1VkWNcVTASG&`%_H4)T_p0YV z@nq&c2J6&V6Fg)$ysl1PaH%`rNnODO_0VAOTfxEL!Ju~GRDOs) zgmuRKi6!TPy=4z#Dt{T-AQW@!LEOK5=}hl-6f#D=47;nUAvBqp0ljclqjf*R6Zhdz9V3 z>7Lu~+IkzpsDp9)A;#wr2>SfT-5u9gxqkvJTXG%XXF)zxAb%()KL+?BzTpCS2bZJo zpTWN$`fQ-Q-RFPC-R`S@+7t3gCo9^04Nq07zQFM+)z>y%y~n2{d~HErAn0po_er1! z`t3e1KUXb-c^mk#@8{_9^YZx!I7h%Q_TLrwPT32c5u6my9$2okNbY=x=VUB&uDiuz zbN4K|KEhJrWs{&@_}pN@^@WAx|Gt)uBY)bhAYqmK$=Hbsh1clpaoKJ0wH#&anxN|h ztrv8ophWNhz>D}q(ONkpVA?NmpTcspMOda%;Wfe+1W$2OdvpdO9+o5T&#cggt&HwU2J58-}pha#9Y_|kbbD*g;&>GmuMxtT(z#K9X$w)jVwaEcFAT^kYRO}Jy zu9nuFJ9loE8lurd6L;FMw(ZnpS?Yn4Z<|{wl6&AA*IyF%Fta3Hk(-xxXC9cPmrLqb z<>qanel;ugzCExCXr2`6*D#uIg?MdlUKZlT_b-%tVD-+5_gJWZJqwh0j~=*jD<$y~ z_c-p~&!k$#?wZ#;HCPd!N!Vl(m8*KdtvOi zKoO@?zAEr?<8v0|E|@2ob&Alm$VHA9j~hx$#q$a`E1rjMaX-cH{Ufe_W6^xOjt^k* zIBWsjRbsw<0Jy}8=T8IRrSe7ha@@!8Hi?D4Ppbl_^+;#jo-%$804{M4g%6_)-o^bC zuj?s}7y3Z%bQ!!IWa}ZnME9!-Vfw2w?al+f9#YPXI49o;5Il z>)pk9tz#lix}8zG8-@OZj`e;U;5Wd$b>`FV5IA1@u^9Zx*u5MVjE(dHj`=sd#@kCZ z?^khN?wee{IQ}mS|B_=LXytf`{eL83Ce767s5}BGsofoYT2J@>en_(Ab7`76p^acR z4YF*S9@oaA@!@b((;*cGd9l=CHWHthj2fn)%U|8Gv!%2WPmgKgL?S!|*)B6N#YPk1 z2}9FU6BAQlV&ix!u0U0fry!5lh!@Vr(L)gFFj#c;1^0xsP;Vz@1bO6Cha9pNQiX!r z*~he9J$u`OJ=)%`uKl5Ytv}e_6G9`*`Q;kY3jv;NWLoDpdV_nqJ48B9QS4bdk=q+d zrmW;2&mQuO;b%!$IunD1zDwjB|9gsaFXR&SNKAv2CiDcep(Qh(@CG6KDDsZ>bf>04 z&NMfidNQt!hhsWqPi;9;D`f01&z9O^q$FrTQj_O7nVg)OFvG(@&4fkAsRkKRBQeS3 zSll$^V0(9?86FedSS%$Ery}rsLPTdWa^vCTIFt3M82GcOnXn|{U|7ItAWIn0FdB&3 zWYlCb4_t<-JQfGmG!Da)r*7p$oCho$<6<_B>)?bq%hZ}JmIc)x9sxCICJYH;h#_vG zdq6PDD?^f($*@2sVA9*y_5WJO?>uY?x&6P*tpJz*-Hh%{9E1nz+RGP#!Mh4<2fWZZ zmwuO$1WttZKjNF9Vz;OBuqhmFB}GA<_ML#Q!rg}2KkZhy=4k;~T>gIN<5HIh5gZ-rd6TeHHiMu zVIQbgxMBb&B@~L+;)?kngTUTCotqS4{|XJPa6s*nKg{*n?J2*pK_ndLo=^JD{{KSQ zQ!{kFk%av|G8EKlkH42;`(#h|r%7So`6>2u4tu(1ofY;i=-gJEBp8pV9tpu*IoH_H+-V-}4tm|HX97^@rxc zX-E6?``Q|I3W~G8#1nlFbnNlx?v`X=lt_P@ECu9912SIQ3o!DliQ#Of2XIm?Wzxmjl;S}Iceei@9+i&> literal 0 HcmV?d00001 diff --git a/test/memo/fences b/test/memo/fences new file mode 100755 index 0000000000000000000000000000000000000000..3196361964c6638c9c1c4523165bead5448d1566 GIT binary patch literal 9040 zcmeHMZ)_aJ6`#BFzc|VH90-^MHCsqfg5>3#IIa^^*t31k8aW|#Y)D1T`s_RVE}ZYo z-CpWYQcN8pP9b2?eu$7tEzwHt7nG_9(SC>>1(5`y*0dnGlu9lXbPfT`zsPOD?t3%y z)_Z$*fGY8=W9`0qzxQX}%+AcsJUZDzr)F(P810zcP!@l9uE&X-7HQ%V>_SnJ-Pnf zeLs5sxo;nP<({J`!%s=y?a{M}tEx=fhFA?e>)^Q%-8TJ)x1W5lHTe4F+4~P(f9Rp7 z9{l~ukG${w%TE9(hOY%&aVi6k^RgH|2Y4|*kCnjvfGhAgOD6z| z69oP+JjML~q6Gfi68Ip;y=<~dgBoMc@Heb27h^uQfsOk5BqGSiKz!^v7IonN;`oLF z{64@j&M~=@^&MJ1VZBxMYTVhLu% z5;2pR(Nx$NNJTkUpE>dhb#ejmXHr&2H z`)#;=e`>bj5Rg?g8(wXpjOjL9ZjD^J--c5kQJ{}suF_AGuV1Aw{gG+2JckopAAhmx z95=IG%RAkmvb?1X-Zh&vs39Lk`TX26lr8_R0v?B8euncOBadC5pXU4}yXP{NM!eyfnPuk$v@EJ^PkE{?CQ| z-5uwrr>ixlpFg{wlk>Q~azkMF>0r$!_;Gk42?Nrj*W)_X#}~bN_MO8UUqDwl47I&e zC|I5YX%Cpi2B1l=tWlf507_UGjhfJ-eWv&E2lMUeaG(GS^$)R+G1yO|18v zXn*XxwGcnc)b@a3E&+k{zEr+csW8_kyrn50{DA7?x3f(7dp`v`%h^Y0usqW{{{Yym z#Dge&OD%i!b3L0`IA69U4gq3;>WHlBQ?J2jU^&flyO)-i8!l#F)=wVI>1Xz@5`t{- z&0OD#WKKUbV@YOn?I6)l9L;5eujQ&meJ&fE$t`^W_|#|8c{cb8_Kj$-vN*fUOthztWVXf7M+4~f$d(A{}*%hMhOB05=*^gu`UN=Nqf&TaTTtMs#9cyf1x zvHr;Wrqb{?ntz?yOP$#(ZQx<~>NoZAb1r??dznkPaPR32{2l9?cTaOYF7WSYK+~!;ntgX zY`y_KpihkZ*WeeoL>BP+j=NjeR=A&rmW4bFa5MDbXr6r3k{<*7R0%oy{v|w%AdjGZ zi`VyryTx1gxF_gUPL{QJw?0;`d;P~NbZ_%`FJXPduI_u&fcpI>+HT84I1?t`n?v&!X!iOfg=mXoM*%B>->?tGJFf~T{@tXuGOR=7q6N@s*Ru*I@o5bKRU*u2P} z5SnAt5~g*A>l@3pg0Q*@jn@cglBc+-y;YxL<5x4aNU=&kCs;uQNw-J1-q3qe%w#pkffP$j6Zrt+~?T8Rf#+I z^)~K*B~IFZ4sg71JRgvL=yw8GUXH`t#R|X6uK+LBuOw`+7$=>_`Pl+=pM{6_OP~Qu78^IzC>GDl+_Z2W{+;_N{O+G{{i_P*TNxj~!g073a95G} zb_s9=@+i*vqX1qkuhYnJFT-0O7W$p~K;pC>Z{|`s+m-OM4{$~5*hy~*{5I~Va9!We zak~dmpD2O1fVdX&Np$-ulcvv!xgZ+=UkCHqnLpbsalD>miSRdLjU1PZjkE)f`8K?6+Y4?C z#qw}nCHx%XehT}wN$QU|_6?QeMSd3sQfAuB3=XOTkb=6Swae)2IM5Brww0WkVGbJu zm{o&pn-NYLL-AyPC~kxyB?kGi%qSa34v)kmW+beBXXmcQ;z~RnW`t6y&=JUPnW-ae zFclh(7~#zD@DVVvaXclLuZkJ9G(^}Bn(bYIy+I?muMIPTJYuRtZrKRxQbBL)V#c1% zJ6i&s#+~i$2ZG&3cc7&+h(?(6vl(g~uamHJCIIt&7s)w(d5ZH+$Qg!X2?J7^&=bst7R`9VmxC;$%rEkQWxCTaAZKa~ zXE>cSqM<|>vZuBjsR$YS%d@4n7-bUFp1ib4#hsiIq9V`9)bx>IGt>{%ObHsL8e~W# zsS&0ol4e8=v~<*)p&`i)B{FJ%CI&&vQ#7< zLIYVFiJMI29a5pH4kdv#Bct%-6Js_CnRUygCR9G;>un6qy|9`FHc>uOP>vw|Ax%7WFx@VDp)U}rzfx){CY!AH9 zd6@o>rAV9z?UTeeK*erP=Vntn+)Rp+I_=v4zXEq5YX6j5==Ah?zLAlHI$@4HRkbj94vvOb);E%?DniuLs(2IAXZ|W zgZLXM3eledYqzI+%mhwKC={>Y3i+Rdz-~V&+n<#7H&}@S;epyEf6qAVDIfBpOi;kh zEwA8M+ski&!S?C<(K%>F+7H>4q3*QD|M%JL>Ho&`|Kzr>u%B|+(|v4ACRFe|YA??5 zya+-sJk~JLeG5S-PJJi;I_T8EL-usPtNNPu{{UMIk?iRn<@=iU?}9B(RkEl1BK`k= zPWGSXH^oo$;FP0%`v2M@b_xpV3vPuc{6i4f{AXErDgeC@|%7{W;k)reiWRn0%DUqu}uJ6sx zyW8747gVW#wPWqRdB1t@&70Yoxp~hIhg!Bf9S%mt$!=xHwJnl4WWE_w)^Ju}^=vVd z**dnCRRB^BkIY+;nl+;H!ZcC0kaGbogQwnU0`*RrSBS1PVd%ju6QZ1{8tdmT<0IOJs{ ztckz#6lJlry{kvCe!P;iKxJMby3K?cQPR5;^!WHh`{xm#5ZEpHTWDSw&4-|3xa|7a zKu=xm^|45GY#@;tsvfGZtFEi{r<4B8eB5XsWq0iAA|d4A@B zJ!|iK_Gcz$GqG_`-Er3V$5%Qug0i0RQ0v zcmQw-9(!p4K(d3t?}evSzfq2RSesjh8e{GJ&DcCpA6w1(ecb{v$-5lChIQNU^BiAY zgx?Q1_8SoA1yp$%g!gjzf=4T46AHJj&8**-gtp#DS`F*T_&~23ONJvgbylP|86OO%G*uhw?GGpVG-y?$ zV2r^4dU5^NvBA_pLXW~I5E7#>JJlj#Jq!&!>9mP6RZB$Jj+W+zMs>4)vwsWD2W>fP z&B4q++z}3t!S_o*X&+}+4=hIc&(Hvrd2ctTcqZUpqOwYS*F^xJ9V(Iq&-c&RMhk8| zcLNsOdhXO)aO{JMY{A9R#+wui?j>QM%E)=QGFINXSYpb-NxgjbNe;g3K4}qxYIaKl zh-5c3!P~n|h8ptyC^UCA3uVJi$m3Awra8YEc^u;0BrnvK`*Rg6C?BY(Zn*3o==vb$1d%IOmq79%;0 z`(*Z8p!oNwcU=>l^L;P@ok}(CH)UkrqZse*U2_~w;jou=O<+UzEC@fs?RTBTQAYj5 zzliOf$~Qjb22NadfdR$1pq!Y!O>vx3Ucangm9w^lta;b5u9If}!?)ZG{!%C`gL_?Y)J;e#JMW#l%NDL?ll=;e%EM1|~h*W81kllKQv_;!JsN#iBsz^96l zxez^FwxI{SWDIK&UQ-Som{ndJ7l+d9cQ0qN%GiNfBXnkVC)8_RF+wxOlrr*i036K? z7Wzl~?a;v<#W(<#Lm%GkfH#~@VDUU)XT1}d^Ap(Jar|b0OdFZkj8n5NFzcO|p3vcQ z)LfEBFE)*ZUNbUNO~$FwsoCFr#vM2tZ5nI+Fxq6ap7B1nG8!~q_db_7(=ygM4TdIL zjNcoX7mT;YI$s!TodW$SBXk^vpXK@>eggEno{fg8{@{J;-fDLnrQgx`JN|b_MSZswWTUKiS8yU%5Syz^&_mGfEp8)OvL-BJB&O zr45mDpwmF>VTH~EJqA=3haTQPus9yv%^X8M$C{;!+=m^De2C+3dp+3NgaV?JmS=1| zw4?mcKeO3kl=b+wdsglAF4^ZEX1A@rdD9K+uR|DRV7s%kV7DECpvU*9v+;@w=Pu~k zv=aeX0-x*AM`{m^xLke*mq9hO@i;v7u$(mn8a%#lI~zQ!o^XXc(xI{j&&J2g6;I&N z3dK`DvZ&P~r#$sRPax>o*x->s4&)m=Zhrsz9jJGM9Xt&GU;Z~|KoUnVBPynW?gn=H zl4xHlDBbVyo{WX=b=R0|F3zIx5tceHs|9t7cnbFi7Ha?GayE(lQKyU~7xRslnLOP& zW}GHp2{Kp~3y1Nn#j?sI>?%Qt;1518{O2ft(>f+#+V6CSSt;-f}cJ^cvdPdsfuk{D2>oT0H`Fc&AKTzwh2~?R4(&j)-U7#+omG#EpW-aa2 zQt5$YLaO%%`~hjBp2{Tdmu{%7+q!jYm9#My+Z(^$g4I`9dM#ab!LLufQ!Z+B!EaJW zN!-Qsl6YBeU0RK~V3p34l&@g4ZVTlXu~OgL1-pRONum5=M(eE*uVl0?3-RLk3)@|6 zDVr4EvrzsDCYSh*E{M1(A5T@Cr0QuxYToMhE;;i)0cg+lxq)>aZPj*C&x#pu+_TfzNa#x7>_ zh*`t))B&fI-G4ksoiP8yw(o+L5udc-eu3N1^CoUT?@>dqEt1>=O#p7KGxTD0nS_I>jSn)cMK)zIdrk3L#hEXCGx{ED=%5uxT+r(Sp z{mv)`KVATD0JUY1Uor!~{J17TUMe=v&H%m) zvKe%4lnI%03&@wl{P;@D^Kw3K#T{G=_%dg4Uh5GMML*53H1FpoA-~7hU101+ZofF6 z78E#!`B*gmX6#PDG0%qKxwYT{P%8h{#pR3r+{Wz}=h<%Oc!_hqH>IcbOf>56g?!V_ z#@%X5b9)CQ)ABhpRgbH^m^FiJni@%}eX(RuIHpGQWD4?MnIVR$u9yaan*YWvTWd=T z@!XdhPNl;8A(f@4_Ooaz9M{xHCLZ4pDi)5X+zLcf@qL>IQ^`K=jk*Q60?+Ugy zH;NpcEL&4=B4O8?&X^fJo*m>F!7q@IEKV90<^KwMvnZ6xDgN91<{gkdj0_}H$Y;VZ zQM6>b6Fw{C8%3tkn(I_mNSNm4I+9MRkjsof>eP}THM5sE89Y^5n6%`1Oy*DTkL%$c zpnA%r{ZxYtsFoUJ{zOvO{K1CiYCYU1xV}Wj-;)`De;o`&m>;?RaJrxQBl{Cz&!l?F zY!P?B0!D?lloku4f~XC~bmr%7`l0IYO9HEFL-6LQS$`_Y9rkPeVnOytzzA`ss=07X z4XWSQ3u4es7;?ejLsCccfM6Ea4@q3+hff!Wb#L9;|4|)(&*7-co&R)CrT>pnd_=}k z)>^&<48|mI9PmQ-S^EEzByb{hz7k&p6{|kodv#%OJqZeG*KY#+62vgn|52yRC65Zg z?$eyGaWP;y-@Jr6iUGT=3j`ZoiJt`cfxX_d~ zZBQNQz3^a6M*4IwKT>W=(f9?M>xbm;2QiHCh^PBI&q6|*WSZgmDy#njW_aI1S4p4l z`7@$J8YlH{AO9mlzd;zJc;JFiI3{pp(Ux8R3Bb@VimNHEKPmu<*Fl6AF|EWh18P?N z$qJdbO$z;C&gEY|Q6>5m@K$|_Lu6c(P{?1CE9QRy4OV@MSK5UB@?5}gTA+T(-cM}$ zl*fRCBrg=tle~TWKNtG+{pcPuDD=0JqM&yDU)c01PNM$>${RQ>^1iI)V=~Eo!`-1xKfi5mJ(x-Tj z{%?O)j9)Cr+<0gm9JTdN|390@K|!&Pmw2KdfsEDvT>L0HXyaD$FVZ7AZ_}qZvrXue zpJajbh`$UK#Ay6<-|QBOc6nN-r0)Xf(f^`CBH2E*~@wI@Vk2D@S7jb`<>VHNg?jknh_Wu6``dFnu literal 0 HcmV?d00001 diff --git a/test/memo/script.sh b/test/memo/script.sh new file mode 100755 index 00000000..a97c7022 --- /dev/null +++ b/test/memo/script.sh @@ -0,0 +1,19 @@ +#!/bin/sh + +clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/userprog.c + +gcc -o userprog userprog.o -L/scratch/random-fuzzer -lmodel + +#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/double-read-fv.c + +#gcc -o double-read-fv double-read-fv.o -L/scratch/random-fuzzer -lmodel + +#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/rmw2prog.c + +#gcc -o rmw2prog rmw2prog.o -L/scratch/random-fuzzer -lmodel + +#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/fences.c + +#gcc -o fences fences.o -L/scratch/random-fuzzer -lmodel + +export LD_LIBRARY_PATH=/scratch/random-fuzzer diff --git a/test/memo/userprog b/test/memo/userprog new file mode 100755 index 0000000000000000000000000000000000000000..67443eaac35d2a1785c469d7dd721f14d1ddd973 GIT binary patch literal 9056 zcmeHNeQaCR6~DIg;ikn&N(9b1vph7q82-3HChx$hkN z`Q>?_N&92cZuNZb`JIn@?|Jv$ckfB>4|R9CT`s}JExsg>o2XPJWc~^SkZY!1((?cN)K(Glv$I8nAk7VYZDu8#DXo}!L1SEb>+K6C%zDlw{Ras$L%I;RMljAeZKJ&MRG2H$bM*pb0ZAY(ciQ}jMhvQoX56%IU|LDWzo9ouU{hjZ< z`h&;6^;^yN*3VzQ6=nD;`MrJfnBwx5shbe1hG!)_Gb5X(fBEOf?rjgfIY0Z=J?rnf z|GW48;_wH)v#-C;ZyB_T%d5bmt-U+~fD?WR;EG)tc$}9`_#1#b`8iSo50voJT>}3` z2|v%2z{g79LlXCi39kw@h^71$;_pCf#9A?4(@%&=-j(2x$L^sb)mdL)`6xMzENJei30ga_hLQ|2hiq@yW)G#pEa!AKhXCsWbu znuH!p#0+7Kq$2uYDjGJTX8o=t>4lBtXlyXAj-~{~li>(D7y=IhMlgsAqeYCRVhLji zhJg?bL$<0%BVi*9f`K$P55p6BG!YToy1Uxi^(KFle+vY}wiGEuE?6V@57&zM?>N+X zeP`CjmZ9ZE(!NmLFKf70;2PsnNAI-~0QAL0vEbZ3%IYn+bw3VRaO-~5YQdpH`J!5I z+VZ4Kv*63~+OR)ba2_LywS)6s?NIr~Ws1-qoHojHPfG9wF9yR>7PqVfmBo##;J12% z3N_?MP-E`YB9x6)$YTiRPDrGVDS_vKOp`09mi1*`I&zn z<-OY1|0*3EyXXN2T6RG@mb*!Fy{Nr*(O8}Lww%3HZxDUQ&Grx6cqQ~-WNLfCFqeRi z^}Sf`1IYD}Y-y?nKA76Un?$Dk?BigUclH4qES~I}+YdH{{vZnPQaus+1pAx4?}C=i zEND}4=q8rjGZz;ZPn2y${tDo=sWFy3YD$>brjA0$uskbrt3lTIQubx-@O?S$`Tk|5 zARBr+cSAvPN_&1fFPY6<2@>tleYtGtjoj%^W&Kn(bTaoltWW)#oM%I?fd8KX2L3}c z*%|HN3o1t0j5m!(X*{ptSPH#;9WBmhLkovO3)#@QL!ooo(EOp^dCO2IK;=;8oHq4` z!a%wK%Z75$h=Ps4tCR7{`_IQIUF`ovX#QFVg=~N$l-tY=oGvtQ_7h73LleO-2X6~z z7lXaQp6CFS1-TEdqCW@_J(V(yZS2hfjY3vMGpMVAQ1G`JmhY_ zq{4k1S~leofR8}``-WbKY&>5ls~5{OmY4khv#H0e12PFviW-!Ums!0%CeTI7d{VIaGqmf`NtO*lgJ-& zt4Q*9zR5C^=d;DE+vKZ22TK)on9mG#CM;GHWr81YS?KG*b9S0wUbnbcV7c5R!ds!r z8siJ)CeQum_Lh-8^RO)BcutZ&Y$uZE_%0CtG|9>QzfSlbYj3Cm&KX!PBYF+d7NVU* zZzDQHbT3h9Z28&N-hRDO-#d^=7#U@Yzu6yXXvs*f@oSAO{y?+8F|f%LC{2OJmOx8j zs~C)jVWZz0O{HVWgwpB{_ybD4k;)|QR<3Jq*}8S>CZ#?e-#fb5g0*h4wCY^-z^ra{ zt4o9)_}26|;vQi*;$`{yX?5m-**fc}UmzNH zzVyC@au3|F7ic~g>t7-cIJ`#>Bndb#RIKlCZAgkLWBUSzfL2w1(eKNRC@#2!a{={*?jJc4(> zf)`x(W#WUy0%F#1UvK>7puk}s{t-}@!+ZZ&>R-BKzE#KoE{($)z+DdWZ60t%ES*1B z0q&GHYLPgsJ6cElomya==EJqJe?oMY@Us(eg>$NCrjv`0ldZ`o__<}DV`n(V6A&;9_s<>C*O^@-D=YB zr}aYJ7wZ9E3G2e1Kf8u-h2B?`3|b`4)&;7Sz%g%(c{pCDY=NnIr~F($=wqA>>L>Sq zK>Ara-YcnH%qLh&K;jPHi@}tUHZns){y|7n-Q2!Q@9x^&14+0-u1z;a^+C+GK^9Jr zB=zBVav&VnBalsl#8_rr3?@g%;!z_S@qcm4)@ElVnKIMEsZ@9$WWbEnJ~5OEk4E)K zW^{BPm{>TOo-0ztG~QS$IShRq0Nu`A!R;YEw4(!ag|g3Fhpe+6(nvw;*d_FB-M6#_ zyY*W-J9meA^qyc_cL*DZF6ePb7_~ zKiJmQV1$Q>8%|{W1DP27Jt7tne&j~N=@H?N>`Q<@lNu>gLI=tsMh96c8V{oZ)yCq6 z@XKNNq3Rz_0&7Ia;a8@0{i&qvus=FNvvMQ?PM9-I&ADS*aQ&`9P=jW|kUWMyBn@;A z2xfr&kN_5bSSX_~`K{~nKds~W0JaSH#+rrCz5I7KzITyW>T(_F7vRCW4%_qjnE$S& zfXrHW-(jo~Dpq?wM;qkuYE~p_x99svyFO6vK1!3+VM2Ou}HuUto(g~w{o_mu^*&nM2wsK!R0u-Wsy<^WDg zDBNF@TgrbQ1lIN^DpjdELH6!^BEj^)?VFqsPeR3N&-sxjC}F{Q0@kN##jN-t+4K9G ztWu?HlI*+lnr6jr|6_o$eYWSnBlF*vJ3hmH%4W~^vj8qCD9z~HQta`331mKa@?qlp z7lKgi`gZ)qGC-cfl5?8r$>zk^euyDH=ab$NYGB z9vrc?&-cs=I4CIg@iNc!ebBM?KYt&k2KGoVg&($KdckJT_trgR&;4W%Y{&dXs36AU z=kw@D348ne^FZgZ{{ePLlP*e*Kw{2B@ls1kPY(PRAEB)}?x7yEA|98?l bz5;~!t>W?HUWNtNr&Ig&q!6