improve randomization

diff --git a/context.h b/context.h
index ea32d2f5edf3e21a4a95623899df07919eb1cf35..fb56e24761174fdb598f8f055c066ed6420ba02c 100644 (file)
--- a/context.h
+++ b/context.h
@@ -7,6 +7,7 @@
 #define __CONTEXT_H__
 
 #include <ucontext.h>
 #define __CONTEXT_H__
 
 #include <ucontext.h>

+#include <stdio.h>

 
 #ifdef MAC
 
 
 #ifdef MAC
 


@@ -15,7 +16,7 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp);
 #else /* !MAC */
 
 static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
 #else /* !MAC */
 
 static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)

-{
+{      

        return swapcontext(oucp, ucp);
 }
 
        return swapcontext(oucp, ucp);
 }
 

diff --git a/execution.cc b/execution.cc
index 861c82a921d0c268cedbaae889f4e3ed08086335..0fcf4e8d10b206e5a07062849e038c12915264a9 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -2877,6 +2877,19 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons
        /* Do not split atomic RMW */
        if (curr->is_rmwr())
                return get_thread(curr);
        /* Do not split atomic RMW */
        if (curr->is_rmwr())
                return get_thread(curr);

+       if (curr->is_write()) {
+//             std::memory_order order = curr->get_mo(); 
+//             switch(order) {
+//                     case std::memory_order_relaxed: 
+//                             return get_thread(curr);
+//                     case std::memory_order_release:
+//                             return get_thread(curr);
+//                     defalut:
+//                             return NULL;
+//             }       
+               return NULL;
+       }
+

        /* Follow CREATE with the created thread */
        if (curr->get_type() == THREAD_CREATE)
                return curr->get_thread_operand();
        /* Follow CREATE with the created thread */
        if (curr->get_type() == THREAD_CREATE)
                return curr->get_thread_operand();

diff --git a/main.cc b/main.cc
index 61554eaa8e11b0d684d1d13a9df5d9a60aca2e83..0d4a6ad7d34b6c62397c2a007da8c1a4a5fcde0a 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -100,7 +100,6 @@ static void print_usage(const char *program_name, struct model_params *params)
                params->verbose,
     params->uninitvalue,
                params->maxexecutions);
                params->verbose,
     params->uninitvalue,
                params->maxexecutions);

-       model_print("Analysis plugins:\n");

 
        exit(EXIT_SUCCESS);
 }
 
        exit(EXIT_SUCCESS);
 }

diff --git a/model.cc b/model.cc
index 0e65c63c9e18f8bb6c45b6fe389facd6f839ee4a..bfb6d22f85009e61e0d4fbad5926764328a4a8fd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -3,6 +3,7 @@
 #include <new>
 #include <stdarg.h>
 #include <string.h>
 #include <new>
 #include <stdarg.h>
 #include <string.h>

+#include <cstdlib>

 
 #include "model.h"
 #include "action.h"
 
 #include "model.h"
 #include "action.h"


@@ -100,10 +101,9 @@ Thread * ModelChecker::get_next_thread()
         * Have we completed exploring the preselected path? Then let the
         * scheduler decide
         */
         * Have we completed exploring the preselected path? Then let the
         * scheduler decide
         */

-       if (diverge == NULL)
+       if (diverge == NULL)    // W: diverge is set to NULL permanently

                return scheduler->select_next_thread(node_stack->get_head());
 
                return scheduler->select_next_thread(node_stack->get_head());
 

-

        /* Else, we are trying to replay an execution */
        ModelAction *next = node_stack->get_next()->get_action();
 
        /* Else, we are trying to replay an execution */
        ModelAction *next = node_stack->get_next()->get_action();
 


@@ -303,32 +303,40 @@ bool ModelChecker::next_execution()
 
                checkDataRaces();
                run_trace_analyses();
 
                checkDataRaces();
                run_trace_analyses();

-       } else if (inspect_plugin && !execution->is_complete_execution() &&
-               (execution->too_many_steps())) {
-                inspect_plugin->analyze(execution->get_action_trace());
-       }
+       } 

 
        record_stats();
 
        record_stats();

-

        /* Output */
        if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
                print_execution(complete);
        else
                clear_program_output();
 
        /* Output */
        if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
                print_execution(complete);
        else
                clear_program_output();
 

