common: make model_print() use OS file descriptor, not C library FILE*

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 4d62361197dd5c416a15ab6754186e60d679857e..f385e560f085cc9af3aec101207f732a7a3ef8e3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -154,9 +154,6 @@ void ModelChecker::reset_to_initial_state()
        DEBUG("+++ Resetting to initial state +++\n");
        node_stack->reset_execution();
 
-       /* Print all model-checker output before rollback */
-       fflush(model_out);
-
        /**
         * FIXME: if we utilize partial rollback, we will need to free only
         * those pending actions which were NOT pending before the rollback
@@ -286,7 +283,7 @@ Thread * ModelChecker::get_next_thread()
        }
        DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
        ASSERT(tid != THREAD_ID_T_NONE);
-       return thread_map->get(id_to_int(tid));
+       return get_thread(id_to_int(tid));
 }
 
 /**
@@ -755,6 +752,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
        Node *node = prev->get_node()->get_parent();
 
+       /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
        int low_tid, high_tid;
        if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
                low_tid = id_to_int(act->get_tid());
@@ -771,6 +769,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
                if (i >= node->get_num_threads())
                        break;
 
+               /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
                /* Don't backtrack into a point where the thread is disabled or sleeping. */
                if (node->enabled_status(tid) != THREAD_ENABLED)
                        continue;
@@ -1219,9 +1218,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
        }
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
-               while (!th->wait_list_empty()) {
-                       ModelAction *act = th->pop_wait_list();
-                       scheduler->wake(get_thread(act));
+               /* Wake up any joining threads */
+               for (unsigned int i = 0; i < get_num_threads(); i++) {
+                       Thread *waiting = get_thread(int_to_id(i));
+                       if (waiting->waiting_on() == th &&
+                                       waiting->get_pending()->is_thread_join())
+                               scheduler->wake(waiting);
                }
                th->complete();
                /* Completed thread can't satisfy promises */
@@ -1464,7 +1466,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
        } else if (curr->is_thread_join()) {
                Thread *blocking = curr->get_thread_operand();
                if (!blocking->is_complete()) {
-                       blocking->push_wait_list(curr);
                        thread_blocking_check_promises(blocking, get_thread(curr));
                        return false;
                }