fix this stuff...
[model-checker.git] / main.cc
1 #include <stdlib.h>
2
3 #include "libthreads.h"
4 #include "schedule.h"
5 #include "common.h"
6 #include "threads.h"
7
8 /* global "model" object */
9 #include "model.h"
10
11 /*
12  * Return 1 if found next thread, 0 otherwise
13  */
14 int num;
15 int num1;
16 int num2;
17
18 static int thread_system_next(void)
19 {
20         Thread *curr, *next;
21
22         curr = thread_current();
23         if (curr) {
24                 if (curr->get_state() == THREAD_READY) {
25                         model->check_current_action();
26                         model->scheduler->add_thread(curr);
27                 } else if (curr->get_state() == THREAD_RUNNING)
28                         /* Stopped while running; i.e., completed */
29                         curr->complete();
30                 else
31                         ASSERT(false);
32         }
33         next = model->scheduler->next_thread();
34         if (next)
35                 next->set_state(THREAD_RUNNING);
36         DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
37         if (!next)
38                 return 1;
39         return Thread::swap(model->get_system_context(), next);
40 }
41
42 static void thread_wait_finish(void)
43 {
44
45         DBG();
46
47         while (!thread_system_next());
48 }
49
50 /*
51  * Main system function
52  */
53 int main()
54 {
55         thrd_t user_thread;
56         ucontext_t main_context;
57
58         model = new ModelChecker();
59
60         if (getcontext(&main_context))
61                 return 1;
62
63         model->set_system_context(&main_context);
64
65         do {
66                 /* Start user program */
67                 model->add_thread(new Thread(&user_thread, &user_main, NULL));
68
69                 /* Wait for all threads to complete */
70                 thread_wait_finish();
71         } while (model->next_execution());
72
73         delete model;
74
75         DEBUG("Exiting\n");
76         return 0;
77 }