Mercurial > hg > CbC > old > DPP
changeset 0:d4bc23cb728b
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 | 2874954d97b2 |
| files | .hgignore Changes Makefile crc32.c crc32.h dpp.cbc dpp.h dpp2.cbc dpp2.h dpp3.cbc dpp3.h dpp_common.h ltl.cbc ltl.h main.cbc memory.c memory.h queue.cbc queue.h scheduler.cbc scheduler.h state_db.c state_db.h tableau.cbc tableau2.cbc tableau3.cbc test/memory_test.c test/state_test.c tools/depth-plot.sh |
| diffstat | 29 files changed, 2869 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/.hgignore Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,4 @@ +syntax: glob +CVS* +*.swp +*.o
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Changes Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,254 @@ +Sun Sep 10 08:19:53 JST 2006 + +あれ? cmp_memory1 では、アドレスを識別しているので、(comment とは +反対に...) アドレスが異なるメモリパターンはshare されてないね。 +こまったものだ。 + +copy_memory の呼び出す、memory_lookup を書き換えないとだめだな。 + +state.c/h は、必要ないみたいだな。 + +state 間のpointer を用意した方があとで実行させてみる時には +便利だろう。(実行って言うのかな? これは、なんだろう? trace +generation? ) + +Sun Sep 10 05:09:02 JST 2006 + +1.6MHz 17inch PowerBook Memory 1GB + ++leo+kono time ./tableau 8 > ers; tail ers +./tableau 8 > ers 237.58s user 12.92s system 79% cpu 5:16.63 total +found 3915727 +no more banch 3915727 +All done count 3915727 + memory_header 11747304 + memcmp_count 830530587 + memory_body 1792 + restore_count 82230288 + restore_size 1096403840 + range_count 24 + range_size 320 ++leo+kono time ./tableau 7 > ers; tail ers +./tableau 7 > ers 35.42s user 1.99s system 90% cpu 41.401 total +found 845529 +no more banch 845529 +All done count 845529 + memory_header 2536695 + memcmp_count 114942650 + memory_body 1568 + restore_count 15219540 + restore_size 202927200 + range_count 21 + range_size 280 ++leo+kono time ./tableau 6 > ers; tail ers +./tableau 6 > ers 5.04s user 0.32s system 97% cpu 5.514 total +found 159299 +no more banch 159299 +All done count 159299 + memory_header 477990 + memcmp_count 15198190 + memory_body 1344 + restore_count 2389500 + restore_size 31860000 + range_count 18 + range_size 240 ++leo+kono time ./tableau 5 > ers; tail ers +./tableau 5 > ers 1.04s user 0.08s system 96% cpu 1.154 total +no more banch 38984 +no more banch 38984 +All done count 38984 + memory_header 117030 + memcmp_count 2432088 + memory_body 1120 + restore_count 467820 + restore_size 6237600 + range_count 15 + range_size 200 + +Lite ( tableau on SICStus Prolog ) では、 + +208.57 sec. +1365 states +60 subterms +21075 state transions +renaming,singleton,length limit 5 + +なので、結構、いい値かな。つうか、知っていはいたが、Lite 遅すぎ。 +状態数が多いのは何故だろう? たぶん、code segment のtask のpointer +が細かすぎるのだろう... + +Sun Sep 10 02:45:16 JST 2006 + +Iterator を使えば、tableau 自体もそんなに難しくないか。 + +Sat Sep 9 23:25:42 JST 2006 + +あ、そうか。 + memory の部分木が同じなら、それもshareした方が良い +でも、そのためには、pattern だけでなく、adr/left/right も +含んだ形で share を行わないとダメ。 + +まぁ、とりあえず、全部copyってことで... + +copy_memory を、もっとintelligentにすればいいんだろうな... + +Sat Sep 9 22:15:10 JST 2006 + +range を登録して、そのrangeに対して、state を決める。 +それを look up するわけだけど、 + state, memory range for real address + state, memory range in database (as copy) +と二つあることになる。 + +実際に、code segement を実行して、すべてのmemory rangeを +lookup するのは、実はばかげてる。code segment で memory に +書き込んだときに、どこを書き込んだのか dirty list みたいな +形で持っておくべきでしょうね。 + +単にデータを圧縮するだけでなく、そのあたりを工夫しないと +速度的に厳しい。 + +code segment の実行も、同じパターンの実行だったら、二度は +行わないみたいな工夫が必要だと思う。それは、一種の理論に +なるんだろうけど... + +まぁ、とりあえずは、それはやらないけどさ。 + +memory range は、実際には増減することになる。malloc / free +した時にどうするかは、これからの課題だろう。 + +Sat Sep 9 19:16:10 JST 2006 + +memory_add は、いいんだけど、state DB のlookup で使う状態は、 +どうやって作るんだろう? + +間が開いているので、何やろうとしていたんだか、良くわからん。 + +memory_add は、状態に対して行うべきものなんじゃないの? + +たぶん、memory_add に相当するものは、 + state に対する address range の登録 + memory pattern の検索と登録 +の二種類があるんだと思われる。そのあたりを曖昧に作ってしまった +らしい。 + + +Sun Aug 6 15:23:05 JST 2006 + +tree をbaranceさせないとだめなのは、そうなんだけど、 +tree search routine も code segement で記述した方が +やっぱり良い。 + +main loop を書くのが面倒だが、あと、も少しなはずだが、 +今日中に終る自信はないね。 + +Binary Tree そのものが状態データベースになるわけなので、 +そこに安直なものを使うのはまずい。 + +Sat Aug 5 22:04:00 JST 2006 + +はぁ、だいぶ出来た。 + + MemoryPtr + add_memory(void *ptr,int length, MemoryPtr *parent) + +で、登録していくわけね。 + +test routine を書いていかないと。 + +Sat Aug 5 19:35:56 JST 2006 + +typedef struct memory { + void *adr; + int length; + void *body; + int crc; + struct memory *left,*right; +} Memory, *MemoryPtr; + +body と address をわけて、中身が同じなら、同じものを +さすようにする。ということは、crc でhashしないとだめ。 +crc じゃなくて hash か。 + +content hash で 2分木をつくって、さらに、adr/length pair +で2分木を作ればいいんじゃないか? そうすれば hash はいりません。 +バランスはさせないとまずいけど。 + +Sat Aug 5 17:45:26 JST 2006 + +state と state_db にわけるのか。 + +typedef struct memory { + void *ptr; + int length; + struct memory *next; +} Memory, *MemoryPtr; + +なんだが、binary tree にするべきかどうか。まぁ、するべきな +んだけど、そうすると、形がuniqueでなくなるのがまずい。正規 +形にならないの? まぁ、正規形でなくても、maximum share され +ていれば、文句はないんだけど。 + +大半のルーチンで、変更されるメモリはごく一部なはず。それを +効率的に捕まえるためには、compiler or program 変換で捕まえる +必要があるはず。(OSのサポートとか?) + +同じ形のメリットは同一性の判定の問題だけ。連続した領域とか +の同一性はどうする? MD5? MD5 はだめだな。 + +address が違うだけで、中身が同じ場合は共有するべきだろ? +だとすれば、中身はハッシュするべきだろう。 + +queue とかの場合の対称性は、abstrct()で正規形に変換してから +db に登録すれば良いわけなんだが、そこまでは間に合わないらしい。 +正規形の大半は、制御に影響しない(あるいはランダムに影響する) +データをzero clearすることになるはず。 + +まぁ、何か変だね。もう少し考えると、すっきりしたもの(ordered BDD +を含む)なにかが見つかるだろう。 + + |------| |------| + +という領域ではなくて、 + + |------xxxxxx------| + +という don't care を含むメモリ領域の正規化という問題だってこと? + +BDD は、 + |tfxxxxxfxtxxfffttt| +という文字列の正規化とみなせるわけだから... なんか、どっかで +見た問題だな。 + +Sat Jul 29 18:44:33 JST 2006 + +No compile errors. + +まぁ、走らせるのは簡単なんだが、状態の登録をどうする? + +malloc() した状態の登録をどうする? + +*同じ* pointer というのを識別する必要がある。 id で識別する? + +まぁ、最初は malloc しないでも良い。 + add_state(void *p,int length); +ぐらい。 + +同じ id (つまり、address )は、同じアドレスである必要があるが... +同じ大きさとは限らない。一番大きなものに合わせる? + +malloc を許すと、そもそも、止まるアルゴリズムにならないが... + +malloc() しても、中身の多様性を無視できる場合。 + add_state(void *p,int length, (*abstrct)(void *,int )); + +メモリreferece は、id で抽象化する必要がある。ということは、 +メモリ演算は、抽象化される必要がある。(移動をともなう場合) + +まぁ、とりあえず固定でやるしかないか。 + +つまり、最初のtablue 展開ルーチンに来るまでに、 +add_state は有限固定回起きるという話なわけね。 +しかも順序が固定というわけか。 + +/* epoch */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Makefile Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,128 @@ +CC=gcc +MCC=mcc +TARGET=dpp dpp2 tableau tableau2 tableau3 +MCCFLAGS=-s +CFLAGS=-I. -g -Wall + +.SUFFIXES: .cbc .c .o + +.cbc.o: + $(MCC) $(MCCFLAGS) $< + $(CC) $(CFLAGS) -o $@ -c $(<:.cbc=.s) + +all: $(TARGET) + +# single running +dpp: dpp.o main.o + $(CC) $(CFLAGS) -o $@ $^ + +# multiple running +dpp2: dpp2.o queue.o scheduler.o memory.o crc32.o + $(CC) $(CFLAGS) -o $@ $^ + +# tableau expansion +tableau: dpp2.o queue.o tableau.o memory.o state_db.o crc32.o + $(CC) $(CFLAGS) -o $@ $^ + +# tableau expansion with LTL +tableau2: dpp2.o queue.o ltl.o tableau2.o memory.o state_db.o crc32.o + $(CC) $(CFLAGS) -o $@ $^ + +# tableau expansion with LTL (reduced the number of states) +tableau3: dpp3.o queue.o ltl.o tableau3.o memory.o state_db.o crc32.o + $(CC) $(CFLAGS) -o $@ $^ + +# + +test: memory_test state_test + +memory_test: test/memory_test + test/memory_test +state_test: test/state_test + test/state_test + +test/memory_test: test/memory_test.o memory.o crc32.o + $(CC) $(CFLAGS) -I. $^ -o $@ +test/state_test: test/state_test.o memory.o state_db.o crc32.o + $(CC) $(CFLAGS) -I. $^ -o $@ + +clean: + $(RM) -f $(TARGET) + $(RM) -f *.s *.o + $(RM) -f test/*.s test/*.o test/state_test test/memory_test + + +depend: + makedepend *.cbc *.[hc] test/*.c + +# DO NOT DELETE + +dpp.o: dpp.h +dpp2.o: dpp2.h queue.h dpp.h state_db.h scheduler.h +main.o: dpp.h +queue.o: queue.h dpp.h state_db.h +scheduler.o: /usr/include/stdio.h /usr/include/features.h +scheduler.o: /usr/include/sys/cdefs.h /usr/include/bits/wordsize.h +scheduler.o: /usr/include/gnu/stubs.h /usr/include/gnu/stubs-32.h +scheduler.o: /usr/include/bits/types.h /usr/include/bits/typesizes.h +scheduler.o: /usr/include/libio.h /usr/include/_G_config.h +scheduler.o: /usr/include/wchar.h /usr/include/bits/wchar.h +scheduler.o: /usr/include/gconv.h /usr/include/bits/stdio_lim.h +scheduler.o: /usr/include/bits/sys_errlist.h /usr/include/stdlib.h +scheduler.o: /usr/include/sys/types.h /usr/include/time.h +scheduler.o: /usr/include/endian.h /usr/include/bits/endian.h +scheduler.o: /usr/include/sys/select.h /usr/include/bits/select.h +scheduler.o: /usr/include/bits/sigset.h /usr/include/bits/time.h +scheduler.o: /usr/include/sys/sysmacros.h /usr/include/bits/pthreadtypes.h +scheduler.o: /usr/include/alloca.h dpp2.h queue.h dpp.h state_db.h +tableau.o: /usr/include/stdlib.h /usr/include/features.h +tableau.o: /usr/include/sys/cdefs.h /usr/include/bits/wordsize.h +tableau.o: /usr/include/gnu/stubs.h /usr/include/gnu/stubs-32.h +tableau.o: /usr/include/sys/types.h /usr/include/bits/types.h +tableau.o: /usr/include/bits/typesizes.h /usr/include/time.h +tableau.o: /usr/include/endian.h /usr/include/bits/endian.h +tableau.o: /usr/include/sys/select.h /usr/include/bits/select.h +tableau.o: /usr/include/bits/sigset.h /usr/include/bits/time.h +tableau.o: /usr/include/sys/sysmacros.h /usr/include/bits/pthreadtypes.h +tableau.o: /usr/include/alloca.h dpp2.h queue.h dpp.h state_db.h memory.h +memory.o: /usr/include/stdio.h /usr/include/features.h +memory.o: /usr/include/sys/cdefs.h /usr/include/bits/wordsize.h +memory.o: /usr/include/gnu/stubs.h /usr/include/gnu/stubs-32.h +memory.o: /usr/include/bits/types.h /usr/include/bits/typesizes.h +memory.o: /usr/include/libio.h /usr/include/_G_config.h /usr/include/wchar.h +memory.o: /usr/include/bits/wchar.h /usr/include/gconv.h +memory.o: /usr/include/bits/stdio_lim.h /usr/include/bits/sys_errlist.h +memory.o: /usr/include/stdlib.h /usr/include/sys/types.h /usr/include/time.h +memory.o: /usr/include/endian.h /usr/include/bits/endian.h +memory.o: /usr/include/sys/select.h /usr/include/bits/select.h +memory.o: /usr/include/bits/sigset.h /usr/include/bits/time.h +memory.o: /usr/include/sys/sysmacros.h /usr/include/bits/pthreadtypes.h +memory.o: /usr/include/alloca.h memory.h crc32.h /usr/include/string.h +queue.o: dpp.h state_db.h +state_db.o: /usr/include/stdlib.h /usr/include/features.h +state_db.o: /usr/include/sys/cdefs.h /usr/include/bits/wordsize.h +state_db.o: /usr/include/gnu/stubs.h /usr/include/gnu/stubs-32.h +state_db.o: /usr/include/sys/types.h /usr/include/bits/types.h +state_db.o: /usr/include/bits/typesizes.h /usr/include/time.h +state_db.o: /usr/include/endian.h /usr/include/bits/endian.h +state_db.o: /usr/include/sys/select.h /usr/include/bits/select.h +state_db.o: /usr/include/bits/sigset.h /usr/include/bits/time.h +state_db.o: /usr/include/sys/sysmacros.h /usr/include/bits/pthreadtypes.h +state_db.o: /usr/include/alloca.h state_db.h memory.h +test/memory_test.o: /usr/include/stdio.h /usr/include/features.h +test/memory_test.o: /usr/include/sys/cdefs.h /usr/include/bits/wordsize.h +test/memory_test.o: /usr/include/gnu/stubs.h /usr/include/gnu/stubs-32.h +test/memory_test.o: /usr/include/bits/types.h /usr/include/bits/typesizes.h +test/memory_test.o: /usr/include/libio.h /usr/include/_G_config.h +test/memory_test.o: /usr/include/wchar.h /usr/include/bits/wchar.h +test/memory_test.o: /usr/include/gconv.h /usr/include/bits/stdio_lim.h +test/memory_test.o: /usr/include/bits/sys_errlist.h /usr/include/strings.h +test/memory_test.o: memory.h +test/state_test.o: /usr/include/stdio.h /usr/include/features.h +test/state_test.o: /usr/include/sys/cdefs.h /usr/include/bits/wordsize.h +test/state_test.o: /usr/include/gnu/stubs.h /usr/include/gnu/stubs-32.h +test/state_test.o: /usr/include/bits/types.h /usr/include/bits/typesizes.h +test/state_test.o: /usr/include/libio.h /usr/include/_G_config.h +test/state_test.o: /usr/include/wchar.h /usr/include/bits/wchar.h +test/state_test.o: /usr/include/gconv.h /usr/include/bits/stdio_lim.h +test/state_test.o: /usr/include/bits/sys_errlist.h memory.h state_db.h
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/crc32.c Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,80 @@ +/* + $Id: crc32.c,v 1.1.1.1 2007/03/06 06:34:39 atsuki Exp $ + Shinji KONO <kono@ie.u-ryukyu.ac.jp> + based on open source CRCtextDlg.cpp Richard A. Ellingson + + This is generated by Perl, do not edit this. Edit Perl script. + */ + +static unsigned crc32_table[256] = { + 0x00000000,0x04c11db7,0x09823b6e,0x0d4326d9,0x130476dc,0x17c56b6b, + 0x1a864db2,0x1e475005,0x2608edb8,0x22c9f00f,0x2f8ad6d6,0x2b4bcb61, + 0x350c9b64,0x31cd86d3,0x3c8ea00a,0x384fbdbd,0x4c11db70,0x48d0c6c7, + 0x4593e01e,0x4152fda9,0x5f15adac,0x5bd4b01b,0x569796c2,0x52568b75, + 0x6a1936c8,0x6ed82b7f,0x639b0da6,0x675a1011,0x791d4014,0x7ddc5da3, + 0x709f7b7a,0x745e66cd,0x9823b6e0,0x9ce2ab57,0x91a18d8e,0x95609039, + 0x8b27c03c,0x8fe6dd8b,0x82a5fb52,0x8664e6e5,0xbe2b5b58,0xbaea46ef, + 0xb7a96036,0xb3687d81,0xad2f2d84,0xa9ee3033,0xa4ad16ea,0xa06c0b5d, + 0xd4326d90,0xd0f37027,0xddb056fe,0xd9714b49,0xc7361b4c,0xc3f706fb, + 0xceb42022,0xca753d95,0xf23a8028,0xf6fb9d9f,0xfbb8bb46,0xff79a6f1, + 0xe13ef6f4,0xe5ffeb43,0xe8bccd9a,0xec7dd02d,0x34867077,0x30476dc0, + 0x3d044b19,0x39c556ae,0x278206ab,0x23431b1c,0x2e003dc5,0x2ac12072, + 0x128e9dcf,0x164f8078,0x1b0ca6a1,0x1fcdbb16,0x018aeb13,0x054bf6a4, + 0x0808d07d,0x0cc9cdca,0x7897ab07,0x7c56b6b0,0x71159069,0x75d48dde, + 0x6b93dddb,0x6f52c06c,0x6211e6b5,0x66d0fb02,0x5e9f46bf,0x5a5e5b08, + 0x571d7dd1,0x53dc6066,0x4d9b3063,0x495a2dd4,0x44190b0d,0x40d816ba, + 0xaca5c697,0xa864db20,0xa527fdf9,0xa1e6e04e,0xbfa1b04b,0xbb60adfc, + 0xb6238b25,0xb2e29692,0x8aad2b2f,0x8e6c3698,0x832f1041,0x87ee0df6, + 0x99a95df3,0x9d684044,0x902b669d,0x94ea7b2a,0xe0b41de7,0xe4750050, + 0xe9362689,0xedf73b3e,0xf3b06b3b,0xf771768c,0xfa325055,0xfef34de2, + 0xc6bcf05f,0xc27dede8,0xcf3ecb31,0xcbffd686,0xd5b88683,0xd1799b34, + 0xdc3abded,0xd8fba05a,0x690ce0ee,0x6dcdfd59,0x608edb80,0x644fc637, + 0x7a089632,0x7ec98b85,0x738aad5c,0x774bb0eb,0x4f040d56,0x4bc510e1, + 0x46863638,0x42472b8f,0x5c007b8a,0x58c1663d,0x558240e4,0x51435d53, + 0x251d3b9e,0x21dc2629,0x2c9f00f0,0x285e1d47,0x36194d42,0x32d850f5, + 0x3f9b762c,0x3b5a6b9b,0x0315d626,0x07d4cb91,0x0a97ed48,0x0e56f0ff, + 0x1011a0fa,0x14d0bd4d,0x19939b94,0x1d528623,0xf12f560e,0xf5ee4bb9, + 0xf8ad6d60,0xfc6c70d7,0xe22b20d2,0xe6ea3d65,0xeba91bbc,0xef68060b, + 0xd727bbb6,0xd3e6a601,0xdea580d8,0xda649d6f,0xc423cd6a,0xc0e2d0dd, + 0xcda1f604,0xc960ebb3,0xbd3e8d7e,0xb9ff90c9,0xb4bcb610,0xb07daba7, + 0xae3afba2,0xaafbe615,0xa7b8c0cc,0xa379dd7b,0x9b3660c6,0x9ff77d71, + 0x92b45ba8,0x9675461f,0x8832161a,0x8cf30bad,0x81b02d74,0x857130c3, + 0x5d8a9099,0x594b8d2e,0x5408abf7,0x50c9b640,0x4e8ee645,0x4a4ffbf2, + 0x470cdd2b,0x43cdc09c,0x7b827d21,0x7f436096,0x7200464f,0x76c15bf8, + 0x68860bfd,0x6c47164a,0x61043093,0x65c52d24,0x119b4be9,0x155a565e, + 0x18197087,0x1cd86d30,0x029f3d35,0x065e2082,0x0b1d065b,0x0fdc1bec, + 0x3793a651,0x3352bbe6,0x3e119d3f,0x3ad08088,0x2497d08d,0x2056cd3a, + 0x2d15ebe3,0x29d4f654,0xc5a92679,0xc1683bce,0xcc2b1d17,0xc8ea00a0, + 0xd6ad50a5,0xd26c4d12,0xdf2f6bcb,0xdbee767c,0xe3a1cbc1,0xe760d676, + 0xea23f0af,0xeee2ed18,0xf0a5bd1d,0xf464a0aa,0xf9278673,0xfde69bc4, + 0x89b8fd09,0x8d79e0be,0x803ac667,0x84fbdbd0,0x9abc8bd5,0x9e7d9662, + 0x933eb0bb,0x97ffad0c,0xafb010b1,0xab710d06,0xa6322bdf,0xa2f33668, + 0xbcb4666d,0xb8757bda,0xb5365d03,0xb1f740b4 +}; + + + +// Once the lookup table has been filled in by the two functions above, +// this function creates all CRCs using only the lookup table. + +int Get_CRC(unsigned char *buffer,int len) +{ + // Be sure to use unsigned variables, + // because negative values introduce high bits + // where zero bits are required. + // Start out with all bits set high. + + unsigned ulCRC = 0xffffffff; + + // Perform the algorithm on each character + // in the string, using the lookup table values. + + while(len-->0) { + ulCRC = (ulCRC >> 8) ^ crc32_table[(ulCRC & 0xFF) ^ *buffer++]; + } + // Exclusive OR the result with the beginning value. + return ulCRC ^ 0xffffffff; +} + +// ******* End custom code ******* +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/crc32.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,8 @@ +/* + $Id: crc32.h,v 1.1.1.1 2007/03/06 06:34:39 atsuki Exp $ + Shinji KONO <kono@ie.u-ryukyu.ac.jp> + based on open source + */ + +extern int Get_CRC(unsigned char *buffer,int len); +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,69 @@ +/* +** Program: Dining Philosophors Problem +** Author : Atsuki Shimoji +** Note : This is a single running program. +*/ + +#include "dpp.h" + +code putdown_lfork(PhilsPtr self) +{ + printf("%d: putdown_lfork:%d\n", self->id, self->left_fork->id); + self->left_fork->owner = NULL; + goto thinking(self); +} + +code putdown_rfork(PhilsPtr self) +{ + printf("%d: putdown_rfork:%d\n", self->id, self->right_fork->id); + self->right_fork->owner = NULL; + goto putdown_lfork(self); +} + +code eating(PhilsPtr self) +{ + printf("%d: eating\n", self->id); + goto putdown_rfork(self); +} + +/* waiting for right fork */ +code hungry2(PhilsPtr self) +{ + printf("%d: hungry2\n", self->id); + goto pickup_rfork(self); +} + +/* waiting for left fork */ +code hungry1(PhilsPtr self) +{ + printf("%d: hungry1\n", self->id); + goto pickup_lfork(self); +} + +code pickup_rfork(PhilsPtr self) +{ + if (self->right_fork->owner == NULL) { + printf("%d: pickup_rfork:%d\n", self->id, self->right_fork->id); + self->right_fork->owner = self; + goto eating(self); + } else { + goto hungry2(self); + } +} + +code pickup_lfork(PhilsPtr self) +{ + if (self->left_fork->owner == NULL) { + printf("%d: pickup_lfork:%d\n", self->id, self->left_fork->id); + self->left_fork->owner = self; + goto pickup_rfork(self); + } else { + goto hungry1(self); + } +} + +code thinking(PhilsPtr self) +{ + printf("%d: thinking\n", self->id); + goto hungry1(self); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,16 @@ +#ifndef _DPP_H_ +#define _DPP_H_ +#define NULL (0) + +#include "dpp_common.h" + +extern code putdown_lfork(PhilsPtr self); +extern code putdown_rfork(PhilsPtr self); +extern code eating(PhilsPtr self); +extern code hungry2(PhilsPtr self); +extern code hungry1(PhilsPtr self); +extern code pickup_rfork(PhilsPtr self); +extern code pickup_lfork(PhilsPtr self); +extern code thinking(PhilsPtr self); + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp2.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,82 @@ +/* +** Program: Dining Philosophors Problem +** Author : Atsuki Shimoji +*/ + +#include "dpp2.h" +#include "queue.h" +#include "scheduler.h" + +code putdown_lfork(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: putdown_lfork:%d\n", self->id, self->left_fork->id); + self->left_fork->owner = NULL; + self->next = thinking; + goto scheduler(self, current_task); +} + +code putdown_rfork(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: putdown_rfork:%d\n", self->id, self->right_fork->id); + self->right_fork->owner = NULL; + self->next = putdown_lfork; + goto scheduler(self, current_task); +} + +code eating(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: eating\n", self->id); + self->next = putdown_rfork; + goto scheduler(self, current_task); +} + +/* waiting for right fork */ +code hungry2(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: hungry2\n", self->id); + self->next = pickup_rfork; + goto scheduler(self, current_task); +} + +/* waiting for left fork */ +code hungry1(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: hungry1\n", self->id); + self->next = pickup_lfork; + goto scheduler(self, current_task); +} + +code pickup_rfork(PhilsPtr self, TaskPtr current_task) +{ + if (self->right_fork->owner == NULL) { + //printf("%d: pickup_rfork:%d\n", self->id, self->right_fork->id); + self->right_fork->owner = self; + self->next = eating; + goto scheduler(self, current_task); + } else { + self->next = hungry2; + goto scheduler(self, current_task); + } +} + +code pickup_lfork(PhilsPtr self, TaskPtr current_task) +{ + if (self->left_fork->owner == NULL) { + //printf("%d: pickup_lfork:%d\n", self->id, self->left_fork->id); + self->left_fork->owner = self; + self->next = pickup_rfork; + goto scheduler(self, current_task); + } else { + self->next = hungry1; + goto scheduler(self, current_task); + } +} + +code thinking(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: thinking\n", self->id); + self->next = hungry1; + goto scheduler(self, current_task); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp2.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,16 @@ +#ifndef _DPP2_H_ +#define _DPP2_H_ +#define NULL (0) + +#include "dpp_common.h" + +extern code putdown_lfork(PhilsPtr self, struct task * current_task); +extern code putdown_rfork(PhilsPtr self, struct task * current_task); +extern code eating(PhilsPtr self, struct task * current_task); +extern code hungry2(PhilsPtr self, struct task * current_task); +extern code hungry1(PhilsPtr self, struct task * current_task); +extern code pickup_rfork(PhilsPtr self, struct task * current_task); +extern code pickup_lfork(PhilsPtr self, struct task * current_task); +extern code thinking(PhilsPtr self, struct task * current_task); + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp3.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,61 @@ +/* +** Program: Dining Philosophors Problem +** Author : Atsuki Shimoji +*/ + +#include "dpp3.h" +#include "queue.h" + +__code putdown_fork(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: putdown_lfork:%d\n", self->id, self->left_fork->id); + self->right_fork->owner = NULL; + self->left_fork->owner = NULL; + self->next = pickup_lfork; + goto scheduler(self, current_task); +} + +/* +__code putdown_lfork(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: putdown_lfork:%d\n", self->id, self->left_fork->id); + self->left_fork->owner = NULL; + self->next = pickup_lfork; + goto scheduler(self, current_task); +} + +__code putdown_rfork(PhilsPtr self, TaskPtr current_task) +{ + //printf("%d: putdown_rfork:%d\n", self->id, self->right_fork->id); + self->right_fork->owner = NULL; + self->next = putdown_lfork; + goto scheduler(self, current_task); +} +*/ + +__code pickup_rfork(PhilsPtr self, TaskPtr current_task) +{ + if (self->right_fork->owner == NULL) { + //printf("%d: pickup_rfork:%d\n", self->id, self->right_fork->id); + self->right_fork->owner = self; + self->next = putdown_fork; + goto scheduler(self, current_task); + } else { + self->next = pickup_rfork; + goto scheduler(self, current_task); + } +} + +__code pickup_lfork(PhilsPtr self, TaskPtr current_task) +{ + if (self->left_fork->owner == NULL) { + //printf("%d: pickup_lfork:%d\n", self->id, self->left_fork->id); + self->left_fork->owner = self; + self->next = pickup_rfork; + goto scheduler(self, current_task); + } else { + self->next = pickup_lfork; + goto scheduler(self, current_task); + } +} +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp3.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,12 @@ +#ifndef _DPP3_H_ +#define _DPP3_H_ +#define NULL (0) + +#include "dpp_common.h" + +extern __code putdown_lfork(PhilsPtr self, struct task * current_task); +extern __code putdown_rfork(PhilsPtr self, struct task * current_task); +extern __code pickup_rfork(PhilsPtr self, struct task * current_task); +extern __code pickup_lfork(PhilsPtr self, struct task * current_task); + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/dpp_common.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,19 @@ +#ifndef _DPP_COMMON_H_ +#define _DPP_COMMON_H_ +#define NULL (0) + +typedef struct phils { + int id; + struct fork *right_fork; + struct fork *left_fork; + struct phils *right; + struct phils *left; + code (*next)(struct phils *, struct task *); +} Phils, *PhilsPtr; + +typedef struct fork { + int id; + struct phils *owner; +} Fork, *ForkPtr; + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ltl.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,35 @@ +#include <stdio.h> +#include "queue.h" +#include "dpp_common.h" + +static int +p(PhilsPtr phils) +{ + PhilsPtr current = phils; + PhilsPtr last = phils->left; + + if (last->left_fork->owner == NULL) return 0; + while (current != last) { + if (current->left_fork->owner == NULL) return 0; + current = current->right; + } + return 1; +} + +code check(int *always_flag, PhilsPtr phils, TaskPtr list) +{ + if (p(list->phils)) { + *always_flag = 0; + } + goto tableau(list); +} + +void +show_result(int always_flag) +{ + if (always_flag == 1) { + printf("[]~p is valid.\n"); + } else { + printf("[]~p is not valid.\n"); + } +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ltl.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,10 @@ +#ifndef _LTL_H_ +#define _LTL_H_ + +extern code +check(int *always_flag, struct phils *phils, struct task *list); + +extern void +show_result(int always_flag); + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/main.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,119 @@ +/* +** Dining Philosophers Problem's scheduler +*/ +#include "dpp.h" + +#define NUM_PHILOSOPHER 5 /* A number of philosophers must be more than 2. */ + +code (*ret)(int); +void *env; + +PhilsPtr phils_list = NULL; + +code run(PhilsPtr self) +{ + goto thinking(self); +} + +code init_final(PhilsPtr self) +{ + self->right = phils_list; + self->right_fork = phils_list->left_fork; + printf("init all\n"); + + goto run(phils_list); +} + +code init_phils2(PhilsPtr self, int count, int id) +{ + PhilsPtr tmp_self; + + tmp_self = (PhilsPtr)malloc(sizeof(Phils)); + if (!tmp_self) { + goto die("Can't allocate Phils\n"); + } + self->right = tmp_self; + tmp_self->id = id; + tmp_self->right_fork = NULL; + tmp_self->left_fork = self->right_fork; + tmp_self->right = NULL; + tmp_self->left = self; + tmp_self->next = thinking; + + count--; + id++; + + if (count == 0) { + goto init_final(tmp_self); + } else { + goto init_fork2(tmp_self, count, id); + } +} + +code init_fork2(PhilsPtr self, int count, int id) +{ + ForkPtr tmp_fork; + + tmp_fork = (ForkPtr)malloc(sizeof(Fork)); + if (!tmp_fork) { + goto die("Can't allocate Fork\n"); + } + tmp_fork->id = id; + tmp_fork->owner = NULL; + self->right_fork = tmp_fork; + + goto init_phils2(self, count, id); +} + +code init_phils1(ForkPtr fork, int count, int id) +{ + PhilsPtr self; + + self = (PhilsPtr)malloc(sizeof(Phils)); + if (!self) { + goto die("Can't allocate Phils\n"); + } + phils_list = self; + self->id = id; + self->right_fork = NULL; + self->left_fork = fork; + self->right = NULL; + self->left = NULL; + self->next = thinking; + + count--; + id++; + + goto init_fork2(self, count, id); +} + +code init_fork1(int count) +{ + ForkPtr fork; + int id = 1; + + fork = (ForkPtr)malloc(sizeof(Fork)); + if (!fork) { + goto die("Can't allocate Fork\n"); + } + fork->id = id; + fork->owner = NULL; + + goto init_phils1(fork, count, id); +} + +code die(char *err) +{ + printf("%s\n", err); + goto ret(1), env; +} + +int main(void) +{ + ret = return; + env = environment; + + goto init_fork1(NUM_PHILOSOPHER); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/memory.c Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,359 @@ +/* + + memory fragment management library + + Shinji Kono (2006) + + usage: + + MemoryPtr db = 0; + add_memory(address,length,&db); + + memory pattern is copyied and stored in a binary tree in db. + All patterns are shared. + + memory pattern database (binary tree by pattern) + + + */ + +#include <stdio.h> +#include <stdlib.h> +#include "memory.h" +#include "crc32.h" +#include <string.h> + +#define MEMORY_REPORT 1 + +#if MEMORY_REPORT +int memory_header; +int memcmp_count; +int memory_body; +int restore_count; +int restore_size; +int range_count; +int range_size; +#endif + +extern void die_exit(char *); + +void +die_exit(char *msg) +{ + fprintf(stderr,"%s\n",msg); + exit(1); +} + +// static MemoryPtr memory_root; + + +/* + + make memory fragment as a part of the program state + + */ + +MemoryPtr +create_memory(void *adr, int length) +{ + MemoryPtr m = (MemoryPtr)malloc(sizeof(Memory)); + if (!m) die_exit("Cann't alloc memory list."); + m->left = m->right = 0; + m->length = length; + m->adr = m->body = adr; +#if MEMORY_REPORT + memory_header++; +#endif + return m; +} + +/* + + Compute hash value of a memory fragment + + */ + +void +compute_memory_hash1(MemoryPtr m) +{ + m->hash = Get_CRC((unsigned char *)m->adr,m->length); +} + +void +free_memory(MemoryPtr m) +{ + m->left = m->right = 0; + m->adr = m->body = 0; + free(m); +} + +/* + + Compare memory contents ( doesn't care about its address ) + + */ + +int +cmp_content(MemoryPtr a,MemoryPtr b) +{ + if (a->length != b->length) { + if (a->length > b->length) { + return 1; + } else { + return -1; + } + } + if (a->hash == b->hash) { +#if MEMORY_REPORT + memcmp_count ++; +#endif + return memcmp(a->body,b->body,a->length); + } else if (a->hash > b->hash) { + return 1; + } else { + return -1; + } +} + +/* + + Compare entire memory contents ( doesn't care about its address ) + + */ + +static int +cmp_memory1(MemoryPtr a,MemoryPtr b) +{ + int r; + if ((r=cmp_content(a,b))) return r; + + if (a->adr==b->adr) { + return 0; + } + return (a->adr > b->adr) ? 1 : -1; +} + +int +cmp_memory(MemoryPtr a,MemoryPtr b) +{ + int r; + while(1) { + if ((r=cmp_memory1(a,b))) return r; + if (a->left && b->left) { + if ((r=cmp_memory(a->left,b->left))) return r; + } else if (a->left || b->left) { + return (a->left > b->left)? 1 : -1; + } + if (a->right && b->right) { + a = a->right; b = b->right; + // recursive loop + } else if (a->right || b->right) { + return (a->right > b->right)? 1 : -1; + } else { + return 0; // singleton + } + } +} + +/* + Make a copy of real memory fragments + */ + +MemoryPtr +copy_memory1(MemoryPtr m) +{ + MemoryPtr new = create_memory(m->adr,m->length); + void *p = (void *)malloc(m->length); + if (!p) { + die_exit("can't alloc memory body"); + return 0; + } +#if MEMORY_REPORT + memory_body += m->length; +#endif + memcpy(p,m->adr,m->length); + m->body = new->body = p; // abondon original memory pattern + new->hash = m->hash; + return new; +} + +MemoryPtr +copy_memory(MemoryPtr m, MemoryPtr *db) +{ + MemoryPtr new, out; + if (!m) return m; + new = create_memory(m->adr,m->length); + new->hash = m->hash; + // look up is necessary to share its memory pattern + memory_lookup(new, db, copy_memory1, &out); + if (m->left) new->left = copy_memory(m->left, db); + if (m->right) new->right = copy_memory(m->right, db); + return new; +} + +/* + restore copied memory save to the original addresses + */ + +void +restore_memory(MemoryPtr m) +{ + while (m) { + memcpy(m->adr,m->body,m->length); +#if MEMORY_REPORT + restore_count ++; + restore_size += m->length; +#endif + if (m->left) restore_memory(m->left); + m = m->right; + } +} + + +/* + get hash for all memeory fragments + initial value of hash should be zero + */ + +int +get_memory_hash(MemoryPtr m, int hash) +{ + if (!m) return hash; + compute_memory_hash1(m); + if (m->left) hash = get_memory_hash(m->left, hash); + if (m->right) return get_memory_hash(m->right, hash); + return m->hash | hash; +} + +/* + add modified memory fragments to the pattern database + */ + +MemoryPtr +add_memory(void *ptr,int length, MemoryPtr *parent) +{ + Memory m, *out; + m.adr = m.body = ptr; + m.length = length; + m.left = m.right = 0; + compute_memory_hash1(&m); + + memory_lookup(&m, parent, copy_memory1, &out); + return out; +} + +int +memory_lookup(MemoryPtr m, MemoryPtr *parent, + MemoryPtr (*new_memory)(MemoryPtr), MemoryPtr *out) +{ + MemoryPtr db; + int r; + + while(1) { + db = *parent; + if (!db) { + /* not found */ + if (new_memory && out) { + db = new_memory(m); + db->left = db->right = 0; + *out = *parent = db; + } + return 0; + } + if(!(r = cmp_memory1(m,db))) { + /* bingo */ + if (out) { + *out = db; + } + return 1; + } else if (r>0) { + parent = &db->left; + } else if (r<0) { + parent = &db->right; + } + } + /* !NOT REACHED */ +} + +/* + memory range list management for state registration + this list points the real memory + */ + +MemoryPtr +add_memory_range(void *ptr,int length, MemoryPtr *parent) +{ + Memory m, *out; + m.adr = ptr; + m.length = length; + m.left = m.right = 0; + + memory_range_lookup(&m, parent, &out); + return out; +} + +static int +cmp_range(MemoryPtr a,MemoryPtr b) +{ + if (a->adr==b->adr) { + if (a->length != b->length) + die_exit("memory range inconsitency"); + return 0; + } + return (a->adr > b->adr) ? 1 : -1; +} + +int +memory_range_lookup(MemoryPtr m, MemoryPtr *parent, MemoryPtr *out) +{ + MemoryPtr db; + int r; + + while(1) { + db = *parent; + if (!db) { + /* not found */ + if (out) { + db = create_memory(m->adr, m->length); + *out = *parent = db; + } +#if MEMORY_REPORT + range_count++; + range_size+=m->length; +#endif + return 0; + } + if(!(r = cmp_range(m,db))) { + /* bingo (actually an error) */ + if (out) { + *out = db; + } + return 1; + } else if (r>0) { + parent = &db->left; + } else if (r<0) { + parent = &db->right; + } + } + /* !NOT REACHED */ +} + +/* + */ + +void +memory_usage() +{ +#if MEMORY_REPORT + printf(" memory_header %d\n",memory_header); + printf(" memcmp_count %d\n",memcmp_count); + printf(" memory_body %d\n",memory_body); + printf(" restore_count %d\n",restore_count); + printf(" restore_size %d\n",restore_size); + printf(" range_count %d\n",range_count); + printf(" range_size %d\n",range_size); +#endif +} + + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/memory.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,57 @@ +#ifndef _MEMORY_H_ +#define _MEMORY_H_ + + +typedef struct memory { + void *adr; + int length; + void *body; + int hash; + struct memory *left,*right; +} Memory, *MemoryPtr; + +extern void die_exit(char *); + +extern MemoryPtr +create_memory(void *adr, int length); + +extern void +compute_memory_hash1(MemoryPtr m); + +extern void +free_memory(MemoryPtr m); + +extern int +cmp_content(MemoryPtr a,MemoryPtr b); + +extern int +cmp_memory(MemoryPtr a,MemoryPtr b); + +extern MemoryPtr +copy_memory(MemoryPtr m, MemoryPtr *db); + +extern void +restore_memory(MemoryPtr m) ; + +extern int +get_memory_hash(MemoryPtr m, int hash); + +MemoryPtr +add_memory(void *ptr,int length, MemoryPtr *parent); + +extern int +memory_lookup(MemoryPtr m, MemoryPtr *parent, + MemoryPtr (*new_memory)(MemoryPtr), MemoryPtr *out); + +extern MemoryPtr +add_memory_range(void *ptr,int length, MemoryPtr *parent); + +extern int +memory_range_lookup(MemoryPtr m, MemoryPtr *parent, MemoryPtr *out); + +extern void +memory_usage(); + + +#endif +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/queue.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,117 @@ +/* + OS Scheduler Simulator + +** 連絡先： 琉球大学情報工学科 河野 真治 +** （E-Mail Address: kono@ie.u-ryukyu.ac.jp） +** +** このソースのいかなる複写，改変，修正も許諾します。ただし、 +** その際には、誰が貢献したを示すこの部分を残すこと。 +** 再配布や雑誌の付録などの問い合わせも必要ありません。 +** 営利利用も上記に反しない範囲で許可します。 +** バイナリの配布の際にはversion messageを保存することを条件とします。 +** このプログラムについては特に何の保証もしない、悪しからず。 +** +** Everyone is permitted to do anything on this program +** including copying, modifying, improving, +** as long as you don't try to pretend that you wrote it. +** i.e., the above copyright notice has to appear in all copies. +** Binary distribution requires original version messages. +** You don't have to ask before copying, redistribution or publishing. +** THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE. + + Task Queue Manager + +** modify: Atsuki Shimoji(atsuki@cr.ie.u-ryukyu.ac.jp) + + */ +#include "queue.h" + +code create_queue(int count, PhilsPtr self, TaskPtr list, TaskPtr last, + code (*dest)( + int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q + )) +{ + TaskPtr q; + q = (TaskPtr)malloc(sizeof(Task)); + if (q) { + q->next = NULL; + q->phils = self; + } + goto dest(count, self, list, last, q); /* dest(TaskPtr new_queue) */ +} + +void +free_queue(TaskPtr q) +{ + free(q); +} + +code lastSearch(code (*dest)(), TaskPtr list, TaskPtr p, TaskPtr q) +{ + if (p->next) { + p = p->next; + goto lastSearch(dest, list, p, q); + } else { + p->next = q; + goto dest(list); /* dest(TaskPtr appended_queue) */ + } +} + +code enqueue(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q, + code (*dest)( + int count, PhilsPtr self, TaskPtr list, TaskPtr last + )) +{ + q->next = list; + goto dest(count,self,q, last); +} + +code dequeue(code (*dest)(), TaskPtr list) +{ + TaskPtr p = list; + if (p) { + list = list->next; + p->next = 0; + goto dest(p, list); /* dest(TaskPtr out, TaskPtr queue) */ + } + goto dest(p, list); /* dest(TaskPtr out, TaskPtr queue) */ +} + +TaskIteratorPtr +create_task_iterator(TaskPtr list,StateDB s,TaskIteratorPtr prev) +{ + TaskIteratorPtr new = (TaskIteratorPtr)malloc(sizeof(TaskIterator)); + if (!new) die_exit("can't allocate task iterlator"); + + new->prev = prev; + new->state = s; + new->list = list; + new->last = list; + return new; +} + +TaskPtr +next_task_iterator(TaskIteratorPtr self) +{ + TaskPtr next; + if (!self->list) { + die_exit("task iterator inconsistency"); + } + next = self->list->next; + if (!next) { + die_exit("task iterator next inconsistency"); + } + if (next == self->last) { + return 0; + } + self->list = next; + return next; +} + +void +free_task_iterator(TaskIteratorPtr iter) +{ + free(iter); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/queue.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,68 @@ +/* + OS Scheduler Simulator + +** 連絡先： 琉球大学情報工学科 河野 真治 +** （E-Mail Address: kono@ie.u-ryukyu.ac.jp） +** +** このソースのいかなる複写，改変，修正も許諾します。ただし、 +** その際には、誰が貢献したを示すこの部分を残すこと。 +** 再配布や雑誌の付録などの問い合わせも必要ありません。 +** 営利利用も上記に反しない範囲で許可します。 +** バイナリの配布の際にはversion messageを保存することを条件とします。 +** このプログラムについては特に何の保証もしない、悪しからず。 +** +** Everyone is permitted to do anything on this program +** including copying, modifying, improving, +** as long as you don't try to pretend that you wrote it. +** i.e., the above copyright notice has to appear in all copies. +** Binary distribution requires original version messages. +** You don't have to ask before copying, redistribution or publishing. +** THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE. + + Task Queue Manager + +** modify: Atsuki Shimoji(atsuki@cr.ie.u-ryukyu.ac.jp) + + */ +#ifndef _QUEUE_H_ +#define _QUEUE_H_ +#include "dpp_common.h" +#include "state_db.h" + +typedef struct task { + struct task *next; + struct phils *phils; +} Task, *TaskPtr; + +typedef struct task_iterator { + struct task_iterator *prev; + StateDB state; + TaskPtr list; + TaskPtr last; +} TaskIterator, *TaskIteratorPtr; + +extern TaskIteratorPtr +create_task_iterator(TaskPtr list,struct state *s,TaskIteratorPtr prev); + +extern TaskPtr +next_task_iterator(TaskIteratorPtr self); + +extern void +free_task_iterator(TaskIteratorPtr iter); + +extern +code create_queue(int count, PhilsPtr self, TaskPtr list, TaskPtr last, + code (*dest)( + int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q + )); +extern +code enqueue(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q, + code (*dest)( + int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q, + )); + + +extern void free_queue(TaskPtr q); +extern code dequeue(code (*dest)(), TaskPtr list, TaskPtr *q); + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/scheduler.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,217 @@ +/* +** Dining Philosophers Problem's scheduler +*/ +#include <stdio.h> +#include <stdlib.h> +#include <time.h> +#include "dpp2.h" +#include "queue.h" + +#define NUM_PHILOSOPHER 5 /* A number of philosophers must be more than 2. */ + +code (*ret)(int); +void *env; + +code (*get_next_task)(TaskPtr); +PhilsPtr phils_list = NULL; +int id = 1; /* This is a counter variable to detect a process. */ + +static int max_step = 100; + +/* 環状リストでもlengthを返す */ +int list_length(TaskPtr list) +{ + int length; + TaskPtr q; + if (!list) return 0; + q = list->next; + + for (length = 1; q && q != list; length++) { + q = q->next; + } + return length; +} + +TaskPtr get_task(int num, TaskPtr list) +{ + while (num-- > 0) { + list = list->next; + } + return list; +} + +code get_next_task_random(TaskPtr list) +{ + TaskPtr t = list; + TaskPtr e; + + if (max_step--<0) goto die("Simuration end."); + + // list = list->next; + list = get_task((random()%list_length(list)+1), list); + goto list->phils->next(list->phils,list); +} + +code get_next_task_fifo(TaskPtr list) +{ + TaskPtr t = list; + TaskPtr e; + + if (max_step--<0) goto die("Simuration end."); + + list = list->next; + goto list->phils->next(list->phils,list); +} + +code scheduler(PhilsPtr phils, TaskPtr list) +{ + goto get_next_task(list); +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last); + +code task_entry2(int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q) +{ + if (!q) { + goto die("Can't allocate Task\n"); + } else { + goto enqueue(count, self, list, last, q, task_entry1); + } +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last) +{ +printf("int count %d, PhilsPtr self %x, TaskPtr list %x, TaskPtr last %x\n", +count, self, list, last); + + if (count++ < NUM_PHILOSOPHER) { + self = self->left; + goto create_queue(count,self,list,last,task_entry2); + } else { + last->next = list; + goto scheduler(list->phils,list); + } +} + +code task_entry0(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q) +{ + goto task_entry1(count, self, q, q); +} + +code init_final(PhilsPtr self) +{ + self->right = phils_list; + self->right_fork = phils_list->left_fork; + printf("init all\n"); + + goto create_queue(1, self, 0, 0, task_entry0); +} + +code init_phils2(PhilsPtr self, int count, int id) +{ + PhilsPtr tmp_self; + + tmp_self = (PhilsPtr)malloc(sizeof(Phils)); + if (!tmp_self) { + goto die("Can't allocate Phils\n"); + } + self->right = tmp_self; + tmp_self->id = id; + tmp_self->right_fork = NULL; + tmp_self->left_fork = self->right_fork; + tmp_self->right = NULL; + tmp_self->left = self; + tmp_self->next = thinking; + + count--; + id++; + + if (count == 0) { + goto init_final(tmp_self); + } else { + goto init_fork2(tmp_self, count, id); + } +} + +code init_fork2(PhilsPtr self, int count, int id) +{ + ForkPtr tmp_fork; + + tmp_fork = (ForkPtr)malloc(sizeof(Fork)); + if (!tmp_fork) { + goto die("Can't allocate Fork\n"); + } + tmp_fork->id = id; + tmp_fork->owner = NULL; + self->right_fork = tmp_fork; + + goto init_phils2(self, count, id); +} + +code init_phils1(ForkPtr fork, int count, int id) +{ + PhilsPtr self; + + self = (PhilsPtr)malloc(sizeof(Phils)); + if (!self) { + goto die("Can't allocate Phils\n"); + } + phils_list = self; + self->id = id; + self->right_fork = NULL; + self->left_fork = fork; + self->right = NULL; + self->left = NULL; + self->next = thinking; + + count--; + id++; + + goto init_fork2(self, count, id); +} + +code init_fork1(int count) +{ + ForkPtr fork; + int id = 1; + + fork = (ForkPtr)malloc(sizeof(Fork)); + if (!fork) { + goto die("Can't allocate Fork\n"); + } + fork->id = id; + fork->owner = NULL; + + goto init_phils1(fork, count, id); +} + +code die(char *err) +{ + printf("%s\n", err); + goto ret(1), env; +} + +int main(int argc, char **argv) +{ + ret = return; + env = environment; + // srand((unsigned)time(NULL)); + // srandom((unsigned long)time(NULL)); + get_next_task = get_next_task_fifo; + if (argc == 2) { + if (argv[1][0] == '-') { + if (argv[1][1] == 'r') { + printf("select random\n"); + get_next_task = get_next_task_random; + srandom(time(NULL)); + } else { + printf("FIFO\n"); + get_next_task = get_next_task_fifo; + } + } + } + + goto init_fork1(NUM_PHILOSOPHER); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/scheduler.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,8 @@ +/* +** Dining Philosophers Problem's scheduler +*/ + +extern struct task * current_task; +code scheduler(PhilsPtr self, TaskPtr task); + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/state_db.c Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,83 @@ +#include <stdlib.h> + +#include "state_db.h" +#include "memory.h" + +StateDB +create_stateDB() +{ + StateDB s = (StateDB)malloc(sizeof(StateNode)); + if (!s) die_exit("Cann't alloc state db node."); + return s; +} + +static MemoryPtr mem_db; + +static int state_count0; + +void +reset_state_count() +{ + state_count0 = 0; +} + +int +state_count() +{ + return state_count0; +} + + +/* + + lookup_StateDB(struct state *s, StateDB *parent, StatePtr *out) + + s->memory points the real memory + if s is new, it is copied in the database (parent). + if s is in the database, existing state is returned. + + if return value is 0, it returns new state. + if out is null, no copy_state is created. (lookup mode) + + Founded state or newly created state is returned in out. + + */ + +int +lookup_StateDB(StateDB s, StateDB *parent, StateDB *out) +{ + StateDB db; + int r; + + while(1) { + db = *parent; + if (!db) { + /* not found */ + if (out) { + db = create_stateDB(); + db->left = db->right = 0; + db->memory = copy_memory(s->memory,&mem_db); + db->hash = s->hash; + state_count0 ++; + *parent = db; + *out = db; + } + return 0; + } + if (s->hash == db->hash) { + r = cmp_memory(s->memory,db->memory); + } else + r = (s->hash > db->hash)? 1 : -1; + if(!r) { + /* bingo */ + if (out) *out = db; + return 1; + } else if (r>0) { + parent = &db->left; + } else if (r<0) { + parent = &db->right; + } + } +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/state_db.h Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,20 @@ +#ifndef _STATE_DB_H_ +#define _STATE_DB_H_ + + +typedef struct state_db { + struct memory *memory; + int hash; + struct state_db *left; + struct state_db *right; +} StateNode, *StateDB; + +extern int +lookup_StateDB(StateDB s, StateDB *db, StateDB *out); + +extern int state_count(); +extern void reset_state_count(); + + + +#endif
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tableau.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,293 @@ +/* +** Dining Philosophers Problem's scheduler +** with state developper as a tableau method + +** 連絡先： 琉球大学情報工学科 河野 真治 +** （E-Mail Address: kono@ie.u-ryukyu.ac.jp） +** +** このソースのいかなる複写，改変，修正も許諾します。ただし、 +** その際には、誰が貢献したを示すこの部分を残すこと。 +** 再配布や雑誌の付録などの問い合わせも必要ありません。 +** 営利利用も上記に反しない範囲で許可します。 +** バイナリの配布の際にはversion messageを保存することを条件とします。 +** このプログラムについては特に何の保証もしない、悪しからず。 +** +** Everyone is permitted to do anything on this program +** including copying, modifying, improving, +** as long as you don't try to pretend that you wrote it. +** i.e., the above copyright notice has to appear in all copies. +** Binary distribution requires original version messages. +** You don't have to ask before copying, redistribution or publishing. +** THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE. + +*/ +#include <stdlib.h> +#include <time.h> +#include "dpp2.h" +#include "queue.h" +#include "memory.h" +#include "state_db.h" + +int NUM_PHILOSOPHER = 5; /* A number of philosophers must be more than 2. */ + +static code (*ret)(int); +static void *env; + +static PhilsPtr phils_list = NULL; + +static int max_step = 100; + +static StateDB state_db; +static MemoryPtr mem; +static StateNode st; + +int +list_length(TaskPtr list) +{ + int length; + TaskPtr t; + + if (!list) return 0; + t = list->next; + + for (length = 1; t && t != list; length++) { + t = t->next; + } + return length; +} + +TaskPtr +get_task(int num, TaskPtr list) +{ + while (num-- > 0) { + list = list->next; + } + return list; +} + + +static TaskIteratorPtr task_iter; +static int depth,count; + +/* + Performe depth frist search + Possible task iterleave is generated by TaskIterator + (using task ring) + State are recorded in StateDB + all memory fragments are regsitered by add_memory_range() + including task queue + */ + + +code tableau(TaskPtr list) +{ + StateDB out; + + st.hash = get_memory_hash(mem,0); + if (lookup_StateDB(&st, &state_db, &out)) { + // found in the state database + //printf("found %d\n",count); + while(!(list = next_task_iterator(task_iter))) { + // no more branch, go back to the previous one + TaskIteratorPtr prev_iter = task_iter->prev; + if (!prev_iter) { + printf("All done count %d\n",count); + memory_usage(); + goto ret(0),env; + } + //printf("no more branch %d\n",count); + depth--; + free_task_iterator(task_iter); + task_iter = prev_iter; + } + // return to previous state + // here we assume task list is fixed, we don't have to + // recover task list itself + restore_memory(task_iter->state->memory); + //printf("restore list %x next %x\n",(int)list,(int)(list->next)); + } else { + // one step further + depth++; + task_iter = create_task_iterator(list,out,task_iter); + } + //printf("depth %d count %d\n", depth, count++); + count++; + goto list->phils->next(list->phils,list); +} + +code get_next_task_fifo(TaskPtr list) +{ + TaskPtr t = list; + TaskPtr e; + + if (max_step--<0) goto die("Simuration end."); + + list = list->next; + goto list->phils->next(list->phils,list); +} + +code scheduler(PhilsPtr phils, TaskPtr list) +{ + goto tableau(list); + // goto next_next_task_fifo(list); +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last); + +code task_entry2(int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q) +{ + if (!q) { + goto die("Can't allocate Task\n"); + } else { + add_memory_range(q,sizeof(Task),&mem); + goto enqueue(count, self, list, last, q, task_entry1); + } +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last) +{ + StateDB out; + /* + printf("int count %d, PhilsPtr self %x, TaskPtr list %x, TaskPtr last %x\n", + count, self, list, last); + */ + + if (count++ < NUM_PHILOSOPHER) { + self = self->left; + goto create_queue(count,self,list,last,task_entry2); + } else { + // make circular task list + last->next = list; + st.memory = mem; + st.hash = get_memory_hash(mem,0); + lookup_StateDB(&st, &state_db, &out); + task_iter = create_task_iterator(list,out,0); + // start first task + goto list->phils->next(list->phils,list); + } +} + +code task_entry0(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q) +{ + add_memory_range(q,sizeof(Task),&mem); + goto task_entry1(count, self, q, q); +} + +code init_final(PhilsPtr self) +{ + self->right = phils_list; + self->right_fork = phils_list->left_fork; + //printf("init all\n"); + + goto create_queue(1, self, 0, 0, task_entry0); +} + +code init_phils2(PhilsPtr self, int count, int id) +{ + PhilsPtr tmp_self; + + tmp_self = (PhilsPtr)malloc(sizeof(Phils)); + if (!tmp_self) { + goto die("Can't allocate Phils\n"); + } + self->right = tmp_self; + tmp_self->id = id; + tmp_self->right_fork = NULL; + tmp_self->left_fork = self->right_fork; + tmp_self->right = NULL; + tmp_self->left = self; + tmp_self->next = thinking; + add_memory_range(tmp_self,sizeof(Phils),&mem); + + count--; + id++; + + if (count == 0) { + goto init_final(tmp_self); + } else { + goto init_fork2(tmp_self, count, id); + } +} + +code init_fork2(PhilsPtr self, int count, int id) +{ + ForkPtr tmp_fork; + + tmp_fork = (ForkPtr)malloc(sizeof(Fork)); + if (!tmp_fork) { + goto die("Can't allocate Fork\n"); + } + tmp_fork->id = id; + tmp_fork->owner = NULL; + self->right_fork = tmp_fork; + add_memory_range(tmp_fork,sizeof(Fork),&mem); + + goto init_phils2(self, count, id); +} + +code init_phils1(ForkPtr fork, int count, int id) +{ + PhilsPtr self; + + self = (PhilsPtr)malloc(sizeof(Phils)); + if (!self) { + goto die("Can't allocate Phils\n"); + } + phils_list = self; + self->id = id; + self->right_fork = NULL; + self->left_fork = fork; + self->right = NULL; + self->left = NULL; + self->next = thinking; + add_memory_range(self,sizeof(Phils),&mem); + + count--; + id++; + + goto init_fork2(self, count, id); +} + +code init_fork1(int count) +{ + ForkPtr fork; + int id = 1; + + fork = (ForkPtr)malloc(sizeof(Fork)); + if (!fork) { + goto die("Can't allocate Fork\n"); + } + fork->id = id; + fork->owner = NULL; + add_memory_range(fork,sizeof(Fork),&mem); + + goto init_phils1(fork, count, id); +} + +code die(char *err) +{ + printf("%s\n", err); + goto ret(1), env; +} + +int main(int ac, char *av[]) +{ + ret = return; + env = environment; + // srand((unsigned)time(NULL)); + // srandom((unsigned long)time(NULL)); + srandom(555); + + if (ac==2) { + NUM_PHILOSOPHER = atoi(av[1]); + if (NUM_PHILOSOPHER >10 ||NUM_PHILOSOPHER < 2) { + printf("illegal number of philosopher = %d\n", NUM_PHILOSOPHER ); + return 1; + } + printf("number of philosopher = %d\n", NUM_PHILOSOPHER ); + } + + goto init_fork1(NUM_PHILOSOPHER); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tableau2.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,299 @@ +/* +** Dining Philosophers Problem's scheduler +** with state developper as a tableau method + +** 連絡先： 琉球大学情報工学科 河野 真治 +** （E-Mail Address: kono@ie.u-ryukyu.ac.jp） +** +** このソースのいかなる複写，改変，修正も許諾します。ただし、 +** その際には、誰が貢献したを示すこの部分を残すこと。 +** 再配布や雑誌の付録などの問い合わせも必要ありません。 +** 営利利用も上記に反しない範囲で許可します。 +** バイナリの配布の際にはversion messageを保存することを条件とします。 +** このプログラムについては特に何の保証もしない、悪しからず。 +** +** Everyone is permitted to do anything on this program +** including copying, modifying, improving, +** as long as you don't try to pretend that you wrote it. +** i.e., the above copyright notice has to appear in all copies. +** Binary distribution requires original version messages. +** You don't have to ask before copying, redistribution or publishing. +** THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE. + +*/ +#include <stdlib.h> +#include <time.h> +#include "dpp2.h" +#include "queue.h" +#include "memory.h" +#include "state_db.h" +#include "ltl.h" + +int NUM_PHILOSOPHER = 5; /* A number of philosophers must be more than 2. */ + +static code (*ret)(int); +static void *env; + +static PhilsPtr phils_list = NULL; + +static int max_step = 100; + +static StateDB state_db; +static MemoryPtr mem; +static StateNode st; +static int always_flag; // for LTL + +int +list_length(TaskPtr list) +{ + int length; + TaskPtr t; + + if (!list) return 0; + t = list->next; + + for (length = 1; t && t != list; length++) { + t = t->next; + } + return length; +} + +TaskPtr +get_task(int num, TaskPtr list) +{ + while (num-- > 0) { + list = list->next; + } + return list; +} + + +static TaskIteratorPtr task_iter; +static int depth,count; + +/* + Performe depth frist search + Possible task iterleave is generated by TaskIterator + (using task ring) + State are recorded in StateDB + all memory fragments are regsitered by add_memory_range() + including task queue + */ + + +code tableau(TaskPtr list) +{ + StateDB out; + + st.hash = get_memory_hash(mem,0); + if (lookup_StateDB(&st, &state_db, &out)) { + // found in the state database + //printf("found %d\n",count); + while(!(list = next_task_iterator(task_iter))) { + // no more branch, go back to the previous one + TaskIteratorPtr prev_iter = task_iter->prev; + if (!prev_iter) { + printf("All done count %d\n",count); + memory_usage(); + show_result(always_flag); + goto ret(0),env; + } + //printf("no more branch %d\n",count); + depth--; + free_task_iterator(task_iter); + task_iter = prev_iter; + } + // return to previous state + // here we assume task list is fixed, we don't have to + // recover task list itself + restore_memory(task_iter->state->memory); + //printf("restore list %x next %x\n",(int)list,(int)(list->next)); + } else { + // one step further + depth++; + task_iter = create_task_iterator(list,out,task_iter); + } + //printf("depth %d count %d\n", depth, count++); + count++; + goto list->phils->next(list->phils,list); +} + +code get_next_task_fifo(TaskPtr list) +{ + TaskPtr t = list; + TaskPtr e; + + if (max_step--<0) goto die("Simuration end."); + + list = list->next; + goto list->phils->next(list->phils,list); +} + +code scheduler(PhilsPtr phils, TaskPtr list) +{ + goto check(&always_flag, phils, list); + // goto next_next_task_fifo(list); +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last); + +code task_entry2(int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q) +{ + if (!q) { + goto die("Can't allocate Task\n"); + } else { + add_memory_range(q,sizeof(Task),&mem); + goto enqueue(count, self, list, last, q, task_entry1); + } +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last) +{ + StateDB out; + /* + printf("int count %d, PhilsPtr self %x, TaskPtr list %x, TaskPtr last %x\n", + count, self, list, last); + */ + + if (count++ < NUM_PHILOSOPHER) { + self = self->left; + goto create_queue(count,self,list,last,task_entry2); + } else { + // make circular task list + last->next = list; + st.memory = mem; + st.hash = get_memory_hash(mem,0); + lookup_StateDB(&st, &state_db, &out); + task_iter = create_task_iterator(list,out,0); + // start first task + goto list->phils->next(list->phils,list); + } +} + +code task_entry0(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q) +{ + add_memory_range(q,sizeof(Task),&mem); + goto task_entry1(count, self, q, q); +} + +code init_final(PhilsPtr self) +{ + self->right = phils_list; + phils_list->left = self; + self->right_fork = phils_list->left_fork; + always_flag = 1; + //add_memory_range(&always_flag, sizeof(int), &mem); + //printf("init all\n"); + + goto create_queue(1, self, 0, 0, task_entry0); +} + +code init_phils2(PhilsPtr self, int count, int id) +{ + PhilsPtr tmp_self; + + tmp_self = (PhilsPtr)malloc(sizeof(Phils)); + if (!tmp_self) { + goto die("Can't allocate Phils\n"); + } + self->right = tmp_self; + tmp_self->id = id; + tmp_self->right_fork = NULL; + tmp_self->left_fork = self->right_fork; + tmp_self->right = NULL; + tmp_self->left = self; + tmp_self->next = thinking; + add_memory_range(tmp_self,sizeof(Phils),&mem); + + count--; + id++; + + if (count == 0) { + goto init_final(tmp_self); + } else { + goto init_fork2(tmp_self, count, id); + } +} + +code init_fork2(PhilsPtr self, int count, int id) +{ + ForkPtr tmp_fork; + + tmp_fork = (ForkPtr)malloc(sizeof(Fork)); + if (!tmp_fork) { + goto die("Can't allocate Fork\n"); + } + tmp_fork->id = id; + tmp_fork->owner = NULL; + self->right_fork = tmp_fork; + add_memory_range(tmp_fork,sizeof(Fork),&mem); + + goto init_phils2(self, count, id); +} + +code init_phils1(ForkPtr fork, int count, int id) +{ + PhilsPtr self; + + self = (PhilsPtr)malloc(sizeof(Phils)); + if (!self) { + goto die("Can't allocate Phils\n"); + } + phils_list = self; + self->id = id; + self->right_fork = NULL; + self->left_fork = fork; + self->right = NULL; + self->left = NULL; + self->next = thinking; + add_memory_range(self,sizeof(Phils),&mem); + + count--; + id++; + + goto init_fork2(self, count, id); +} + +code init_fork1(int count) +{ + ForkPtr fork; + int id = 1; + + fork = (ForkPtr)malloc(sizeof(Fork)); + if (!fork) { + goto die("Can't allocate Fork\n"); + } + fork->id = id; + fork->owner = NULL; + add_memory_range(fork,sizeof(Fork),&mem); + + goto init_phils1(fork, count, id); +} + +code die(char *err) +{ + printf("%s\n", err); + goto ret(1), env; +} + +int main(int ac, char *av[]) +{ + ret = return; + env = environment; + // srand((unsigned)time(NULL)); + // srandom((unsigned long)time(NULL)); + srandom(555); + + if (ac==2) { + NUM_PHILOSOPHER = atoi(av[1]); + if (NUM_PHILOSOPHER >10 ||NUM_PHILOSOPHER < 2) { + printf("illegal number of philosopher = %d\n", NUM_PHILOSOPHER ); + return 1; + } + printf("number of philosopher = %d\n", NUM_PHILOSOPHER ); + } + + goto init_fork1(NUM_PHILOSOPHER); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tableau3.cbc Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,301 @@ +/* +** Dining Philosophers Problem's scheduler +** with state developper as a tableau method + +** 連絡先： 琉球大学情報工学科 河野 真治 +** （E-Mail Address: kono@ie.u-ryukyu.ac.jp） +** +** このソースのいかなる複写，改変，修正も許諾します。ただし、 +** その際には、誰が貢献したを示すこの部分を残すこと。 +** 再配布や雑誌の付録などの問い合わせも必要ありません。 +** 営利利用も上記に反しない範囲で許可します。 +** バイナリの配布の際にはversion messageを保存することを条件とします。 +** このプログラムについては特に何の保証もしない、悪しからず。 +** +** Everyone is permitted to do anything on this program +** including copying, modifying, improving, +** as long as you don't try to pretend that you wrote it. +** i.e., the above copyright notice has to appear in all copies. +** Binary distribution requires original version messages. +** You don't have to ask before copying, redistribution or publishing. +** THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE. + +*/ +#include <stdlib.h> +#include <time.h> +#include "dpp2.h" +#include "queue.h" +#include "memory.h" +#include "state_db.h" +#include "ltl.h" + +int NUM_PHILOSOPHER = 5; /* A number of philosophers must be more than 2. */ + +static code (*ret)(int); +static void *env; + +static PhilsPtr phils_list = NULL; + +static int max_step = 100; + +static StateDB state_db; +static MemoryPtr mem; +static StateNode st; +static int always_flag; // for LTL + +int +list_length(TaskPtr list) +{ + int length; + TaskPtr t; + + if (!list) return 0; + t = list->next; + + for (length = 1; t && t != list; length++) { + t = t->next; + } + return length; +} + +TaskPtr +get_task(int num, TaskPtr list) +{ + while (num-- > 0) { + list = list->next; + } + return list; +} + + +static TaskIteratorPtr task_iter; +static int depth,count; + +/* + Performe depth frist search + Possible task iterleave is generated by TaskIterator + (using task ring) + State are recorded in StateDB + all memory fragments are regsitered by add_memory_range() + including task queue + */ + + +code tableau(TaskPtr list) +{ + StateDB out; + + st.hash = get_memory_hash(mem,0); + if (lookup_StateDB(&st, &state_db, &out)) { + // found in the state database + //printf("found %d\n",count); + while(!(list = next_task_iterator(task_iter))) { + // no more branch, go back to the previous one + TaskIteratorPtr prev_iter = task_iter->prev; + if (!prev_iter) { + printf("All done count %d\n",count); + printf("Number of unique states %d\n", state_count()); + memory_usage(); + show_result(always_flag); + goto ret(0),env; + } + //printf("no more branch %d\n",count); + depth--; + free_task_iterator(task_iter); + task_iter = prev_iter; + } + // return to previous state + // here we assume task list is fixed, we don't have to + // recover task list itself + restore_memory(task_iter->state->memory); + //printf("restore list %x next %x\n",(int)list,(int)(list->next)); + } else { + // one step further + depth++; + task_iter = create_task_iterator(list,out,task_iter); + } + //printf("depth %d count %d\n", depth, count++); + count++; + goto list->phils->next(list->phils,list); +} + +code get_next_task_fifo(TaskPtr list) +{ + TaskPtr t = list; + TaskPtr e; + + if (max_step--<0) goto die("Simuration end."); + + list = list->next; + goto list->phils->next(list->phils,list); +} + +code scheduler(PhilsPtr phils, TaskPtr list) +{ + goto check(&always_flag, phils, list); + // goto next_next_task_fifo(list); +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last); + +code task_entry2(int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q) +{ + if (!q) { + goto die("Can't allocate Task\n"); + } else { + add_memory_range(q,sizeof(Task),&mem); + goto enqueue(count, self, list, last, q, task_entry1); + } +} + +code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last) +{ + StateDB out; + /* + printf("int count %d, PhilsPtr self %x, TaskPtr list %x, TaskPtr last %x\n", + count, self, list, last); + */ + + if (count++ < NUM_PHILOSOPHER) { + self = self->left; + goto create_queue(count,self,list,last,task_entry2); + } else { + // make circular task list + last->next = list; + st.memory = mem; + st.hash = get_memory_hash(mem,0); + lookup_StateDB(&st, &state_db, &out); + task_iter = create_task_iterator(list,out,0); + // start first task + goto list->phils->next(list->phils,list); + } +} + +code task_entry0(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q) +{ + add_memory_range(q,sizeof(Task),&mem); + goto task_entry1(count, self, q, q); +} + +code init_final(PhilsPtr self) +{ + self->right = phils_list; + phils_list->left = self; + self->right_fork = phils_list->left_fork; + always_flag = 1; + //add_memory_range(&always_flag, sizeof(int), &mem); + //printf("init all\n"); + + goto create_queue(1, self, 0, 0, task_entry0); +} + +code init_phils2(PhilsPtr self, int count, int id) +{ + PhilsPtr tmp_self; + + tmp_self = (PhilsPtr)malloc(sizeof(Phils)); + if (!tmp_self) { + goto die("Can't allocate Phils\n"); + } + self->right = tmp_self; + tmp_self->id = id; + tmp_self->right_fork = NULL; + tmp_self->left_fork = self->right_fork; + tmp_self->right = NULL; + tmp_self->left = self; + tmp_self->next = pickup_lfork; + add_memory_range(tmp_self,sizeof(Phils),&mem); + + count--; + id++; + + if (count == 0) { + goto init_final(tmp_self); + } else { + goto init_fork2(tmp_self, count, id); + } +} + +code init_fork2(PhilsPtr self, int count, int id) +{ + ForkPtr tmp_fork; + + tmp_fork = (ForkPtr)malloc(sizeof(Fork)); + if (!tmp_fork) { + goto die("Can't allocate Fork\n"); + } + tmp_fork->id = id; + tmp_fork->owner = NULL; + self->right_fork = tmp_fork; + add_memory_range(tmp_fork,sizeof(Fork),&mem); + + goto init_phils2(self, count, id); +} + +code init_phils1(ForkPtr fork, int count, int id) +{ + PhilsPtr self; + + self = (PhilsPtr)malloc(sizeof(Phils)); + if (!self) { + goto die("Can't allocate Phils\n"); + } + phils_list = self; + self->id = id; + self->right_fork = NULL; + self->left_fork = fork; + self->right = NULL; + self->left = NULL; + self->next = pickup_lfork; + add_memory_range(self,sizeof(Phils),&mem); + + count--; + id++; + + goto init_fork2(self, count, id); +} + +code init_fork1(int count) +{ + ForkPtr fork; + int id = 1; + + fork = (ForkPtr)malloc(sizeof(Fork)); + if (!fork) { + goto die("Can't allocate Fork\n"); + } + fork->id = id; + fork->owner = NULL; + add_memory_range(fork,sizeof(Fork),&mem); + + goto init_phils1(fork, count, id); +} + +code die(char *err) +{ + printf("%s\n", err); + goto ret(1), env; +} + +int main(int ac, char *av[]) +{ + ret = return; + env = environment; + // srand((unsigned)time(NULL)); + // srandom((unsigned long)time(NULL)); + reset_state_count(); + srandom(555); + + if (ac==2) { + NUM_PHILOSOPHER = atoi(av[1]); + if (NUM_PHILOSOPHER >10 ||NUM_PHILOSOPHER < 2) { + printf("illegal number of philosopher = %d\n", NUM_PHILOSOPHER ); + return 1; + } + //printf("number of philosopher = %d\n", NUM_PHILOSOPHER ); + } + + goto init_fork1(NUM_PHILOSOPHER); +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/memory_test.c Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,84 @@ +#include <stdio.h> +#include <strings.h> + +#include "memory.h" + +static int array1[100]; +static int array2[100]; +static int array3[200]; +static int array4[200]; + +MemoryPtr db; + +int main() +{ + int found; + /* basic unit test */ + + MemoryPtr m1 = create_memory(array1,sizeof(array1)); + MemoryPtr m2 = create_memory(array2,sizeof(array2)); + + compute_memory_hash1(m1); + compute_memory_hash1(m2); + + printf("cmp %d ... 0 \n", cmp_content(m1,m2)); + + array1[0x55] = 0x55; + compute_memory_hash1(m1); + + printf("cmp %d .... 1 or -1 \n", cmp_content(m1,m2)); + + /* memory fragments */ + + MemoryPtr a1 = add_memory(array1,sizeof(array1),&db); + MemoryPtr a2 = add_memory(array2,sizeof(array2),&db); + MemoryPtr a3 = add_memory(array3,sizeof(array3),&db); + MemoryPtr a4 = add_memory(array4,sizeof(array4),&db); + + array1[0x45] = 0xff; + array2[0x46] = 0xf0; + array3[0x47] = 0xe8; + array4[0x48] = 0xe8; + + a1 = add_memory(array1,sizeof(array1),&db); + a2 = add_memory(array2,sizeof(array2),&db); + a3 = add_memory(array3,sizeof(array3),&db); + a4 = add_memory(array4,sizeof(array4),&db); + + array2[0x55] = 0x55; + array1[0x46] = 0xf0; + array2[0x45] = 0xff; + array3[0x48] = 0xe8; + array4[0x47] = 0xe8; + + a1 = add_memory(array1,sizeof(array1),&db); + a2 = add_memory(array2,sizeof(array2),&db); + a3 = add_memory(array3,sizeof(array3),&db); + a4 = add_memory(array4,sizeof(array4),&db); + + bzero(array1,sizeof(array1)); + + printf("zero\n"); + a1 = add_memory(array1,sizeof(array1),&db); + found = memory_lookup(a1,&db,0,&a2); + if (found) { + printf("found\n"); + if (cmp_memory(a1,a2)) printf("different\n"); else printf("same\n"); + } else { + printf("not found\n"); + } + + printf("modified\n"); + array1[0x10] = 0xf0; + found = memory_lookup(m1,&db,0,&a2); + if (found) { + printf("found\n"); + if (cmp_memory(a1,a2)) printf("same\n"); else printf("different\n"); + } else { + printf("not found\n"); + } + + return 0; +} + +/* end */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/state_test.c Wed Dec 16 15:16:11 2015 +0900 @@ -0,0 +1,45 @@ +#include <stdio.h> +#include "memory.h" +#include "state_db.h" + +static int array1[10]; +static int array2[10]; +static int array3[20]; +static int array4[20]; + +MemoryPtr mem; // memory range +StateDB state_db; // state database + +int main() +{ + StateDB s0; + StateNode st; + int ret; + + // register memory fragments + MemoryPtr a1 = add_memory_range(array1,sizeof(array1),&mem); + MemoryPtr a2 = add_memory_range(array2,sizeof(array2),&mem); + MemoryPtr a3 = add_memory_range(array3,sizeof(array3),&mem); + MemoryPtr a4 = add_memory_range(array4,sizeof(array4),&mem); + st.memory = mem; + + printf("%d %d\n",a1->body==a2->body,a3->body==a4->body); + for(;;) { + + // modify memory and calculate hash + array2[5] = (array2[5]+1)&0xf; + st.hash = get_memory_hash(mem,0); + + // check if it is in the db + ret = lookup_StateDB(&st, &state_db, &s0); + printf("%0x %d\n",(int)s0,array2[5]); + if (ret) { + printf("the same state %d\n", state_count()); + break;; + } + } + + return 0; +} + +/* end */