model/action: bugfix - UNINIT actions do not have a Node

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 83c79c97ffc654818df100c04ebbf5efa8c244a6..7bff598f974e762daecc27d7d58926bdfa466d68 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1,6 +1,7 @@
 #include <stdio.h>
 #include <algorithm>
 #include <mutex>
+#include <new>
 
 #include "model.h"
 #include "action.h"
@@ -712,7 +713,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        /* Read from future value */
                        value = curr->get_node()->get_future_value();
                        modelclock_t expiration = curr->get_node()->get_future_value_expiration();
-                       read_from(curr, NULL);
+                       curr->set_read_from(NULL);
                        Promise *valuepromise = new Promise(curr, value, expiration);
                        promises->push_back(valuepromise);
                }
@@ -2101,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)
@@ -2447,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++) {
@@ -2488,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");
@@ -2508,7 +2510,10 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 }
 
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
-       while(true) {
+       while (true) {
+               /* UNINIT actions don't have a Node, and they never sleep */
+               if (write->is_uninitialized())
+                       return true;
                Node *prevnode=write->get_node()->get_parent();
 
                bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
@@ -2523,6 +2528,19 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
        }
 }
 
+/**
+ * @brief Create a new action representing an uninitialized atomic
+ * @param location The memory location of the atomic object
+ * @return A pointer to a new ModelAction
+ */
+ModelAction * ModelChecker::new_uninitialized_action(void *location) const
+{
+       ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
+       act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
+       act->create_cv(NULL);
+       return act;
+}
+
 static void print_list(action_list_t *list, int exec_num = -1)
 {
        action_list_t::iterator it;