model: remove old "uninitialized" bug check

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 771847ab35d0da14ba6c0b023bb54e0f31a78d19..1499d12aa3a9a6c8c24c9838602c23f532c86140 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2102,18 +2102,32 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
-       action_trace->push_back(act);
+       ModelAction *uninit = NULL;
+       int uninit_id = -1;
+       action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+       if (list->empty()) {
+               uninit = new_uninitialized_action(act->get_location());
+               uninit_id = id_to_int(uninit->get_tid());
+               list->push_back(uninit);
+       }
+       list->push_back(act);
 
-       get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
+       action_trace->push_back(act);
+       if (uninit)
+               action_trace->push_front(uninit);
 
        std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
        if (tid >= (int)vec->size())
                vec->resize(priv->next_thread_id);
        (*vec)[tid].push_back(act);
+       if (uninit)
+               (*vec)[uninit_id].push_front(uninit);
 
        if ((int)thrd_last_action->size() <= tid)
                thrd_last_action->resize(get_num_threads());
        (*thrd_last_action)[tid] = act;
+       if (uninit)
+               (*thrd_last_action)[uninit_id] = uninit;
 
        if (act->is_fence() && act->is_release()) {
                if ((int)thrd_last_fence_release->size() <= tid)
@@ -2448,16 +2462,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ModelAction *last_sc_write = NULL;
 
-       /* Track whether this object has been initialized */
-       bool initialized = false;
-
-       if (curr->is_seqcst()) {
+       if (curr->is_seqcst())
                last_sc_write = get_last_seq_cst_write(curr);
-               /* We have to at least see the last sequentially consistent write,
-                        so we are initialized. */
-               if (last_sc_write != NULL)
-                       initialized = true;
-       }
 
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
@@ -2489,17 +2495,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
-                       if (act->happens_before(curr)) {
-                               initialized = true;
+                       if (act->happens_before(curr))
                                break;
-                       }
                }
        }
 
-       if (!initialized)
-               assert_bug("May read from uninitialized atomic");
-
-       if (DBG_ENABLED() || !initialized) {
+       if (DBG_ENABLED()) {
                model_print("Reached read action:\n");
                curr->print();
                model_print("Printing may_read_from\n");