X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=967fd39e26955a561a04cf7e485c5d94c31978bc;hb=544dab66fd213c49e18e276748b3352b1063cc52;hp=e49acfcf18566959c21e5e616345be75b215b377;hpb=936b81aa71ea88fb0336594916ff4820c15ad9a5;p=model-checker.git diff --git a/main.cc b/main.cc index e49acfc..967fd39 100644 --- a/main.cc +++ b/main.cc @@ -1,3 +1,5 @@ +/* -*- Mode: C; indent-tabs-mode: t -*- */ + #include "libthreads.h" #include "common.h" #include "threads.h" @@ -11,59 +13,59 @@ * Return 1 if found next thread, 0 otherwise */ static int thread_system_next(void) { - Thread *curr, *next; + Thread *curr, *next; - curr = thread_current(); - if (curr) { - if (curr->get_state() == THREAD_READY) { - model->check_current_action(); - model->scheduler->add_thread(curr); - } else if (curr->get_state() == THREAD_RUNNING) - /* Stopped while running; i.e., completed */ - curr->complete(); - else - ASSERT(false); - } - next = model->scheduler->next_thread(); - if (next) - next->set_state(THREAD_RUNNING); - DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); - if (!next) - return 1; - return Thread::swap(model->get_system_context(), next); + curr = thread_current(); + if (curr) { + if (curr->get_state() == THREAD_READY) { + model->check_current_action(); + model->scheduler->add_thread(curr); + } else if (curr->get_state() == THREAD_RUNNING) + /* Stopped while running; i.e., completed */ + curr->complete(); + else + ASSERT(false); + } + next = model->scheduler->next_thread(); + if (next) + next->set_state(THREAD_RUNNING); + DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); + if (!next) + return 1; + return Thread::swap(model->get_system_context(), next); } static void thread_wait_finish(void) { - DBG(); + DBG(); - while (!thread_system_next()); + while (!thread_system_next()); } void real_main() { - thrd_t user_thread; - ucontext_t main_context; + thrd_t user_thread; + ucontext_t main_context; - //Create the singleton snapshotStack object - snapshotObject = new snapshotStack(); + //Create the singleton snapshotStack object + snapshotObject = new snapshotStack(); - model = new ModelChecker(); + model = new ModelChecker(); - if (getcontext(&main_context)) - return; + if (getcontext(&main_context)) + return; - model->set_system_context(&main_context); + model->set_system_context(&main_context); - do { - /* Start user program */ - model->add_thread(new Thread(&user_thread, &user_main, NULL)); + do { + /* Start user program */ + model->add_thread(new Thread(&user_thread, &user_main, NULL)); - /* Wait for all threads to complete */ - thread_wait_finish(); - } while (model->next_execution()); + /* Wait for all threads to complete */ + thread_wait_finish(); + } while (model->next_execution()); - delete model; + delete model; - DEBUG("Exiting\n"); + DEBUG("Exiting\n"); } int main_numargs; @@ -73,10 +75,10 @@ char ** main_args; * Main system function */ int main(int numargs, char ** args) { - /* Stash this stuff in case someone wants it eventually */ - main_numargs=numargs; - main_args=args; + /* Stash this stuff in case someone wants it eventually */ + main_numargs=numargs; + main_args=args; - /* Let's jump in quickly and start running stuff */ - initSnapShotLibrary(10000 /*int numbackingpages*/, 1024 /*unsigned int numsnapshots*/, 1024 /*unsigned int nummemoryregions*/ , 1000 /*int numheappages*/, &real_main /*MyFuncPtr entryPoint*/); + /* Let's jump in quickly and start running stuff */ + initSnapShotLibrary(10000 /*int numbackingpages*/, 1024 /*unsigned int numsnapshots*/, 1024 /*unsigned int nummemoryregions*/ , 1000 /*int numheappages*/, &real_main /*MyFuncPtr entryPoint*/); }