-       if (complete)
-               earliest_diverge = NULL;
-

        if (restart_flag) {
                do_restart();
                return true;
        }
        if (restart_flag) {
                do_restart();
                return true;
        }

+// test code
+       execution_number++;
+       reset_to_initial_state();
+       node_stack->pop_restofstack(2);
+//     node_stack->full_reset();
+       diverge = NULL;
+       return false;
+/* test
+       if (complete)
+               earliest_diverge = NULL;

 
        if (exit_flag)
                return false;
 
 
        if (exit_flag)
                return false;
 

-       if ((diverge = execution->get_next_backtrack()) == NULL)
+//     diverge = execution->get_next_backtrack();
+       if (diverge == NULL) {
+               execution_number++;
+               reset_to_initial_state();
+               model_print("Does not diverge\n");

                return false;
                return false;

+       } 

 
        if (DBG_ENABLED()) {
                model_print("Next execution will diverge at:\n");
 
        if (DBG_ENABLED()) {
                model_print("Next execution will diverge at:\n");


@@ -342,6 +350,8 @@ bool ModelChecker::next_execution()
 
        reset_to_initial_state();
        return true;
 
        reset_to_initial_state();
        return true;

+*/
+

 }
 
 /** @brief Run trace analyses on complete trace */
 }
 
 /** @brief Run trace analyses on complete trace */


@@ -400,9 +410,10 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());

+/* W: No plugin

        if (inspect_plugin != NULL) {
        if (inspect_plugin != NULL) {

-               inspect_plugin->inspectModelAction(act);
-       }
+               inspect_plugin->inspectModelAction(act); 
+       }*/

        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");


@@ -461,11 +472,11 @@ void ModelChecker::do_restart()
 void ModelChecker::run()
 {
        bool has_next;
 void ModelChecker::run()
 {
        bool has_next;

+       int i = 0;

        do {
                thrd_t user_thread;
        do {
                thrd_t user_thread;

-               Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL);
+               Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program

                execution->add_thread(t);
                execution->add_thread(t);

-

                do {
                        /*
                         * Stash next pending action(s) for thread(s). There
                do {
                        /*
                         * Stash next pending action(s) for thread(s). There


@@ -473,11 +484,12 @@ void ModelChecker::run()
                         * thread which just took a step--plus the first step
                         * for any newly-created thread
                         */
                         * thread which just took a step--plus the first step
                         * for any newly-created thread
                         */

+

                        for (unsigned int i = 0; i < get_num_threads(); i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
                                if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
                        for (unsigned int i = 0; i < get_num_threads(); i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
                                if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {

-                                       switch_from_master(thr);
+                                       switch_from_master(thr);        // L: context swapped, and action type of thr changed. 

                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                }
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                }


@@ -491,13 +503,30 @@ void ModelChecker::run()
                                        scheduler->sleep(th);
                                }
                        }
                                        scheduler->sleep(th);
                                }
                        }

-

                        /* Catch assertions from prior take_step or from
                         * between-ModelAction bugs (e.g., data races) */
                        /* Catch assertions from prior take_step or from
                         * between-ModelAction bugs (e.g., data races) */

+
+                       for (unsigned int i = 1; i < get_num_threads(); i++) {
+                               Thread *th = get_thread(int_to_id(i));
+                               ModelAction *act = th->get_pending();
+                               if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ){
+                                       if (act->is_write()){
+                                               std::memory_order order = act->get_mo(); 
+                                               if (order == std::memory_order_relaxed || order == std::memory_order_release) {
+                                                       t = th;
+                                                       break;
+                                               }
+                                       } else if (act->get_type() == THREAD_CREATE || act->get_type() == THREAD_START || act->get_type() == THREAD_FINISH) {
+                                               t = th;
+                                               break;
+                                       }                               
+                               }
+                       }
+
+

                        if (execution->has_asserted())
                                break;
                        if (execution->has_asserted())
                                break;

-
-                       if (!t)
+                       if (!t)                         

                                t = get_next_thread();
                        if (!t || t->is_model_thread())
                                break;
                                t = get_next_thread();
                        if (!t || t->is_model_thread())
                                break;


