clean up code
[c11tester.git] / execution.cc
index e3a0a8550aa156055e181411184282216b2b1a42..de7cfa2ffff23e33961700a77ae40a7a582cb2b8 100644 (file)
@@ -6,7 +6,6 @@
 #include "model.h"
 #include "execution.h"
 #include "action.h"
-#include "nodestack.h"
 #include "schedule.h"
 #include "common.h"
 #include "clockvector.h"
@@ -48,7 +47,7 @@ struct model_snapshot_members {
 };
 
 /** @brief Constructor */
-ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
+ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        model(m),
        params(NULL),
        scheduler(scheduler),
@@ -62,16 +61,14 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack
        mutex_map(),
        thrd_last_action(1),
        thrd_last_fence_release(),
-       node_stack(node_stack),
        priv(new struct model_snapshot_members ()),
-                        mo_graph(new CycleGraph()),
+       mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
        add_thread(model_thread);
        scheduler->register_engine(this);
-       node_stack->register_engine(this);
 }
 
 /** @brief Destructor */
@@ -99,7 +96,7 @@ static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t
        return tmp;
 }
 
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 {
        SnapVector<action_list_t> *tmp = hash->get(ptr);
        if (tmp == NULL) {
@@ -522,8 +519,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
 
 /**
  * Initialize the current action by performing one or more of the following
- * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
- * in the NodeStack, manipulating backtracking sets, allocating and
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions,
+ * manipulating backtracking sets, allocating and
  * initializing clock vectors, and computing the promises to fulfill.
  *
  * @param curr The current action, as passed from the user context; may be
@@ -543,7 +540,6 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                ModelAction *newcurr = *curr;
 
                newcurr->set_seq_number(get_next_seq_num());
-               node_stack->add_action(newcurr);
                /* Always compute new clock vector */
                newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 
@@ -953,21 +949,6 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                        mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
                                }
                                break;
-                       } else if (act->is_read() && !act->could_synchronize_with(curr) &&
-                                                                !act->same_thread(curr)) {
-                               /* We have an action that:
-                                  (1) did not happen before us
-                                  (2) is a read and we are a write
-                                  (3) cannot synchronize with us
-                                  (4) is in a different thread
-                                  =>
-                                  that read could potentially read from our write.  Note that
-                                  these checks are overly conservative at this point, we'll
-                                  do more checks before actually removing the
-                                  pendingfuturevalue.
-
-                                */
-
                        }
                }
        }
@@ -1084,10 +1065,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
        }
        list->push_back(act);
 
+       // Update action trace, a total order of all actions
        action_trace.push_back(act);
        if (uninit)
                action_trace.push_front(uninit);
 
+       // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<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);
@@ -1095,12 +1078,14 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
        if (uninit)
                (*vec)[uninit_id].push_front(uninit);
 
+       // Update thrd_last_action, the last action taken by each thrad
        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;
 
+       // Update thrd_last_fence_release, the last release fence taken by each thread
        if (act->is_fence() && act->is_release()) {
                if ((int)thrd_last_fence_release.size() <= tid)
                        thrd_last_fence_release.resize(get_num_threads());
@@ -1343,18 +1328,17 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
 /**
  * @brief Get an action representing an uninitialized atomic
  *
- * This function may create a new one or try to retrieve one from the NodeStack
+ * This function may create a new one.
  *
  * @param curr The current action, which prompts the creation of an UNINIT action
  * @return A pointer to the UNINIT ModelAction
  */
-ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
+ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
 {
-       Node *node = curr->get_node();
-       ModelAction *act = node->get_uninit_action();
+       ModelAction *act = curr->get_uninit_action();
        if (!act) {
                act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
-               node->set_uninit_action(act);
+               curr->set_uninit_action(act);
        }
        act->create_cv(NULL);
        return act;