Mercurial > hg > CbC > old > DPP

comparison tableau2.cbc @ 0:d4bc23cb728b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Import from CVS (CVS_DB/member/atsuki/cbc/DPP)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 16 Dec 2015 15:16:11 +0900
parents
children 171cc032eb29
comparison
equal deleted inserted replaced
-1:000000000000 0:d4bc23cb728b
1 /*
2 ** Dining Philosophers Problem's scheduler
3 ** with state developper as a tableau method
4
5 ** 連絡先： 琉球大学情報工学科 河野 真治
6 ** （E-Mail Address: kono@ie.u-ryukyu.ac.jp）
7 **
8 ** このソースのいかなる複写，改変，修正も許諾します。ただし、
9 ** その際には、誰が貢献したを示すこの部分を残すこと。
10 ** 再配布や雑誌の付録などの問い合わせも必要ありません。
11 ** 営利利用も上記に反しない範囲で許可します。
12 ** バイナリの配布の際にはversion messageを保存することを条件とします。
13 ** このプログラムについては特に何の保証もしない、悪しからず。
14 **
15 ** Everyone is permitted to do anything on this program
16 ** including copying, modifying, improving,
17 ** as long as you don't try to pretend that you wrote it.
18 ** i.e., the above copyright notice has to appear in all copies.
19 ** Binary distribution requires original version messages.
20 ** You don't have to ask before copying, redistribution or publishing.
21 ** THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE.
22
23 */
24 #include <stdlib.h>
25 #include <time.h>
26 #include "dpp2.h"
27 #include "queue.h"
28 #include "memory.h"
29 #include "state_db.h"
30 #include "ltl.h"
31
32 int NUM_PHILOSOPHER = 5; /* A number of philosophers must be more than 2. */
33
34 static code (*ret)(int);
35 static void *env;
36
37 static PhilsPtr phils_list = NULL;
38
39 static int max_step = 100;
40
41 static StateDB state_db;
42 static MemoryPtr mem;
43 static StateNode st;
44 static int always_flag; // for LTL
45
46 int
47 list_length(TaskPtr list)
48 {
49 int length;
50 TaskPtr t;
51
52 if (!list) return 0;
53 t = list->next;
54
55 for (length = 1; t && t != list; length++) {
56 t = t->next;
57 }
58 return length;
59 }
60
61 TaskPtr
62 get_task(int num, TaskPtr list)
63 {
64 while (num-- > 0) {
65 list = list->next;
66 }
67 return list;
68 }
69
70
71 static TaskIteratorPtr task_iter;
72 static int depth,count;
73
74 /*
75 Performe depth frist search
76 Possible task iterleave is generated by TaskIterator
77 (using task ring)
78 State are recorded in StateDB
79 all memory fragments are regsitered by add_memory_range()
80 including task queue
81 */
82
83
84 code tableau(TaskPtr list)
85 {
86 StateDB out;
87
88 st.hash = get_memory_hash(mem,0);
89 if (lookup_StateDB(&st, &state_db, &out)) {
90 // found in the state database
91 //printf("found %d\n",count);
92 while(!(list = next_task_iterator(task_iter))) {
93 // no more branch, go back to the previous one
94 TaskIteratorPtr prev_iter = task_iter->prev;
95 if (!prev_iter) {
96 printf("All done count %d\n",count);
97 memory_usage();
98 show_result(always_flag);
99 goto ret(0),env;
100 }
101 //printf("no more branch %d\n",count);
102 depth--;
103 free_task_iterator(task_iter);
104 task_iter = prev_iter;
105 }
106 // return to previous state
107 // here we assume task list is fixed, we don't have to
108 // recover task list itself
109 restore_memory(task_iter->state->memory);
110 //printf("restore list %x next %x\n",(int)list,(int)(list->next));
111 } else {
112 // one step further
113 depth++;
114 task_iter = create_task_iterator(list,out,task_iter);
115 }
116 //printf("depth %d count %d\n", depth, count++);
117 count++;
118 goto list->phils->next(list->phils,list);
119 }
120
121 code get_next_task_fifo(TaskPtr list)
122 {
123 TaskPtr t = list;
124 TaskPtr e;
125
126 if (max_step--<0) goto die("Simuration end.");
127
128 list = list->next;
129 goto list->phils->next(list->phils,list);
130 }
131
132 code scheduler(PhilsPtr phils, TaskPtr list)
133 {
134 goto check(&always_flag, phils, list);
135 // goto next_next_task_fifo(list);
136 }
137
138 code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last);
139
140 code task_entry2(int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q)
141 {
142 if (!q) {
143 goto die("Can't allocate Task\n");
144 } else {
145 add_memory_range(q,sizeof(Task),&mem);
146 goto enqueue(count, self, list, last, q, task_entry1);
147 }
148 }
149
150 code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last)
151 {
152 StateDB out;
153 /*
154 printf("int count %d, PhilsPtr self %x, TaskPtr list %x, TaskPtr last %x\n",
155 count, self, list, last);
156 */
157
158 if (count++ < NUM_PHILOSOPHER) {
159 self = self->left;
160 goto create_queue(count,self,list,last,task_entry2);
161 } else {
162 // make circular task list
163 last->next = list;
164 st.memory = mem;
165 st.hash = get_memory_hash(mem,0);
166 lookup_StateDB(&st, &state_db, &out);
167 task_iter = create_task_iterator(list,out,0);
168 // start first task
169 goto list->phils->next(list->phils,list);
170 }
171 }
172
173 code task_entry0(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q)
174 {
175 add_memory_range(q,sizeof(Task),&mem);
176 goto task_entry1(count, self, q, q);
177 }
178
179 code init_final(PhilsPtr self)
180 {
181 self->right = phils_list;
182 phils_list->left = self;
183 self->right_fork = phils_list->left_fork;
184 always_flag = 1;
185 //add_memory_range(&always_flag, sizeof(int), &mem);
186 //printf("init all\n");
187
188 goto create_queue(1, self, 0, 0, task_entry0);
189 }
190
191 code init_phils2(PhilsPtr self, int count, int id)
192 {
193 PhilsPtr tmp_self;
194
195 tmp_self = (PhilsPtr)malloc(sizeof(Phils));
196 if (!tmp_self) {
197 goto die("Can't allocate Phils\n");
198 }
199 self->right = tmp_self;
200 tmp_self->id = id;
201 tmp_self->right_fork = NULL;
202 tmp_self->left_fork = self->right_fork;
203 tmp_self->right = NULL;
204 tmp_self->left = self;
205 tmp_self->next = thinking;
206 add_memory_range(tmp_self,sizeof(Phils),&mem);
207
208 count--;
209 id++;
210
211 if (count == 0) {
212 goto init_final(tmp_self);
213 } else {
214 goto init_fork2(tmp_self, count, id);
215 }
216 }
217
218 code init_fork2(PhilsPtr self, int count, int id)
219 {
220 ForkPtr tmp_fork;
221
222 tmp_fork = (ForkPtr)malloc(sizeof(Fork));
223 if (!tmp_fork) {
224 goto die("Can't allocate Fork\n");
225 }
226 tmp_fork->id = id;
227 tmp_fork->owner = NULL;
228 self->right_fork = tmp_fork;
229 add_memory_range(tmp_fork,sizeof(Fork),&mem);
230
231 goto init_phils2(self, count, id);
232 }
233
234 code init_phils1(ForkPtr fork, int count, int id)
235 {
236 PhilsPtr self;
237
238 self = (PhilsPtr)malloc(sizeof(Phils));
239 if (!self) {
240 goto die("Can't allocate Phils\n");
241 }
242 phils_list = self;
243 self->id = id;
244 self->right_fork = NULL;
245 self->left_fork = fork;
246 self->right = NULL;
247 self->left = NULL;
248 self->next = thinking;
249 add_memory_range(self,sizeof(Phils),&mem);
250
251 count--;
252 id++;
253
254 goto init_fork2(self, count, id);
255 }
256
257 code init_fork1(int count)
258 {
259 ForkPtr fork;
260 int id = 1;
261
262 fork = (ForkPtr)malloc(sizeof(Fork));
263 if (!fork) {
264 goto die("Can't allocate Fork\n");
265 }
266 fork->id = id;
267 fork->owner = NULL;
268 add_memory_range(fork,sizeof(Fork),&mem);
269
270 goto init_phils1(fork, count, id);
271 }
272
273 code die(char *err)
274 {
275 printf("%s\n", err);
276 goto ret(1), env;
277 }
278
279 int main(int ac, char *av[])
280 {
281 ret = return;
282 env = environment;
283 // srand((unsigned)time(NULL));
284 // srandom((unsigned long)time(NULL));
285 srandom(555);
286
287 if (ac==2) {
288 NUM_PHILOSOPHER = atoi(av[1]);
289 if (NUM_PHILOSOPHER >10 ||NUM_PHILOSOPHER < 2) {
290 printf("illegal number of philosopher = %d\n", NUM_PHILOSOPHER );
291 return 1;
292 }
293 printf("number of philosopher = %d\n", NUM_PHILOSOPHER );
294 }
295
296 goto init_fork1(NUM_PHILOSOPHER);
297 }
298
299 /* end */