changes to allow running programs with racing initialization...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 101a5f0864cb6bc7472ee40e58e8b33b36d3f726..f8aa4f0a4fd49b6eb487539c9fece2d15146e2a0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -498,8 +498,17 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  * @return True if synchronization was updated; false otherwise
  */
 bool ModelChecker::process_mutex(ModelAction *curr) {
-       std::mutex *mutex = (std::mutex *)curr->get_location();
-       struct std::mutex_state *state = mutex->get_state();
+       std::mutex *mutex=NULL;
+       struct std::mutex_state *state=NULL;
+
+       if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
+               mutex = (std::mutex *)curr->get_location();
+               state = mutex->get_state();
+       } else if(curr->is_wait()) {
+               mutex = (std::mutex *)curr->get_value();
+               state = mutex->get_state();
+       }
+
        switch (curr->get_type()) {
        case ATOMIC_TRYLOCK: {
                bool success = !state->islocked;
@@ -1500,8 +1509,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                                continue;
                        }
 
-                       /* Only writes can break release sequences */
-                       if (!act->is_write())
+                       /* Only non-RMW writes can break release sequences */
+                       if (!act->is_write() || act->is_rmw())
                                continue;
 
                        /* Check modification order */
@@ -1657,6 +1666,20 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        if ((int)thrd_last_action->size() <= tid)
                thrd_last_action->resize(get_num_threads());
        (*thrd_last_action)[tid] = act;
+
+       if (act->is_wait()) {
+               void *mutex_loc=(void *) act->get_value();
+               obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+       
+               std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+               if (tid >= (int)vec->size())
+                       vec->resize(priv->next_thread_id);
+               (*vec)[tid].push_back(act);
+
+               if ((int)thrd_last_action->size() <= tid)
+                       thrd_last_action->resize(get_num_threads());
+               (*thrd_last_action)[tid] = act;
+       }
 }
 
 /**
@@ -1708,7 +1731,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
        /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
-               if ((*rit)->is_unlock())
+               if ((*rit)->is_unlock() || (*rit)->is_wait())
                        return *rit;
        return NULL;
 }
@@ -1792,6 +1815,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
                                act->is_read() &&
                                !act->could_synchronize_with(curr) &&
                                !act->same_thread(curr) &&
+                               act->get_location() == curr->get_location() &&
                                promise->get_value() == curr->get_value()) {
                        curr->get_node()->set_promise(i);
                }
@@ -1970,6 +1994,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        if (!initialized) {
                /** @todo Need a more informative way of reporting errors. */
                printf("ERROR: may read from uninitialized atomic\n");
+               set_assert();
        }
 
        if (DBG_ENABLED() || !initialized) {
@@ -1979,8 +2004,6 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }
-
-       ASSERT(initialized);
 }
 
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {