more code

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index c07db8e9a7d21a555c789a3053c6bcb2b3846491..38571bec2c22169147903eb3d9ac21a4372b607b 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -66,7 +66,8 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        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.
@@ -390,8 +390,8 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        case ATOMIC_NOTIFY_ALL: {
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                //activate all the waiting threads
-               for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
-                       scheduler->wake(get_thread(*rit));
+               for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
+                 scheduler->wake(get_thread(rit->getVal()));
                }
                waiters->clear();
                break;
@@ -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->get_type() == 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 */
@@ -1098,8 +1101,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                uninit_id = id_to_int(uninit->get_tid());
                list->push_front(uninit);
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
-               if (uninit_id >= (int)vec->size())
-                       vec->resize(uninit_id + 1);
+               if (uninit_id >= (int)vec->size()) {
+                 int oldsize = (int) vec->size();
+                 vec->resize(uninit_id + 1);
+                 for(int i=oldsize; i<uninit_id+1; i++)
+                   new (&vec[i]) action_list_t(); 
+               }
                (*vec)[uninit_id].push_front(uninit);
        }
        list->push_back(act);
@@ -1111,8 +1118,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 
        // 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);
+       if (tid >= (int)vec->size()) {
+         uint oldsize =vec->size();
+         vec->resize(priv->next_thread_id);
+         for(uint i=oldsize; i<priv->next_thread_id; i++)
+           new (&vec[i]) action_list_t(); 
+       }
        (*vec)[tid].push_back(act);
        if (uninit)
                (*vec)[uninit_id].push_front(uninit);
@@ -1136,8 +1147,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
 
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
-               if (tid >= (int)vec->size())
-                       vec->resize(priv->next_thread_id);
+               if (tid >= (int)vec->size()) {
+                 uint oldsize = vec->size();
+                 vec->resize(priv->next_thread_id);
+                 for(uint i=oldsize; i<priv->next_thread_id; i++)
+                   new (&vec[i]) action_list_t(); 
+               }
                (*vec)[tid].push_back(act);
        }
 }
@@ -1196,8 +1211,12 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 
        // 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);
+       if (tid >= (int)vec->size()) {
+         uint oldsize =vec->size();
+         vec->resize(priv->next_thread_id);
+         for(uint i=oldsize; i<priv->next_thread_id; i++)
+           new (&vec[i]) action_list_t();
+       }
        insertIntoActionList(&(*vec)[tid],act);
 
        // Update thrd_last_action, the last action taken by each thrad
@@ -1207,14 +1226,14 @@ 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())
-               vec->resize(priv->next_thread_id);
+       if (tid >= (int)vec->size()) {
+         uint oldsize =vec->size();
+         vec->resize(priv->next_thread_id);
+         for(uint i=oldsize; i<priv->next_thread_id; i++)
+           new (&vec[i]) action_list_t();
+       }
        (*vec)[tid].push_back(write);
 }
 
@@ -1634,7 +1653,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);