threads/model: allocate Thread from w/in ModelChecker

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index ef9bed305fc0295af447e25365cccd6a8f2399a3..400adc208047f8d2c7b4700c31bc20b650854e34 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();
@@ -968,7 +969,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 
        switch (curr->get_type()) {
        case THREAD_CREATE: {
-               Thread *th = curr->get_thread_operand();
+               thrd_t *thrd = (thrd_t *)curr->get_location();
+               struct thread_params *params = (struct thread_params *)curr->get_value();
+               Thread *th = new Thread(thrd, params->func, params->arg);
+               add_thread(th);
                th->set_creation(curr);
                /* Promises can be satisfied by children */
                for (unsigned int i = 0; i < promises->size(); i++) {
@@ -1387,6 +1391,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 +1421,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 +1501,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 +2476,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 +2679,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 +2746,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;
        }