rename snapshotStack -> SnapshotStack
[model-checker.git] / main.cc
1 #include "libthreads.h"
2 #include "common.h"
3 #include "threads.h"
4
5 /* global "model" object */
6 #include "model.h"
7 #include "snapshot.h"
8 #include "snapshot-interface.h"
9
10 /*
11  * Return 1 if found next thread, 0 otherwise
12  */
13 static int thread_system_next(void) {
14         Thread *curr, *next;
15
16         curr = thread_current();
17         if (curr) {
18                 if (curr->get_state() == THREAD_READY) {
19                         model->check_current_action();
20                         model->scheduler->add_thread(curr);
21                 } else if (curr->get_state() == THREAD_RUNNING)
22                         /* Stopped while running; i.e., completed */
23                         curr->complete();
24                 else
25                         ASSERT(false);
26         }
27         next = model->scheduler->next_thread();
28         if (next)
29                 next->set_state(THREAD_RUNNING);
30         DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
31         if (!next)
32                 return 1;
33         return Thread::swap(model->get_system_context(), next);
34 }
35
36 static void thread_wait_finish(void) {
37         DBG();
38
39         while (!thread_system_next());
40 }
41
42 void real_main() {
43         thrd_t user_thread;
44         ucontext_t main_context;
45
46         //Create the singleton SnapshotStack object
47         snapshotObject = new SnapshotStack();
48
49         model = new ModelChecker();
50
51         if (getcontext(&main_context))
52                 return;
53
54         model->set_system_context(&main_context);
55
56         snapshotObject->snapshotStep(0);
57
58         do {
59                 /* Start user program */
60                 model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
61
62                 /* Wait for all threads to complete */
63                 thread_wait_finish();
64         } while (model->next_execution());
65
66         delete model;
67
68         DEBUG("Exiting\n");
69 }
70
71 int main_numargs;
72 char ** main_args;
73
74 /*
75  * Main system function
76  */
77 int main(int numargs, char ** args) {
78         /* Stash this stuff in case someone wants it eventually */
79         main_numargs=numargs;
80         main_args=args;
81
82         /* Let's jump in quickly and start running stuff */
83         initSnapShotLibrary(10000, 1024, 1024, 1000, &real_main);
84 }