From 4d1d81928c3688fbcfb96ee68eab70e73f7771e5 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Thu, 12 Dec 2019 15:25:38 -0800 Subject: [PATCH] Get rid of uninitialized actions and just use non-atomic writes instead --- README.md | 11 ++------ action.cc | 28 +------------------- action.h | 11 +++----- datarace.cc | 4 +-- execution.cc | 75 ---------------------------------------------------- execution.h | 2 -- funcinst.cc | 2 +- main.cc | 11 +------- params.h | 1 - 9 files changed, 10 insertions(+), 135 deletions(-) diff --git a/README.md b/README.md index 8ae834c4..f2a6380a 100644 --- a/README.md +++ b/README.md @@ -55,12 +55,6 @@ Useful Options > Specify the number number of executions to run. -`-u num` - - > Value to provide to atomics loads from uninitialized memory locations. The - > default is 0, but this may cause some programs to throw exceptions - > (segfault) before the model checker prints a trace. - Benchmarks ------------------- @@ -179,9 +173,8 @@ summaries are based off of a few different properties of an execution, which we will break down here: * A _buggy_ execution is an execution in which C11Tester has found a real - bug: a data race, a deadlock, failure of a user-provided assertion, or an - uninitialized load, for instance. C11Tester will only report bugs in feasible - executions. + bug: a data race, a deadlock, or a failure of a user-provided assertion. + C11Tester will only report bugs in feasible executions. Other Notes and Pitfalls diff --git a/action.cc b/action.cc index ec7332dc..4c1630f4 100644 --- a/action.cc +++ b/action.cc @@ -36,7 +36,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, position(NULL), reads_from(NULL), last_fence_release(NULL), - uninitaction(NULL), cv(NULL), rf_cv(NULL), trace_ref(NULL), @@ -71,7 +70,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, position(NULL), time(_time), last_fence_release(NULL), - uninitaction(NULL), cv(NULL), rf_cv(NULL), trace_ref(NULL), @@ -105,7 +103,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, position(NULL), reads_from(NULL), last_fence_release(NULL), - uninitaction(NULL), cv(NULL), rf_cv(NULL), trace_ref(NULL), @@ -143,7 +140,6 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order position(position), reads_from(NULL), last_fence_release(NULL), - uninitaction(NULL), cv(NULL), rf_cv(NULL), trace_ref(NULL), @@ -182,7 +178,6 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order position(position), reads_from(NULL), last_fence_release(NULL), - uninitaction(NULL), cv(NULL), rf_cv(NULL), trace_ref(NULL), @@ -228,8 +223,6 @@ void ModelAction::copy_from_new(ModelAction *newaction) void ModelAction::set_seq_number(modelclock_t num) { - /* ATOMIC_UNINIT actions should never have non-zero clock */ - ASSERT(!is_uninitialized()); ASSERT(seq_number == ACTION_INITIAL_CLOCK); seq_number = num; } @@ -302,11 +295,6 @@ bool ModelAction::is_atomic_var() const return is_read() || could_be_write(); } -bool ModelAction::is_uninitialized() const -{ - return type == ATOMIC_UNINIT; -} - bool ModelAction::is_read() const { return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS || type == ATOMIC_RMW; @@ -314,7 +302,7 @@ bool ModelAction::is_read() const bool ModelAction::is_write() const { - return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE; + return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == NONATOMIC_WRITE; } bool ModelAction::could_be_write() const @@ -643,19 +631,6 @@ void ModelAction::set_read_from(ModelAction *act) ASSERT(act); reads_from = act; - if (act->is_uninitialized()) { // WL - uint64_t val = *((uint64_t *) location); - ModelAction * act_uninitialized = (ModelAction *)act; - act_uninitialized->set_value(val); - reads_from = act_uninitialized; - -// 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()); - */ - } } /** @@ -702,7 +677,6 @@ const char * ModelAction::get_type_str() const case PTHREAD_CREATE: return "pthread create"; case PTHREAD_JOIN: return "pthread join"; - case ATOMIC_UNINIT: return "uninitialized"; case NONATOMIC_WRITE: return "nonatomic write"; case ATOMIC_READ: return "atomic read"; case ATOMIC_WRITE: return "atomic write"; diff --git a/action.h b/action.h index 78f6f140..9486c9df 100644 --- a/action.h +++ b/action.h @@ -58,7 +58,6 @@ typedef enum action_type { PTHREAD_CREATE, // < A pthread creation action PTHREAD_JOIN, // < A pthread join action - ATOMIC_UNINIT, // < Represents an uninitialized atomic NONATOMIC_WRITE, // < Represents a non-atomic store ATOMIC_INIT, // < Initialization of an atomic object (e.g., atomic_init()) ATOMIC_WRITE, // < An atomic write action @@ -85,8 +84,8 @@ typedef enum action_type { * @brief Represents a single atomic action * * A ModelAction is always allocated as non-snapshotting, because it is used in - * multiple executions during backtracking. Except for fake uninitialized - * (ATOMIC_UNINIT) ModelActions, each action is assigned a unique sequence + * multiple executions during backtracking. Except for non-atomic write + * ModelActions, each action is assigned a unique sequence * number. */ class ModelAction { @@ -140,7 +139,6 @@ public: bool is_success_lock() const; bool is_failed_trylock() const; bool is_atomic_var() const; - bool is_uninitialized() const; bool is_read() const; bool is_write() const; bool is_yield() const; @@ -187,8 +185,6 @@ public: /* to accomodate pthread create and join */ Thread * thread_operand; void set_thread_operand(Thread *th) { thread_operand = th; } - void set_uninit_action(ModelAction *act) { uninitaction = act; } - ModelAction * get_uninit_action() { return uninitaction; } void setTraceRef(sllnode *ref) { trace_ref = ref; } void setThrdMapRef(sllnode *ref) { thrdmap_ref = ref; } void setActionRef(sllnode *ref) { action_ref = ref; } @@ -219,7 +215,6 @@ private: /** @brief The last fence release from the same thread */ const ModelAction *last_fence_release; - ModelAction * uninitaction; /** * @brief The clock vector for this operation @@ -253,7 +248,7 @@ private: /** * @brief The sequence number of this action * - * Except for ATOMIC_UNINIT actions, this number should be unique and + * Except for non atomic write actions, this number should be unique and * should represent the action's position in the execution order. */ modelclock_t seq_number; diff --git a/datarace.cc b/datarace.cc index 76fbe936..895e9c01 100644 --- a/datarace.cc +++ b/datarace.cc @@ -66,12 +66,12 @@ bool hasNonAtomicStore(const void *address) { uint64_t shadowval = *shadow; if (ISSHORTRECORD(shadowval)) { //Do we have a non atomic write with a non-zero clock - return ((WRITEVECTOR(shadowval) != 0) && !(ATOMICMASK & shadowval)); + return !(ATOMICMASK & shadowval); } else { if (shadowval == 0) return false; struct RaceRecord *record = (struct RaceRecord *)shadowval; - return !record->isAtomic && record->writeClock != 0; + return !record->isAtomic; } } diff --git a/execution.cc b/execution.cc index 68fd9706..d6988edf 100644 --- a/execution.cc +++ b/execution.cc @@ -711,10 +711,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) wake_up_sleeping_actions(curr); - /* Add uninitialized actions to lists */ - if (!second_part_of_rmw) - add_uninit_action_to_lists(curr); - SnapVector * rf_set = NULL; /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) @@ -1095,58 +1091,6 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { return vec; } -/** - * Performs various bookkeeping operations for the current ModelAction when it is - * the first atomic action occurred at its memory location. - * - * For instance, adds uninitialized action to the per-object, per-thread action vector - * and to the action trace list of all thread actions. - * - * @param act is the ModelAction to process. - */ -void ModelExecution::add_uninit_action_to_lists(ModelAction *act) -{ - int tid = id_to_int(act->get_tid()); - ModelAction *uninit = NULL; - int uninit_id = -1; - SnapVector *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); - if (objvec->empty() && act->is_atomic_var()) { - uninit = get_uninitialized_action(act); - uninit_id = id_to_int(uninit->get_tid()); - SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); - if ((int)vec->size() <= uninit_id) { - int oldsize = (int) vec->size(); - vec->resize(uninit_id + 1); - for(int i = oldsize;i < uninit_id + 1;i++) { - new (&(*vec)[i]) action_list_t(); - } - } - uninit->setActionRef((*vec)[uninit_id].add_front(uninit)); - } - - // Update action trace, a total order of all actions - if (uninit) { - uninit->setTraceRef(action_trace.add_front(uninit)); - } - // Update obj_thrd_map, a per location, per thread, order of actions - SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); - if ((int)vec->size() <= tid) { - uint oldsize = vec->size(); - vec->resize(priv->next_thread_id); - for(uint i = oldsize;i < priv->next_thread_id;i++) - new (&(*vec)[i]) action_list_t(); - } - if (uninit) - uninit->setThrdMapRef((*vec)[uninit_id].add_front(uninit)); - - // Update thrd_last_action, the last action taken by each thrad - if ((int)thrd_last_action.size() <= tid) - thrd_last_action.resize(get_num_threads()); - if (uninit) - thrd_last_action[uninit_id] = uninit; -} - - /** * Performs various bookkeeping operations for the current ModelAction. For * instance, adds action to the per-object, per-thread action vector and to the @@ -1485,25 +1429,6 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu return rf_set; } -/** - * @brief Get an action representing an uninitialized atomic - * - * This function may create a new one. - * - * @param curr The current action, which prompts the creation of an UNINIT action - * @return A pointer to the UNINIT ModelAction - */ -ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const -{ - ModelAction *act = curr->get_uninit_action(); - if (!act) { - act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread); - curr->set_uninit_action(act); - } - act->create_cv(NULL); - return act; -} - static void print_list(action_list_t *list) { sllnode *it; diff --git a/execution.h b/execution.h index 72b51fb8..854513cd 100644 --- a/execution.h +++ b/execution.h @@ -108,7 +108,6 @@ private: void process_thread_action(ModelAction *curr); void read_from(ModelAction *act, ModelAction *rf); bool synchronize(const ModelAction *first, ModelAction *second); - void add_uninit_action_to_lists(ModelAction *act); void add_action_to_lists(ModelAction *act); void add_normal_write_to_lists(ModelAction *act); void add_write_to_lists(ModelAction *act); @@ -121,7 +120,6 @@ private: bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector *priorset, bool *canprune, bool check_only = false); void w_modification_order(ModelAction *curr); ClockVector * get_hb_from_write(ModelAction *rf) const; - ModelAction * get_uninitialized_action(ModelAction *curr) const; ModelAction * convertNonAtomicStore(void*); void removeAction(ModelAction *act); diff --git a/funcinst.cc b/funcinst.cc index 95e93fc2..d4288a14 100644 --- a/funcinst.cc +++ b/funcinst.cc @@ -90,7 +90,7 @@ bool FuncInst::is_read() const * is_write() <==> pure writes (excluding rmw) */ bool FuncInst::is_write() const { - return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE; + return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == NONATOMIC_WRITE; } void FuncInst::print() diff --git a/main.cc b/main.cc index 984d0a31..8fa1e9dd 100644 --- a/main.cc +++ b/main.cc @@ -20,7 +20,6 @@ void param_defaults(struct model_params *params) { params->verbose = !!DBG_ENABLED(); - params->uninitvalue = 0; params->maxexecutions = 10; params->nofork = false; } @@ -47,9 +46,6 @@ static void print_usage(struct model_params *params) " 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" @@ -57,7 +53,6 @@ static void print_usage(struct model_params *params) " -o help for a list of options\n" "-n No fork\n\n", params->verbose, - params->uninitvalue, params->maxexecutions); model_print("Analysis plugins:\n"); for(unsigned int i=0;isize();i++) { @@ -83,11 +78,10 @@ bool install_plugin(char * name) { } void parse_options(struct model_params *params) { - const char *shortopts = "hnt:o:u:x:v::"; + const char *shortopts = "hnt:o:x:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, {"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'}, @@ -134,9 +128,6 @@ void parse_options(struct model_params *params) { case 'v': params->verbose = optarg ? atoi(optarg) : 1; break; - case 'u': - params->uninitvalue = atoi(optarg); - break; case 't': if (install_plugin(optarg)) error = true; diff --git a/params.h b/params.h index d6f5ec9a..b4bfc7e7 100644 --- a/params.h +++ b/params.h @@ -6,7 +6,6 @@ * the model checker. */ struct model_params { - unsigned int uninitvalue; int maxexecutions; bool nofork; -- 2.34.1