edits

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 33a608d6fa18f55b869045b67d6485b6332bb1d6..32fa727daa9fdd13807b929d2e2fc1abea0e6453 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -63,10 +63,11 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        thrd_last_action(1),
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
-       mo_graph(new CycleGraph()),
+                        mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer()),
        thrd_func_list(),
-       thrd_func_inst_lists()
+       thrd_func_inst_lists(),
+       isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
@@ -277,7 +278,6 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
        return act;
 }
 
-
 /**
  * Processes a read model action.
  * @param curr is the read model action to process.
@@ -461,8 +461,8 @@ bool ModelExecution::process_fence(ModelAction *curr)
                                continue;
 
                        /* Establish hypothetical release sequences */
-                       ClockVector *cv = get_hb_from_write(act);
-                       if (curr->get_cv()->merge(cv))
+                       ClockVector *cv = get_hb_from_write(act->get_reads_from());
+                       if (cv != NULL && curr->get_cv()->merge(cv))
                                updated = true;
                }
        }
@@ -480,10 +480,8 @@ bool ModelExecution::process_fence(ModelAction *curr)
  * @param curr The current action
  * @return True if synchronization was updated or a thread completed
  */
-bool ModelExecution::process_thread_action(ModelAction *curr)
+void ModelExecution::process_thread_action(ModelAction *curr)
 {
-       bool updated = false;
-
        switch (curr->get_type()) {
        case THREAD_CREATE: {
                thrd_t *thrd = (thrd_t *)curr->get_location();
@@ -513,19 +511,25 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
-               updated = true; /* trigger rel-seq checks */
                break;
        }
        case PTHREAD_JOIN: {
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
-               updated = true; /* trigger rel-seq checks */
                break;  // WL: to be add (modified)
        }
 
+       case THREADONLY_FINISH:
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
+               if (curr == THREAD_FINISH &&
+                               th == model->getInitThread()) {
+                       th->complete();
+                       setFinished();
+                       break;
+               }
+
                /* Wake up any joining threads */
                for (unsigned int i = 0;i < get_num_threads();i++) {
                        Thread *waiting = get_thread(int_to_id(i));
@@ -534,7 +538,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                                scheduler->wake(waiting);
                }
                th->complete();
-               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_START: {
@@ -543,8 +546,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
        default:
                break;
        }
-
-       return updated;
 }
 
 /**
@@ -852,7 +853,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                        if (act->happens_before(curr)) {
                                if (i==0) {
                                        if (last_sc_fence_local == NULL ||
-                                                       (*last_sc_fence_local < *prev_same_thread)) {
+                                                       (*last_sc_fence_local < *act)) {
                                                prev_same_thread = act;
                                        }
                                }
@@ -910,13 +911,17 @@ void ModelExecution::w_modification_order(ModelAction *curr)
        unsigned int i;
        ASSERT(curr->is_write());
 
+       SnapList<ModelAction *> edgeset;
+
        if (curr->is_seqcst()) {
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
                ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
                if (last_seq_cst != NULL) {
-                       mo_graph->addEdge(last_seq_cst, curr);
+                       edgeset.push_back(last_seq_cst);
                }
+               //update map for next query
+               obj_last_sc_map.put(curr->get_location(), curr);
        }
 
        /* Last SC fence in the current thread */
@@ -932,7 +937,6 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
-               bool force_edge = false;
                for (rit = list->rbegin();rit != list->rend();rit++) {
                        ModelAction *act = *rit;
                        if (act == curr) {
@@ -947,7 +951,6 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 * 3) If normal write, we need to look at earlier actions, so
                                 * continue processing list.
                                 */
-                               force_edge = true;
                                if (curr->is_rmw()) {
                                        if (curr->get_reads_from() != NULL)
                                                break;
@@ -960,7 +963,7 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                        /* C++, Section 29.3 statement 7 */
                        if (last_sc_fence_thread_before && act->is_write() &&
                                        *act < *last_sc_fence_thread_before) {
-                               mo_graph->addEdge(act, curr, force_edge);
+                               edgeset.push_back(act);
                                break;
                        }
 
@@ -976,15 +979,17 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 *   readfrom(act) --mo--> act
                                 */
                                if (act->is_write())
-                                       mo_graph->addEdge(act, curr, force_edge);
+                                       edgeset.push_back(act);
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
+                                       edgeset.push_back(act->get_reads_from());
                                }
                                break;
                        }
                }
        }
+       mo_graph->addEdges(&edgeset, curr);
+
 }
 
 /**
@@ -1205,10 +1210,6 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 
 
 void ModelExecution::add_write_to_lists(ModelAction *write) {
-       // Update seq_cst map
-       if (write->is_seqcst())
-               obj_last_sc_map.put(write->get_location(), write);
-
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
        int tid = id_to_int(write->get_tid());
        if (tid >= (int)vec->size())
@@ -1632,7 +1633,7 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        ASSERT(curr);
 
        /* Process this action in ModelHistory for records*/
-       model->get_history()->process_action( curr, curr_thrd->get_id() );
+       model->get_history()->process_action( curr, curr->get_tid() );
 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);