model: fixup "initialized" check in build_reads_from_past()

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 41e4421c52f3c8b8c932330523771c7a32622649..81679e87ae56f5c3cad43abc525e6365546f54ed 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -27,6 +27,7 @@ ModelChecker::ModelChecker()
        nextThread(THREAD_ID_T_NONE),
        action_trace(new action_list_t()),
        thread_map(new std::map<int, Thread *>),
+       obj_map(new std::map<const void *, action_list_t>()),
        obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
@@ -43,6 +44,7 @@ ModelChecker::~ModelChecker()
        delete thread_map;
 
        delete obj_thrd_map;
+       delete obj_map;
        delete action_trace;
        delete thrd_last_action;
        delete node_stack;
@@ -167,18 +169,17 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
        action_type type = act->get_type();
 
        switch (type) {
-               case THREAD_CREATE:
-               case THREAD_YIELD:
-               case THREAD_JOIN:
-                       return NULL;
                case ATOMIC_READ:
                case ATOMIC_WRITE:
-               default:
+               case ATOMIC_RMW:
                        break;
+               default:
+                       return NULL;
        }
        /* linear search: from most recent to oldest */
+       action_list_t *list = &(*obj_map)[act->get_location()];
        action_list_t::reverse_iterator rit;
-       for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
+       for (rit = list->rbegin(); rit != list->rend(); rit++) {
                ModelAction *prev = *rit;
                if (act->is_synchronizing(prev))
                        return prev;
@@ -272,6 +273,19 @@ void ModelChecker::check_current_action(void)
        set_backtracking(curr);
 
        add_action_to_lists(curr);
+
+       /* Assign reads_from values */
+       /* TODO: perform release/acquire synchronization here; include
+        * reads_from as ModelAction member? */
+       Thread *th = get_thread(curr->get_tid());
+       int value = VALUE_NONE;
+       if (curr->is_read()) {
+               const ModelAction *reads_from = curr->get_node()->get_next_read_from();
+               value = reads_from->get_value();
+               /* Assign reads_from, perform release/acquire synchronization */
+               curr->read_from(reads_from);
+       }
+       th->set_return_value(value);
 }
 
 /**
@@ -283,14 +297,19 @@ void ModelChecker::check_current_action(void)
  */
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
+       int tid = id_to_int(act->get_tid());
        action_trace->push_back(act);
 
+       (*obj_map)[act->get_location()].push_back(act);
+
        std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
-       if (id_to_int(act->get_tid()) >= (int)vec->size())
+       if (tid >= (int)vec->size())
                vec->resize(next_thread_id);
-       (*vec)[id_to_int(act->get_tid())].push_back(act);
+       (*vec)[tid].push_back(act);
 
-       (*thrd_last_action)[id_to_int(act->get_tid())] = act;
+       if ((int)thrd_last_action->size() <= tid)
+               thrd_last_action->resize(get_num_threads());
+       (*thrd_last_action)[tid] = act;
 }
 
 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
@@ -301,6 +320,23 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
        return (*thrd_last_action)[id_to_int(tid)];
 }
 
+/**
+ * Gets the last memory_order_seq_cst action (in the total global sequence)
+ * performed on a particular object (i.e., memory location).
+ * @param location The object location to check
+ * @return The last seq_cst action performed
+ */
+ModelAction * ModelChecker::get_last_seq_cst(const void *location)
+{
+       action_list_t *list = &(*obj_map)[location];
+       /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
+       action_list_t::reverse_iterator rit;
+       for (rit = list->rbegin(); rit != list->rend(); rit++)
+               if ((*rit)->is_write() && (*rit)->is_seqcst())
+                       return *rit;
+       return NULL;
+}
+
 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 {
        ModelAction *parent = get_last_action(tid);
@@ -327,8 +363,17 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ASSERT(curr->is_read());
 
+       ModelAction *last_seq_cst = NULL;
+
+       if (curr->is_seqcst())
+               last_seq_cst = get_last_seq_cst(curr->get_location());
+
        /* Track whether this object has been initialized */
        bool initialized = false;
+       /* Would each action synchronize if we read from it? */
+       bool all_synch = true;
+       /* Is the may_read_from set empty? (tracked locally) */
+       bool empty = true;
 
        for (i = 0; i < thrd_lists->size(); i++) {
                action_list_t *list = &(*thrd_lists)[i];
@@ -340,12 +385,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        if (!act->is_write())
                                continue;
 
-                       DEBUG("Adding action to may_read_from:\n");
-                       if (DBG_ENABLED()) {
-                               act->print();
-                               curr->print();
+                       /* Don't consider more than one seq_cst write */
+                       if (!act->is_seqcst() || act == last_seq_cst) {
+                               DEBUG("Adding action to may_read_from:\n");
+                               if (DBG_ENABLED()) {
+                                       act->print();
+                                       curr->print();
+                               }
+                               curr->get_node()->add_read_from(act);
+                               empty = false;
+
+                               if (!(act->is_release() && curr->is_acquire())
+                                               && !act->same_thread(curr))
+                                       all_synch = false;
                        }
-                       curr->get_node()->add_read_from(act);
 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr)) {
@@ -355,6 +408,9 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                }
        }
 
+       if (!empty && all_synch)
+               initialized = true;
+
        if (!initialized) {
                /* TODO: need a more informative way of reporting errors */
                printf("ERROR: may read from uninitialized atomic\n");