Get rid of uninitialized actions and just use non-atomic writes instead

diff --git a/README.md b/README.md
index 8ae834c4def5af80b37ed5ff5aceba8ac72ea239..f2a6380a332c8c940659de6e854dda12838afe63 100644 (file)
--- 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 ec7332dc696dc6221628e9139e004b59e8ac8d4d..4c1630f48d984ded88dc2b3015525a587a955420 100644 (file)
--- 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 78f6f140af0f19553ce107d090fc30ce429709e5..9486c9df7b39a4835ed345133b64fa73467c223b 100644 (file)
--- 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<ModelAction *> *ref) { trace_ref = ref; }
        void setThrdMapRef(sllnode<ModelAction *> *ref) { thrdmap_ref = ref; }
        void setActionRef(sllnode<ModelAction *> *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 76fbe936260294b96132cfddc47c605dba3e91ab..895e9c019e539ba8ea78840cbd0784fd30e6c2d1 100644 (file)
--- 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 68fd970691f50e2017e4bbcb275284c9c7bccdac..d6988edf3096008288213af4ff20f8b096d1409b 100644 (file)
--- 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<ModelAction *> * 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<action_list_t> *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<action_list_t> *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<action_list_t> *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<ModelAction *> *  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<ModelAction*> *it;

diff --git a/execution.h b/execution.h
index 72b51fb882da49e9958a9bb41a3b3eb515566aba..854513cd4b16cc4c6bc74ad0916fe6d108ea6a78 100644 (file)
--- 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<const ModelAction *> *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 95e93fc20e6865e90c1c67cf05e2df049458b12f..d4288a1438384aff5520ae96aa36016fe6aa8ec6 100644 (file)
--- 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 984d0a317ffc43dd7b095a3fa870c3171bb09e31..8fa1e9dd99a52076043b821653836f916bbb489d 100644 (file)
--- 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;i<registeredanalysis->size();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 d6f5ec9a9fc5a5cf51b7ea3d8571d518b9aaac37..b4bfc7e7b7921b62c80ccf82ba2c0b2bdd30f925 100644 (file)
--- a/params.h
+++ b/params.h
@@ -6,7 +6,6 @@
  * the model checker.
  */
 struct model_params {
-       unsigned int uninitvalue;
        int maxexecutions;
        bool nofork;