新機能 イベントメッセージの予約機能を追加しました。イベント主催者様は、参加者へのメッセージ送信を事前に予約できます。詳しくはこちらをご確認ください。

新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

このエントリーをはてなブックマークに追加

Sep

20

トレース比較器を作って学ぶマルチスレッドプログラミング

Organizing : 株式会社 PRINCIPIA

Hashtag :#形式手法
Registration info

一般

6000 (Pre-pay)

FCFS
5/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申し込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください

Print receipt data:

発行しない (詳しくはこちら)

Description

セミナーの内容

「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★」の続編です.

デッドロック発見器ではイベント同期という単純なしくみを使って様々な相互作用が表現できることを見ました.相互作用を決めるとシステム全体の振る舞いも状態遷移という形で計算することができ,その過程でデッドロックを発見することができました.

イベントを基礎とした相互作用にはもう1つ優れている点があります.それはシステムの振る舞いを仕様と比較することによって設計の正しさを検証できるという点です.

システムの振る舞いは外部から観測可能なイベントを発生順に並べた列として表すことができます.これをトレースといいます.システムが発生しうるトレースがすべて仕様で許容されたものであれば,システムの振る舞いはかなりの精度で正しいということができます.

一般にシステムは停止せずに動作を継続しますから,いくらでも長いトレースがありえます.さらにシステムが生成しうるトレースの種類も無限になる可能性があります.そうすると有限のメモリしか持たない計算機で有限の時間内に仕様と実装のトレースを比較することは不可能であるように思えますが,興味深いことに模倣(simulation)という考え方を使うとこれが可能になります.この模倣を計算することによって仕様と実装のトレースを比較するプログラムがトレース比較器です.

このセミナーのゴールはトレース比較器を作って仕様とシステムの振る舞いを比較できるようになることです.

以下の例では,初期状態から緑色の遷移をたどって同じトレースがありますが,最後の赤い状態のところで,仕様にはないイベントをシステムが発生していることがわかります.

状態遷移図

トレースは外部から観測可能なイベントだけを含むようにします.ユーザが関心を持つのは外部から見える動作だけで,内部のつくりは関係ないからです.

しかしシステムはコンポーネントを組み合わせて作りますから,その間で行われる相互作用のためのイベントも含まれています.これは内部の都合であって,ユーザには関係しません.

そこでこのような内部で使われるイベントを外から見えなくする処理を行います.これを隠蔽といいます.システムに隠蔽処理をしてからトレース比較を行うということです.

プログラムの正しさを検証するツールの中には,仕様は仕様記述言語,実装はモデリング言語と,仕様・実装で異なる表現形式を使うものがあります.これに対してトレース比較器はどちらも状態遷移で表します.この対称性のおかげで面白いことができます.仕様と実装を交換して比較することです.もし双方向の比較に成功したら,この2つはまったく同じトレースを含んでいるということになります.つまりトレース比較器を使うと状態遷移の等価性を判定することができます.ただし,これには1つ条件があります.実装に非決定性という性質がないことです.これについては発展的な内容としてセミナー内で紹介します.

トレース比較器はシステムの全体の振る舞いだけでなく,要求段階で検討するようなシナリオなども比較することができます.仕様検討や設計の試行錯誤など,プログラム開発の初期段階を支援してくれる強力な武器になると思います.

プログラム

A. プログラムの正当性とトレース比較器のしくみ

  1. 正当性:プログラムが仕様を満たす条件
  2. トレースによる正当性の検査
  3. 模倣(simulation)
  4. トレース比較器のしくみ
  5. 内部動作と隠蔽
  6. 非決定性と決定化[発展]
  7. 振る舞いの等価性[発展]

B. トレース比較器の設計と実装

OCaml と C による実装例を元にトレース比較器の設計を解説します.

  1. 隠蔽
  2. トレース比較
  3. テスト
  4. 決定化[発展]

C. 応用:検査と分析

トレース比較器の典型的な使い方を紹介します.

  1. 排他制御の安全性検査
  2. バッファ結合とキューの等価性
  3. リーダ・ライタ問題

D. トレース比較器の実装

各自、トレース比較器を好きな言語で設計・実装します。

※ セミナー時間内に完成させることは想定していません。セミナー後各自実装していただくことを想定しています。質問はメールまたは Slack にて受け付けます。

講師について

株式会社PRINCIPIA 代表取締役 初谷 久史

プロセス代数 CSP に基づいた対話的モデリング・検査ツール SyncStitch 開発者.

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師.

セミナー参加の前提条件

前提知識

  • マルチスレッドプログラミングについての基本的な知識:プロセス,スレッド,排他制御,ミューテックス,条件変数
  • アルゴリズムの知識:グラフの探索(幅優先探索または深さ優先探索)
  • データ構造の知識:ハッシュ表,キュー

必要なもの

  • 使用するプログラミング言語での開発環境(サンプル実装を動かすためには OCaml または C コンパイラが必要です.OCaml のサンプル実装は version 4.10.0 で確認しています)
  • Graphviz (dot コマンド):状態遷移グラフを可視化するために使用します.

配布物と Zoom URL

申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします。

事前に何度か配布する場合があります.同じ何度もメッセージが複数回届きますがご了承ください

プログラムの大きさの目安

トレース比較器のコード(デッドロック発見器に追加するコード)の大きさは,サンプル実装で次のとおりです.

  • OCaml 約100行(+決定化 約60行)
  • C言語 約150行(+決定化 約100行+整数の集合ライブラリ 約100行)

注意事項

  • このセミナーは「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★」の続編です.「★共有変数編★」の続編ではありません.
  • 講師が知らないプログラミング言語については対処が限られます.
  • 配布資料の公開は禁止です.

参考書

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください.

Media View all Media

If you add event media, up to 3 items will be shown here.

Ended

2020/09/20(Sun)

13:00
17:00

You cannot RSVP if you are already participating in another event at the same date.

Registration Period
2020/08/21(Fri) 00:00 〜
2020/09/20(Sun) 12:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(5)

RyosukeNakagawa

RyosukeNakagawa

トレース比較器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

Tute

Tute

トレース比較器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

hoshi-takanori

hoshi-takanori

トレース比較器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

gos_k

gos_k

トレース比較器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

IKEBE Ryohji

IKEBE Ryohji

トレース比較器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

Attendees (5)