seems to work

diff --git a/execution.cc b/execution.cc
index fe27e2ff70ee41c0aa193179ae007cab673d90fc..c193f229348dd569959a7a613732aa080ad3b434 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1671,7 +1671,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 */
@@ -1683,6 +1683,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

diff --git a/execution.h b/execution.h
index da3544ab210332c4bb10dbb08c5cb4e4b68c36c2..622f17aafedaefe74d675f7eb42ca8be37eace61 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -200,6 +200,7 @@ private:
        Fuzzer * fuzzer;
 
        Thread * action_select_next_thread(const ModelAction *curr) const;
+       bool paused_by_fuzzer(const ModelAction * act) const;
 
        /* thrd_func_list stores a list of function ids for each thread.
         * Each element in thrd_func_list stores the functions that

diff --git a/model.cc b/model.cc
index ce598cfa58302841e5cfe4ea0c2c5e8c3f036a1c..4c4b47ac4c12e466bbe4d03b687a9a3f5debf113 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -414,7 +414,7 @@ void ModelChecker::run()
                                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);        // L: context swapped, and action type of thr changed.
+                                       switch_from_master(thr);
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                }