main, model: move main execution loop into ModelChecker class

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 4cbcd4fd96b215ddf1440b9a20212b01fb4579d5..964e83fbd623270628ec1b078b2e9d81c9d136c0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -475,25 +475,24 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr)) {
-                               if (act->is_read()) {
+                               if (act->is_read())
                                        cyclegraph->addEdge(curr, act->get_reads_from());
-                               } else
+                               else
                                        cyclegraph->addEdge(curr, act);
                                break;
-                       } else {
-                               if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) {
-                                       /* We have an action that:
-                                                (1) did not happen before us
-                                                (2) is a read and we are a write
-                                                (3) cannot synchronize with us
-                                                (4) is in a different thread
-                                                =>
-                                                that read could potentially read from our write.
-                                       */
-                                       if (act->get_node()->add_future_value(curr->get_value())&&
-                                                       (!next_backtrack || *act > * next_backtrack))
-                                               next_backtrack = act;
-                               }
+                       } else if (act->is_read() && !act->is_synchronizing(curr) &&
+                                                    !act->same_thread(curr)) {
+                               /* We have an action that:
+                                  (1) did not happen before us
+                                  (2) is a read and we are a write
+                                  (3) cannot synchronize with us
+                                  (4) is in a different thread
+                                  =>
+                                  that read could potentially read from our write.
+                                */
+                               if (act->get_node()->add_future_value(curr->get_value()) &&
+                                               (!next_backtrack || *act > *next_backtrack))
+                                       next_backtrack = act;
                        }
                }
        }
@@ -748,3 +747,46 @@ int ModelChecker::switch_to_master(ModelAction *act)
        old->set_state(THREAD_READY);
        return Thread::swap(old, get_system_context());
 }
+
+/**
+ * Takes the next step in the execution, if possible.
+ * @return Returns true (success) if a step was taken and false otherwise.
+ */
+bool ModelChecker::take_step() {
+       Thread *curr, *next;
+
+       curr = thread_current();
+       if (curr) {
+               if (curr->get_state() == THREAD_READY) {
+                       check_current_action();
+                       scheduler->add_thread(curr);
+               } else if (curr->get_state() == THREAD_RUNNING) {
+                       /* Stopped while running; i.e., completed */
+                       curr->complete();
+               } else {
+                       ASSERT(false);
+               }
+       }
+       next = scheduler->next_thread();
+
+       /* 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;
+       /* Return false only if swap fails with an error */
+       return (Thread::swap(get_system_context(), next) == 0);
+}
+
+/** Runs the current execution until threre are no more steps to take. */
+void ModelChecker::finish_execution() {
+       DBG();
+
+       while (take_step());
+}