model, nodestack: bugfix - retain UNINIT actions across executions

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index d15a094f7d8049e1a1e81ed8ac78527b6d1ca66a..d2a2c744bea23c0462db61861a6be583f2d50cef 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -822,6 +822,21 @@ void ModelChecker::set_backtracking(ModelAction *act)
                        if (unfair)
                                continue;
                }
+
+               /* See if CHESS-like yield fairness allows */
+               if (model->params.yieldon) {
+                       bool unfair = false;
+                       for (int t = 0; t < node->get_num_threads(); t++) {
+                               thread_id_t tother = int_to_id(t);
+                               if (node->is_enabled(tother) && node->has_priority_over(tid, tother)) {
+                                       unfair = true;
+                                       break;
+                               }
+                       }
+                       if (unfair)
+                               continue;
+               }
+               
                /* Cache the latest backtracking point */
                set_latest_backtrack(prev);
 
@@ -1369,6 +1384,8 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 {
        ASSERT(rf);
+       ASSERT(rf->is_write());
+
        act->set_read_from(rf);
        if (act->is_acquire()) {
                rel_heads_list_t release_heads;
@@ -1476,6 +1493,11 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
        wake_up_sleeping_actions(curr);
 
+       /* Compute fairness information for CHESS yield algorithm */
+       if (model->params.yieldon) {
+               curr->get_node()->update_yield(scheduler);
+       }
+
        /* Add the action to lists before any other model-checking tasks */
        if (!second_part_of_rmw)
                add_action_to_lists(curr);
@@ -2350,9 +2372,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        int uninit_id = -1;
        action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
        if (list->empty() && act->is_atomic_var()) {
-               uninit = new_uninitialized_action(act->get_location());
+               uninit = get_uninitialized_action(act);
                uninit_id = id_to_int(uninit->get_tid());
-               list->push_back(uninit);
+               list->push_front(uninit);
        }
        list->push_back(act);
 
@@ -2793,14 +2815,21 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri
 }
 
 /**
- * @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
+ * @brief Get an action representing an uninitialized atomic
+ *
+ * This function may create a new one or try to retrieve one from the NodeStack
+ *
+ * @param curr The current action, which prompts the creation of an UNINIT action
+ * @return A pointer to the UNINIT ModelAction
  */
-ModelAction * ModelChecker::new_uninitialized_action(void *location) const
+ModelAction * ModelChecker::get_uninitialized_action(const ModelAction *curr) const
 {
-       ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
-       act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
+       Node *node = curr->get_node();
+       ModelAction *act = node->get_uninit_action();
+       if (!act) {
+               act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), 0, model_thread);
+               node->set_uninit_action(act);
+       }
        act->create_cv(NULL);
        return act;
 }
@@ -2814,7 +2843,9 @@ static void print_list(action_list_t *list)
        unsigned int hash = 0;
 
        for (it = list->begin(); it != list->end(); it++) {
-               (*it)->print();
+               const ModelAction *act = *it;
+               if (act->get_seq_number() > 0)
+                       act->print();
                hash = hash^(hash<<3)^((*it)->hash());
        }
        model_print("HASH %u\n", hash);