edits

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index ac3ecbc00e069abd7a53ebbf8d6d70168bf14c97..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.
@@ -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;
 }
 
 /**
@@ -919,6 +920,8 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                if (last_seq_cst != NULL) {
                        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 */
@@ -979,7 +982,7 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                        edgeset.push_back(act);
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       edgeset.push_back(act);
+                                       edgeset.push_back(act->get_reads_from());
                                }
                                break;
                        }
@@ -1207,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())
@@ -1634,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);