annotate slides/20160112/slide.md @ 122:8bee87dcc403

Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 12 Jan 2016 17:54:48 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
122
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Verification of programs using Code Segments and Data Segments
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile:
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # 研究内容
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # 近況報告
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * atsuki さんの DPP 動くようになりました
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * sakura の方から100VMどうですか? って連絡が来てます
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 # DPP について
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 * CVS から持ってきて変換しました
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 * hg/CbC/DPP に mercurial repository を置いています
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 # DPP in LLVM 3.7
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * cbc-clang の 98:88e6d15e811d で動作確認
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 * brew install --HEAD ie-developers/ie/cbc
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * export CbC_Clang=/usr/local/Cellar/cbc/HEAD/bin
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * くらいです
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 # 変更点
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 * code を __code に
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 * return を __return に
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * goto 先が構造体の attribute だと TCE できなくて落ちてた
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * 一旦 enum で受けてその先で switch するとできました
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 # before
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 typedef struct phils {
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 int id;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 struct fork *right_fork;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 struct fork *left_fork;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 struct phils *right;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 struct phils *left;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 __code (*next)(struct phils *);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 } Phils, *PhilsPtr;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 goto list->phils->next(list->phils,list);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 * error: tableau : Tail call elimination was failed on codesegment which is accessed by pointer!
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 # after
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 goto do_action(list->phils, list);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 typedef struct phils {
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 int id;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 struct fork *right_fork;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 struct fork *left_fork;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 struct phils *right;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 struct phils *left;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 enum Action next;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 } Phils, *PhilsPtr;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 enum Action {
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 PutDownLeftFork,
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 PutDownRightFork,
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 /* ...... */
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 PutDownFork
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 };
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 __code do_action(PhilsPtr phils, TaskPtr list)
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 {
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 switch (phils->next) {
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 case PutDownLeftFork:
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 goto putdown_lfork(phils, list);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 case PutDownRightFork:
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 goto putdown_rfork(phils, list);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 /* ....... */
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 default:
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 printf("invalid action\n");
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 exit(1);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 }
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 __code (*action) (PhilsPtr, TaskPtr) = thinking;
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 goto action(phils, list);
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 }
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 ```
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 * で動きました
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 * Gears がこんな感じで enum で一旦受けて meta で next を決める形
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 # DPP について
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 * 実行ファイルが5つできました
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 * dpp
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 * 1つの philosopher のみが行動(スケジューラなし)
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 * 停止しない
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 * dpp2
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 * 全ての philosopher が順番に行動(スケジューラなし)
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 * デッドロックが発生する
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 * tableau
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 * スケジューラがいて遷移を管理している
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 * 乱数の seed が固定値(555)。この値だとデッドロックが発生
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 * tableau2
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 * tableau に LTL がついてるっぽい
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 * デッドロックするので p は満たされないと出る
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 * tableau3
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 * tableau2 で philosopher に行動が足されてるっぽい
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 * 同時にフォークを両方ともおろす
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 * p は not valid とのこと
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 # これから
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 * Gears の llrb に対して random な値を insert して木のバランスをチェックするように
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 * 状態の抽象化?
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 * 反例の短縮?
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 # sakura について
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 * 「講義用のクラウドについて」
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 * date 2016/01/05
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 * from nishiura@sakura.ad.jp (Toru Nishiura)
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 * 先生の提案とかあれば
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 # sakura についての案とか
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 * 講義用テンプレートのコピー
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 * イメージの削除
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137
8bee87dcc403 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 <!-- vim: set filetype=markdown.slide: -->