model: add const qualifier to get_thread()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index b5843ed6b7c5ebf6ba091e05afac6ac70593e1ae..8d8944d71ab27e59af1108e2a66debd3d6999596 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -12,6 +12,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "mutex.h"
+#include "threads.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -940,7 +941,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
                                        }
                                } else {
                                        const ModelAction *prevreadfrom = act->get_reads_from();
-                                       if (prevreadfrom != NULL && rf != prevreadfrom) {
+                                       //if the previous read is unresolved, keep going...
+                                       if (prevreadfrom == NULL)
+                                               continue;
+
+                                       if (rf != prevreadfrom) {
                                                mo_graph->addEdge(prevreadfrom, rf);
                                                added = true;
                                        }
@@ -1065,14 +1070,22 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                        ModelAction *act = *rit;
                        if (act == curr) {
                                /*
-                                * If RMW, we already have all relevant edges,
-                                * so just skip to next thread.
-                                * If normal write, we need to look at earlier
-                                * actions, so continue processing list.
+                                * 1) If RMW and it actually read from something, then we
+                                * already have all relevant edges, so just skip to next
+                                * thread.
+                                * 
+                                * 2) If RMW and it didn't read from anything, we should
+                                * whatever edge we can get to speed up convergence.
+                                *
+                                * 3) If normal write, we need to look at earlier actions, so
+                                * continue processing list.
                                 */
-                               if (curr->is_rmw())
-                                       break;
-                               else
+                               if (curr->is_rmw()) {
+                                       if (curr->get_reads_from()!=NULL)
+                                               break;
+                                       else 
+                                               continue;
+                               } else
                                        continue;
                        }
 
@@ -1089,8 +1102,12 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                 */
                                if (act->is_write())
                                        mo_graph->addEdge(act, curr);
-                               else if (act->is_read() && act->get_reads_from() != NULL)
+                               else if (act->is_read()) { 
+                                       //if previous read accessed a null, just keep going
+                                       if (act->get_reads_from() == NULL)
+                                               continue;
                                        mo_graph->addEdge(act->get_reads_from(), curr);
+                               }
                                added = true;
                                break;
                        } else if (act->is_read() && !act->is_synchronizing(curr) &&
@@ -1634,7 +1651,8 @@ void ModelChecker::dumpGraph(char *filename) {
                ModelAction *action=*it;
                if (action->is_read()) {
                        fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
-                       fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+                       if (action->get_reads_from()!=NULL)
+                               fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
                }
                if (thread_array[action->get_tid()] != NULL) {
                        fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
@@ -1695,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));
 }
@@ -1705,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());
 }
@@ -1738,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);
@@ -1752,22 +1770,22 @@ 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);
 
        /* 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);