Fix RMW bug

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 7d38eb43f3f721a99017d2e05d8ce243e9e4efde..b08bbcf9f1b76dc574cfa295d74d9241d017bf31 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -14,6 +14,7 @@
 #include "datarace.h"
 #include "threads-model.h"
 #include "bugmessage.h"
 #include "datarace.h"
 #include "threads-model.h"
 #include "bugmessage.h"

+#include "fuzzer.h"

 
 #define INITIAL_THREAD_ID      0
 
 
 #define INITIAL_THREAD_ID      0
 


@@ -25,10 +26,7 @@ struct model_snapshot_members {
                /* First thread created will have id INITIAL_THREAD_ID */
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
                /* First thread created will have id INITIAL_THREAD_ID */
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),

-               next_backtrack(NULL),

                bugs(),
                bugs(),

-               too_many_reads(false),
-               no_valid_reads(false),

                bad_synchronization(false),
                bad_sc_read(false),
                asserted(false)
                bad_synchronization(false),
                bad_sc_read(false),
                asserted(false)


@@ -42,10 +40,7 @@ struct model_snapshot_members {
 
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
 
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;

-       ModelAction *next_backtrack;

        SnapVector<bug_message *> bugs;
        SnapVector<bug_message *> bugs;

-       bool too_many_reads;
-       bool no_valid_reads;

        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
        bool bad_sc_read;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
        bool bad_sc_read;


@@ -73,7 +68,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
        thrd_last_fence_release(),
        node_stack(node_stack),
        priv(new struct model_snapshot_members()),
        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());
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());


@@ -289,14 +285,13 @@ bool ModelExecution::is_complete_execution() const
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {

-       int random_index = random() % rf_set->size();

        bool updated = false;
                
        bool updated = false;
                

-       const ModelAction *rf = (*rf_set)[random_index];
+       const ModelAction *rf = fuzzer->selectWrite(curr, rf_set);
+

        ASSERT(rf);
        
        mo_graph->startChanges();
        ASSERT(rf);
        
        mo_graph->startChanges();

-       

        updated = r_modification_order(curr, rf);
        read_from(curr, rf);
        mo_graph->commitChanges();
        updated = r_modification_order(curr, rf);
        read_from(curr, rf);
        mo_graph->commitChanges();


@@ -380,20 +375,8 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        }
        case ATOMIC_NOTIFY_ONE: {
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
        }
        case ATOMIC_NOTIFY_ONE: {
                action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());

-
-               //BCD -- TOFIX FUZZER
-               //THIS SHOULD BE A RANDOM CHOICE
-               //              int wakeupthread = curr->get_node()->get_misc();
-               int wakeupthread = 0;
-               action_list_t::iterator it = waiters->begin();
-
-               // WL
-               if (it == waiters->end())
-                       break;
-
-               advance(it, wakeupthread);
-               scheduler->wake(get_thread(*it));
-               waiters->erase(it);
+               Thread * thread = fuzzer->selectNotify(waiters);
+               scheduler->wake(thread);

                break;
        }
 
                break;
        }
 


@@ -495,7 +478,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                break;
        }
        case PTHREAD_CREATE: {
                break;
        }
        case PTHREAD_CREATE: {

-               (*(pthread_t *)curr->get_location()) = pthread_counter++;       
+         (*(uint32_t *)curr->get_location()) = pthread_counter++;

 
                struct pthread_params *params = (struct pthread_params *)curr->get_value();
                Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
 
                struct pthread_params *params = (struct pthread_params *)curr->get_value();
                Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));


@@ -750,10 +733,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
        char *ptr = buf;
        if (mo_graph->checkForCycles())
                ptr += sprintf(ptr, "[mo cycle]");
        char *ptr = buf;
        if (mo_graph->checkForCycles())
                ptr += sprintf(ptr, "[mo cycle]");

-       if (priv->too_many_reads)
-               ptr += sprintf(ptr, "[too many reads]");
-       if (priv->no_valid_reads)
-               ptr += sprintf(ptr, "[no valid reads-from]");

        if (priv->bad_synchronization)
                ptr += sprintf(ptr, "[bad sw ordering]");
        if (priv->bad_sc_read)
        if (priv->bad_synchronization)
                ptr += sprintf(ptr, "[bad sw ordering]");
        if (priv->bad_sc_read)


@@ -771,8 +750,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 bool ModelExecution::is_infeasible() const
 {
        return mo_graph->checkForCycles() ||
 bool ModelExecution::is_infeasible() const
 {
        return mo_graph->checkForCycles() ||

-               priv->no_valid_reads ||
-               priv->too_many_reads ||

                priv->bad_synchronization ||
          priv->bad_sc_read;
 }
                priv->bad_synchronization ||
          priv->bad_sc_read;
 }


@@ -1317,6 +1294,22 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const
        return get_parent_action(tid)->get_cv();
 }
 
        return get_parent_action(tid)->get_cv();
 }
 

+bool valequals(uint64_t val1, uint64_t val2, int size) {
+  switch(size) {
+  case 1:
+    return ((uint8_t)val1) == ((uint8_t)val2);
+  case 2:
+    return ((uint16_t)val1) == ((uint16_t)val2);
+  case 4:
+    return ((uint32_t)val1) == ((uint32_t)val2);
+  case 8:
+    return val1==val2;
+  default:
+    ASSERT(0);
+    return false;
+  }
+}
+

 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from, as well as any previously-observed future values that must still be valid.
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from, as well as any previously-observed future values that must still be valid.


@@ -1355,6 +1348,20 @@ ModelVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *c
                        if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
                                allow_read = false;
 
                        if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
                                allow_read = false;
 

+                       /* Need to check whether we will have two RMW reading from the same value */
+                       if (curr->is_rmwr()) {
+                         /* It is okay if we have a failing CAS */
+                         if (!curr->is_rmwrcas() ||
+                             valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+                               //Need to make sure we aren't the second RMW
+                               CycleNode * node = mo_graph->getNode_noCreate(act);
+                               if (node != NULL && node->getRMW() != NULL) {
+                                 //we are the second RMW
+                                 allow_read = false;
+                               }
+                             }
+                       }
+                       

                        if (allow_read) {
                                /* Only add feasible reads */
                                mo_graph->startChanges();
                        if (allow_read) {
                                /* Only add feasible reads */
                                mo_graph->startChanges();


@@ -1522,7 +1529,13 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const
  * @return A Thread reference
  */
 Thread * ModelExecution::get_pthread(pthread_t pid) {
  * @return A Thread reference
  */
 Thread * ModelExecution::get_pthread(pthread_t pid) {

-        if (pid < pthread_counter + 1) return pthread_map[pid];
+  union {
+    pthread_t p;
+    uint32_t v;
+  } x;
+  x.p = pid;
+  uint32_t thread_id = x.v;
+  if (thread_id < pthread_counter + 1) return pthread_map[thread_id];

         else return NULL;
 }
 
         else return NULL;
 }
 


@@ -1605,3 +1618,6 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        return action_select_next_thread(curr);
 }
 
        return action_select_next_thread(curr);
 }
 

+Fuzzer * ModelExecution::getFuzzer() {
+  return fuzzer;
+}