Mercurial > hg > Members > atton > seminar_slides
annotate slides/20160412/slide.md @ 134:82d19ce3b755
Add slide for seminar
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 12 Apr 2016 18:15:33 +0900 |
parents | |
children |
rev | line source |
---|---|
134
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 title: Verification of programs using Continuation based C |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 author: Yasutaka Higa |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 profile: |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 lang: Japanese |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 # 研究目的 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 # 研究内容 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 * コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 * コードセグメントどうしの接続の間にメタ計算として検証機構を導入する |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 * コードを検証用に変更することなく、仕様を満たすか検証する |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 * 検証の対象として Gears OS のデータ構造を用いる |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 # 近況報告 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 * Synchronized Queue の verification をどうするか |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 * Red-Black Tree の検証の面倒なところ |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 # Gears の synchronized queue はどうするか |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 * 有限長 or 無限長 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 * 有限長なら限度まで入ってる時に put すると(待つ|失敗する) |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 * empty に対して get すると(待つ|失敗する) |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 * 今の Gears のコードは無限長、getは空だと待つ |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 # Synchronized Queue の何をチェックするか |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 * 適当に探してみた論文 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 * [Automatically Verifying Concurrent Queue Algorithms](http://www.cs.technion.ac.il/~yahave/papers/softmc03.pdf) |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 * CAS 版と lock 版がある |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 * こちらも無限長、getは待つ |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 # Properties Sample in Automatically Verifying Concurrent Queue Algorithms |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 * P1. The linked list is always connected. |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 * P2. Nodes are only inserted after the last node of the linked list. |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 * P3. Nodes are only deleted from the beginning of the linked list. |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 * P4. Head always points to the first node in the linked list. |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 * P5. Tail always points to a node in the linked list. |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 # どう検証するか |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 * 仕様 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 * Get は empty なら待ち |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 * Put は中の要素数にかかわらず受けつける |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 * thread の挙動を全列挙すると全部止まる可能性がある |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 * Get する thread と Put する thread の実行順を全部列挙 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 * CAS にたぶん失敗しないので良いのかなといった感じ |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 * CAS のコードは別にチェックする? |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 # Red-Black Tree の検証の面倒な点 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 * 気分転換に書いてたりしましたが |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 * 再帰なしスタックなしで木をどうやってDFSするか |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 * メモリを copying GC like に管理する |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 * copy した tree と node stack との整合性を取るのが大変 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 |
82d19ce3b755
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 <!-- vim: set filetype=markdown.slide: --> |