model: set thread state during 'swap' calls

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index ef9bed305fc0295af447e25365cccd6a8f2399a3..08096528bddc326b04dbe31b0772b1fcfb6458f6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -48,6 +48,7 @@ struct model_snapshot_members {
                stats(),
                failed_promise(false),
                too_many_reads(false),
+               no_valid_reads(false),
                bad_synchronization(false),
                asserted(false)
        { }
@@ -66,6 +67,7 @@ struct model_snapshot_members {
        struct execution_stats stats;
        bool failed_promise;
        bool too_many_reads;
+       bool no_valid_reads;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
        bool asserted;
@@ -294,7 +296,6 @@ void ModelChecker::execute_sleep_set()
                thread_id_t tid = int_to_id(i);
                Thread *thr = get_thread(tid);
                if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
-                       thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
                        priv->current_action->set_sleep_flag();
@@ -1387,6 +1388,8 @@ void ModelChecker::print_infeasibility(const char *prefix) const
                ptr += sprintf(ptr, "[failed promise]");
        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 (promises_expired())
@@ -1415,6 +1418,7 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 bool ModelChecker::is_infeasible() const
 {
        return mo_graph->checkForCycles() ||
+               priv->no_valid_reads ||
                priv->failed_promise ||
                priv->too_many_reads ||
                priv->bad_synchronization ||
@@ -1494,13 +1498,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
                                continue;
 
                        /* Test to see whether this is a feasible write to read from */
-                       mo_graph->startChanges();
-                       r_modification_order(curr, write);
-                       bool feasiblereadfrom = !is_infeasible();
-                       mo_graph->rollbackChanges();
+                       /** NOTE: all members of read-from set should be
+                        *  feasible, so we no longer check it here **/
 
-                       if (!feasiblereadfrom)
-                               continue;
                        rit = ritcopy;
 
                        bool feasiblewrite = true;
@@ -2473,14 +2473,25 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
                                allow_read = false;
 
-                       if (allow_read)
-                               curr->get_node()->add_read_from(act);
+                       if (allow_read) {
+                               /* Only add feasible reads */
+                               mo_graph->startChanges();
+                               r_modification_order(curr, act);
+                               if (!is_infeasible())
+                                       curr->get_node()->add_read_from(act);
+                               mo_graph->rollbackChanges();
+                       }
 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr))
                                break;
                }
        }
+       /* We may find no valid may-read-from only if the execution is doomed */
+       if (!curr->get_node()->get_read_from_size()) {
+               priv->no_valid_reads = true;
+               set_assert();
+       }
 
        if (DBG_ENABLED()) {
                model_print("Reached read action:\n");
@@ -2665,7 +2676,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        DBG();
        Thread *old = thread_current();
        set_current_action(act);
-       old->set_state(THREAD_READY);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
                exit(EXIT_FAILURE);
@@ -2733,13 +2743,10 @@ bool ModelChecker::take_step(ModelAction *curr)
        if (!next_thrd)
                return false;
 
-       next_thrd->set_state(THREAD_RUNNING);
-
        if (next_thrd->get_pending() != NULL) {
                /* restart a pending action */
                set_current_action(next_thrd->get_pending());
                next_thrd->set_pending(NULL);
-               next_thrd->set_state(THREAD_READY);
                return true;
        }