fixup usage of int vs. thread_id_t

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 39a7c2170f59fb0ac9b3a7d2160ecb80027283ff..788a6706b26074b91db6de091f12ef532c54bd27 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -178,7 +178,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        } else {
                tid = next->get_tid();
        }
-       DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+       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));
 }
@@ -324,7 +324,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
                if (!node->set_backtrack(tid))
                        continue;
                DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-                                       prev->get_tid(), t->get_id());
+                                       id_to_int(prev->get_tid()),
+                                       id_to_int(t->get_id()));
                if (DBG_ENABLED()) {
                        prev->print();
                        act->print();
@@ -794,8 +795,7 @@ bool ModelChecker::isfinalfeasible() {
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
-       int tid = id_to_int(act->get_tid());
-       ModelAction *lastread = get_last_action(tid);
+       ModelAction *lastread = get_last_action(act->get_tid());
        lastread->process_rmw(act);
        if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
                mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
@@ -1713,7 +1713,7 @@ void ModelChecker::remove_thread(Thread *t)
  * @param tid The Thread's ID
  * @return A Thread reference
  */
-Thread * ModelChecker::get_thread(thread_id_t tid)
+Thread * ModelChecker::get_thread(thread_id_t tid) const
 {
        return thread_map->get(id_to_int(tid));
 }
@@ -1723,7 +1723,7 @@ Thread * ModelChecker::get_thread(thread_id_t tid)
  * @param act The ModelAction
  * @return A Thread reference
  */
-Thread * ModelChecker::get_thread(ModelAction *act)
+Thread * ModelChecker::get_thread(ModelAction *act) const
 {
        return get_thread(act->get_tid());
 }
@@ -1756,7 +1756,7 @@ bool ModelChecker::take_step() {
        if (has_asserted())
                return false;
 
-       Thread * curr = thread_current();
+       Thread *curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
                        ASSERT(priv->current_action);
@@ -1770,22 +1770,23 @@ bool ModelChecker::take_step() {
                        ASSERT(false);
                }
        }
-       Thread * next = scheduler->next_thread(priv->nextThread);
+       Thread *next = scheduler->next_thread(priv->nextThread);
 
        /* Infeasible -> don't take any more steps */
        if (!isfeasible())
                return false;
 
-       if (next)
-               next->set_state(THREAD_RUNNING);
-       DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+       DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
+                       next ? id_to_int(next->get_id()) : -1);
 
        /* next == NULL -> don't take any more steps */
        if (!next)
                return false;
 
-       if ( next->get_pending() != NULL ) {
-               //restart a pending action
+       next->set_state(THREAD_RUNNING);
+
+       if (next->get_pending() != NULL) {
+               /* restart a pending action */
                set_current_action(next->get_pending());
                next->set_pending(NULL);
                next->set_state(THREAD_READY);