@@ -509,16 +538,8 @@ void ModelChecker::run()
                } while (!should_terminate_execution());
 
                has_next = next_execution();
                } while (!should_terminate_execution());
 
                has_next = next_execution();

-               if (inspect_plugin != NULL && !has_next) {
-                       inspect_plugin->actionAtModelCheckingFinish();
-                       // Check if the inpect plugin set the restart flag
-                       if (restart_flag) {
-                               model_print("******* Model-checking RESTART: *******\n");
-                               has_next = true;
-                               do_restart();
-                       }
-               }
-       } while (has_next);
+               i++;
+       } while (i<250); // while (has_next);

 
        execution->fixup_release_sequences();
 
 
        execution->fixup_release_sequences();
 

diff --git a/nodestack.cc b/nodestack.cc
index bacd067dcb4b8277408e2efd5685fc27bac8e2da..f1856d360f434d04363d544834e4c081816283bb 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -1,5 +1,6 @@
 #define __STDC_FORMAT_MACROS
 #include <inttypes.h>
 #define __STDC_FORMAT_MACROS
 #include <inttypes.h>

+#include <cstdlib>

 
 #include <string.h>
 
 
 #include <string.h>
 


@@ -488,8 +489,11 @@ void Node::add_read_from_past(const ModelAction *act)
  */
 const ModelAction * Node::get_read_from_past() const
 {
  */
 const ModelAction * Node::get_read_from_past() const
 {

-       if (read_from_past_idx < read_from_past.size())
-               return read_from_past[read_from_past_idx];
+       if (read_from_past_idx < read_from_past.size()) {
+               int random_index = rand() % read_from_past.size(); 
+               return read_from_past[random_index];
+       }
+//             return read_from_past[read_from_past_idx];

        else
                return NULL;
 }
        else
                return NULL;
 }

diff --git a/schedule.cc b/schedule.cc
index 2ef4c4d2f968ef2c97dffbf8f17a3e80c447c9cd..2a02e307cf69f3a6a35058254bcafd046300645e 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -214,8 +214,6 @@ void Scheduler::wake(Thread *t)
  */
 Thread * Scheduler::select_next_thread(Node *n)
 {
  */
 Thread * Scheduler::select_next_thread(Node *n)
 {

-       int old_curr_thread = curr_thread_index;
-

        bool have_enabled_thread_with_priority = false;
        if (model->params.fairwindow != 0) {
                for (int i = 0; i < enabled_len; i++) {
        bool have_enabled_thread_with_priority = false;
        if (model->params.fairwindow != 0) {
                for (int i = 0; i < enabled_len; i++) {


@@ -228,8 +226,17 @@ Thread * Scheduler::select_next_thread(Node *n)
                }
        }       
 
                }
        }       
 

-       for (int i = 0; i < enabled_len; i++) {
-               curr_thread_index = (old_curr_thread + i + 1) % enabled_len;
+       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;
+       }
+
+       while (avail_threads > 0) {
+               int random_index = rand() % 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 (model->params.yieldon) {
                        bool bad_thread = false;
                thread_id_t curr_tid = int_to_id(curr_thread_index);
                if (model->params.yieldon) {
                        bool bad_thread = false;


@@ -240,13 +247,20 @@ Thread * Scheduler::select_next_thread(Node *n)
                                        break;
                                }
                        }
                                        break;
                                }
                        }

-                       if (bad_thread)
+                       if (bad_thread) {
+                               thread_list[random_index] = thread_list[avail_threads - 1]; // remove this threads from available threads 
+                               avail_threads--;
+

                                continue;
                                continue;

+                       }

                }
                
                if (enabled[curr_thread_index] == THREAD_ENABLED &&
                                (!have_enabled_thread_with_priority || n->has_priority(curr_tid))) {
                        return model->get_thread(curr_tid);
                }
                
                if (enabled[curr_thread_index] == THREAD_ENABLED &&
                                (!have_enabled_thread_with_priority || n->has_priority(curr_tid))) {
                        return model->get_thread(curr_tid);

+               } else {        // remove this threads from available threads 
+                       thread_list[random_index] = thread_list[avail_threads - 1]; 
+                       avail_threads--;

                }
        }
        
                }
        }