refactor choices into own class

diff --git a/Makefile b/Makefile
index e47c4ada3dbf21daacbd398784a3337dce9ba5e0..5411f5838b1802ac45a712bcbff5c5b0f1c93831 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
-          context.o execution.o libannotate.o plugins.o pthread.o futex.o
+          context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic

diff --git a/classlist.h b/classlist.h
index 6d9106fc9b8b6a3fd8eea9181d718f4552eac552..09aa09d134e19c1e4160896fde3a935424fc7ab6 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -1,5 +1,7 @@
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
+#include "stl-model.h"
+
 class ClockVector;
 class CycleGraph;
 class CycleNode;
@@ -11,8 +13,9 @@ class NodeStack;
 class Scheduler;
 class Thread;
 class TraceAnalysis;
+class Fuzzer;
 
 struct model_snapshot_members;
 struct bug_message;
-
+typedef SnapList<ModelAction *> action_list_t;
 #endif

diff --git a/execution.cc b/execution.cc
index dabf550995b4fb7cb02a4d93e74cd476fdbf9a96..a6ed9d689b5b632bf1d14eae241272283c0d47a2 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -14,6 +14,7 @@
 #include "datarace.h"
 #include "threads-model.h"
 #include "bugmessage.h"
+#include "fuzzer.h"
 
 #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),
-               next_backtrack(NULL),
                bugs(),
-               too_many_reads(false),
-               no_valid_reads(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;
-       ModelAction *next_backtrack;
        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;
@@ -73,7 +68,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
        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());
@@ -289,14 +285,13 @@ bool ModelExecution::is_complete_execution() const
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {
-       int random_index = random() % rf_set->size();
        bool updated = false;
                
-       const ModelAction *rf = (*rf_set)[random_index];
+       const ModelAction *rf = fuzzer->selectWrite(curr, rf_set);
+
        ASSERT(rf);
        
        mo_graph->startChanges();
-       
        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());
-
-               //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;
        }
 
@@ -750,10 +733,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
        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)
@@ -771,8 +750,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 bool ModelExecution::is_infeasible() const
 {
        return mo_graph->checkForCycles() ||
-               priv->no_valid_reads ||
-               priv->too_many_reads ||
                priv->bad_synchronization ||
          priv->bad_sc_read;
 }
@@ -1611,3 +1588,6 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        return action_select_next_thread(curr);
 }
 
+Fuzzer * ModelExecution::getFuzzer() {
+  return fuzzer;
+}

diff --git a/execution.h b/execution.h
index d13cc7215c1cfe72fb90476d268611b6259576fc..737477fea7fc2ddb8871e9c34b873bf854c5c526 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -102,7 +102,7 @@ public:
        bool is_deadlocked() const;
 
        action_list_t * get_action_trace() { return &action_trace; }
-
+  Fuzzer * getFuzzer();
        CycleGraph * const get_mo_graph() { return mo_graph; }
   HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
   HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
@@ -206,6 +206,8 @@ private:
         */
        CycleGraph * const mo_graph;
 
+  Fuzzer * fuzzer;
+  
        Thread * action_select_next_thread(const ModelAction *curr) const;
 };
 

diff --git a/fuzzer.cc b/fuzzer.cc
new file mode 100644 (file)
index 0000000..62097b2
--- /dev/null
+++ b/fuzzer.cc
@@ -0,0 +1,26 @@
+#include "fuzzer.h"
+#include <stdlib.h>
+#include "threads-model.h"
+#include "model.h"
+
+ModelAction * Fuzzer::selectWrite(ModelAction *read, ModelVector<ModelAction *> * rf_set) {
+  int random_index = random() % rf_set->size();
+  return (*rf_set)[random_index];
+}
+
+Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) {
+  int random_index = random() % numthreads;
+  int thread = threadlist[random_index];
+  thread_id_t curr_tid = int_to_id(thread);
+  return model->get_thread(curr_tid);
+}
+
+Thread * Fuzzer::selectNotify(action_list_t * waiters) {
+  int numwaiters = waiters->size();
+  int random_index = random() % numwaiters;
+  action_list_t::iterator it = waiters->begin();
+  advance(it, random_index);
+  Thread *thread = model->get_thread(*it);
+  waiters->erase(it);
+  return thread;
+}

diff --git a/fuzzer.h b/fuzzer.h
new file mode 100644 (file)
index 0000000..14d875d
--- /dev/null
+++ b/fuzzer.h
@@ -0,0 +1,16 @@
+#ifndef FUZZER_H
+#define FUZZER_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "stl-model.h"
+
+class Fuzzer {
+public:
+  Fuzzer() {}
+  ModelAction * selectWrite(ModelAction *read, ModelVector<ModelAction *>* rf_set);
+  Thread * selectThread(Node *n, int * threadlist, int numthreads);
+  Thread * selectNotify(action_list_t * waiters);
+  MEMALLOC
+private:
+};
+#endif

diff --git a/schedule.cc b/schedule.cc
index 83616173c2c6c8878817162d8af8c20733766a1c..fff26ce2128a40d7258e13bfd4ab40e3fa2e35f0 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -7,6 +7,7 @@
 #include "model.h"
 #include "nodestack.h"
 #include "execution.h"
+#include "fuzzer.h"
 
 /**
  * Format an "enabled_type_t" for printing
@@ -203,29 +204,19 @@ void Scheduler::wake(Thread *t)
  */
 Thread * Scheduler::select_next_thread(Node *n)
 {
-       int avail_threads = enabled_len;        // number of available threads
-       int thread_list[enabled_len];   // keep a list of threads to select from
-       for (int i = 0; i< enabled_len; i++){
-               thread_list[i] = i;
+       int avail_threads = 0;
+       int thread_list[enabled_len];
+       for (int i = 0; i< enabled_len; i++) {
+         if (enabled[i] == THREAD_ENABLED)
+           thread_list[avail_threads++] = i;
        }
 
-       while (avail_threads > 0) {
-               int random_index = random() % avail_threads;
-               curr_thread_index = thread_list[random_index];  // randomly select a thread from available threads
-               
-               // curr_thread_index = (curr_thread_index + i + 1) % enabled_len;
-               thread_id_t curr_tid = int_to_id(curr_thread_index);
-               
-               if (enabled[curr_thread_index] == THREAD_ENABLED) {
-                       return model->get_thread(curr_tid);
-               } else {        // remove this threads from available threads 
-                       thread_list[random_index] = thread_list[avail_threads - 1]; 
-                       avail_threads--;
-               }
-       }
-       
-       /* No thread was enabled */
-       return NULL;
+       if (avail_threads == 0)
+           return NULL; // No threads availablex
+           
+       Thread * thread = execution->getFuzzer()->selectThread(n, thread_list, avail_threads);
+       curr_thread_index = id_to_int(thread->get_id());
+       return thread;
 }
 
 void Scheduler::set_scheduler_thread(thread_id_t tid) {