title: Verification of programs using Continuation based C
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的
* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
* プログラムはコードセグメントという処理の集合として表され、相互に接続される
* 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する

# 研究内容
* コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
* コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
* コードを検証用に変更することなく、仕様を満たすか検証する
* 検証の対象として Gears OS のデータ構造を用いる

# 近況報告
* Synchronized Queue の verification をどうするか
* Red-Black Tree の検証の面倒なところ

# Gears の synchronized queue はどうするか
* 有限長 or 無限長
* 有限長なら限度まで入ってる時に put すると(待つ|失敗する)
* empty に対して get すると(待つ|失敗する)
* 今の Gears のコードは無限長、getは空だと待つ

# Synchronized Queue の何をチェックするか
* 適当に探してみた論文
* [Automatically Verifying Concurrent Queue Algorithms](http://www.cs.technion.ac.il/~yahave/papers/softmc03.pdf)
* CAS 版と lock 版がある
* こちらも無限長、getは待つ

# Properties Sample in Automatically Verifying Concurrent Queue Algorithms
* P1. The linked list is always connected.
* P2. Nodes are only inserted after the last node of the linked list.
* P3. Nodes are only deleted from the beginning of the linked list.
* P4. Head always points to the first node in the linked list.
* P5. Tail always points to a node in the linked list.

# どう検証するか
* 仕様
    * Get は empty なら待ち
    * Put は中の要素数にかかわらず受けつける
* thread の挙動を全列挙すると全部止まる可能性がある
* Get する thread と Put する thread の実行順を全部列挙
    * CAS にたぶん失敗しないので良いのかなといった感じ
* CAS のコードは別にチェックする?

# Red-Black Tree の検証の面倒な点
* 気分転換に書いてたりしましたが
* 再帰なしスタックなしで木をどうやってDFSするか
* メモリを copying GC like に管理する
    * copy した tree と node stack との整合性を取るのが大変

<!-- vim: set filetype=markdown.slide: -->