Mercurial > hg > Members > atton > seminar_slides

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

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