Calculate store visibility probability and change the shift of a few hashtables in...

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index c3cb3bbd2d78e5d28ca5c6a465a5e3a89c14d4fa..87dbe69eeeea320257cda85dc16b905665502529 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -92,7 +92,7 @@ int ModelExecution::get_execution_number() const
        return model->get_execution_number();
 }
 
-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
 {
        action_list_t *tmp = hash->get(ptr);
        if (tmp == NULL) {
@@ -102,7 +102,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<const 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, 2> * hash, void * ptr)
 {
        SnapVector<action_list_t> *tmp = hash->get(ptr);
        if (tmp == NULL) {
@@ -130,6 +130,12 @@ modelclock_t ModelExecution::get_next_seq_num()
        return ++priv->used_sequence_numbers;
 }
 
+/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
+void ModelExecution::restore_last_seq_num()
+{
+       priv->used_sequence_numbers--;
+}
+
 /**
  * @brief Should the current action wake up a given thread?
  *
@@ -282,7 +288,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
  * @param rf_set is the set of model actions we can possibly read from
  * @return True if processing this read updates the mo_graph.
  */
-void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
+bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
@@ -294,7 +300,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
                if (index == -1)        // no feasible write exists
-                       return;
+                       return false;
 
                ModelAction *rf = (*rf_set)[index];
 
@@ -311,7 +317,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                                int tid = id_to_int(curr->get_tid());
                                (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
                        }
-                       return;
+                       return true;
                }
                priorset->clear();
                (*rf_set)[index] = rf_set->back();
@@ -367,7 +373,27 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                }
                break;
        }
-       case ATOMIC_WAIT:
+       case ATOMIC_WAIT: {
+               /* wake up the other threads */
+               for (unsigned int i = 0;i < get_num_threads();i++) {
+                       Thread *t = get_thread(int_to_id(i));
+                       Thread *curr_thrd = get_thread(curr);
+                       if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+                               scheduler->wake(t);
+               }
+
+               /* unlock the lock - after checking who was waiting on it */
+               state->locked = NULL;
+
+               if (fuzzer->shouldWait(curr)) {
+                       /* disable this thread */
+                       get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+                       scheduler->sleep(get_thread(curr));
+               }
+
+               break;
+       }
+       case ATOMIC_TIMEDWAIT:
        case ATOMIC_UNLOCK: {
                //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T...  TIMED WAITS MUST EVENMTUALLY RELEASE...
 
@@ -381,10 +407,6 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 
                /* unlock the lock - after checking who was waiting on it */
                state->locked = NULL;
-
-               if (!curr->is_wait())
-                       break;/* The rest is only for ATOMIC_WAIT */
-
                break;
        }
        case ATOMIC_NOTIFY_ALL: {
@@ -689,11 +711,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                rf_set = build_may_read_from(curr);
 
        if (curr->is_read() && !second_part_of_rmw) {
-               process_read(curr, rf_set);
+               bool success = process_read(curr, rf_set);
                delete rf_set;
-       } else {
+               if (!success)
+                       return curr;    // Do not add action to lists
+       } else
                ASSERT(rf_set == NULL);
-       }
 
        /* Add the action to lists */
        if (!second_part_of_rmw && curr->get_type() != NOOP)
@@ -1664,7 +1687,7 @@ bool ModelExecution::is_enabled(thread_id_t tid) const
 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
 {
        /* Do not split atomic RMW */
-       if (curr->is_rmwr())
+       if (curr->is_rmwr() && !paused_by_fuzzer(curr))
                return get_thread(curr);
        /* Follow CREATE with the created thread */
        /* which is not needed, because model.cc takes care of this */
@@ -1676,6 +1699,15 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons
        return NULL;
 }
 
+/** @param act A read atomic action */
+bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
+{
+       ASSERT(act->is_read());
+
+       // Actions paused by fuzzer have their sequence number reset to 0
+       return act->get_seq_number() == 0;
+}
+
 /**
  * Takes the next step in the execution, if possible.
  * @param curr The current step to take