X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=main.cc;h=a400fe3c2defff0eafc93e812b005f6b2b6fcf69;hp=e8a2b3317dc4ebedc235735fef32d272259d4215;hb=2cb7ca6d0aa997474b63f240c165e1a941cf6124;hpb=ca4375ba4697b8abe476e03f211523c491c3e2c3 diff --git a/main.cc b/main.cc index e8a2b331..a400fe3c 100644 --- a/main.cc +++ b/main.cc @@ -1,14 +1,22 @@ +/** @file main.cc + * @brief Entry point for the model checker. + */ + #include "libthreads.h" #include "common.h" #include "threads.h" +#include "datarace.h" + /* global "model" object */ #include "model.h" #include "snapshot-interface.h" -/* - * Return 1 if found next thread, 0 otherwise +/** The thread_system_next function takes the next step in the + * execution. @return Returns the 1 if there is another step and 0 + * otherwise. */ + static int thread_system_next(void) { Thread *curr, *next; @@ -32,15 +40,24 @@ static int thread_system_next(void) { return Thread::swap(model->get_system_context(), next); } +/** The thread_wait_finish method runs the current execution until we + * have no more steps to take. + */ + static void thread_wait_finish(void) { DBG(); while (!thread_system_next()); } + +/** The real_main function contains the main model checking loop. */ + void real_main() { thrd_t user_thread; ucontext_t main_context; + //Initialize race detector + initRaceDetector(); //Create the singleton SnapshotStack object snapshotObject = new SnapshotStack(); @@ -70,8 +87,9 @@ void real_main() { int main_numargs; char ** main_args; -/* - * Main system function +/** + * Main function. Just initializes snapshotting library and the + * snapshotting library calls the real_main function. */ int main(int numargs, char ** args) { /* Stash this stuff in case someone wants it eventually */