X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=main.cc;h=339b85efd45d427096546cbf8641d3afbb71067f;hp=8db63e6d1733d1204e9855575c49d06dafc6d9a6;hb=cf00814e3c709a8cceaa15ec9bb1fc0922213f4b;hpb=4224cb3a9afdac601fd2778253214e42f8b2fdf4 diff --git a/main.cc b/main.cc index 8db63e6d..339b85ef 100644 --- a/main.cc +++ b/main.cc @@ -1,14 +1,20 @@ +/** @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.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; @@ -33,18 +39,26 @@ 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()); } -void real_main() { + +/** The real_main function contains the main model checking loop. */ +static void real_main() { thrd_t user_thread; ucontext_t main_context; - //Create the singleton snapshotStack object - snapshotObject = new snapshotStack(); + //Initialize race detector + initRaceDetector(); + + //Create the singleton SnapshotStack object + snapshotObject = new SnapshotStack(); model = new ModelChecker(); @@ -71,8 +85,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 */