X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=8db63e6d1733d1204e9855575c49d06dafc6d9a6;hb=5b22024b3c5e054ed1861e90b47f28c5698fb3e1;hp=9af745d4280d865dab0c350a306e3594640a4968;hpb=02792abf9399d1dca2fab7bc511f09e934d05f1d;p=model-checker.git diff --git a/main.cc b/main.cc index 9af745d..8db63e6 100644 --- a/main.cc +++ b/main.cc @@ -1,22 +1,16 @@ -#include - #include "libthreads.h" -#include "schedule.h" #include "common.h" #include "threads.h" /* global "model" object */ #include "model.h" +#include "snapshot.h" +#include "snapshot-interface.h" /* * Return 1 if found next thread, 0 otherwise */ -int num; -int num1; -int num2; - -static int thread_system_next(void) -{ +static int thread_system_next(void) { Thread *curr, *next; curr = thread_current(); @@ -39,32 +33,31 @@ static int thread_system_next(void) return Thread::swap(model->get_system_context(), next); } -static void thread_wait_finish(void) -{ - +static void thread_wait_finish(void) { DBG(); while (!thread_system_next()); } -/* - * Main system function - */ -int main() -{ +void real_main() { thrd_t user_thread; ucontext_t main_context; + //Create the singleton snapshotStack object + snapshotObject = new snapshotStack(); + model = new ModelChecker(); if (getcontext(&main_context)) - return 1; + return; model->set_system_context(&main_context); + snapshotObject->snapshotStep(0); + do { /* Start user program */ - model->add_thread(new Thread(&user_thread, &user_main, NULL)); + model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL)); /* Wait for all threads to complete */ thread_wait_finish(); @@ -73,5 +66,19 @@ int main() delete model; DEBUG("Exiting\n"); - return 0; +} + +int main_numargs; +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; + + /* Let's jump in quickly and start running stuff */ + initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main); }