新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

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

May

3

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

設計モデルと仕様を比較するツールを作りましょう.

Organizing : 株式会社 PRINCIPIA

Hashtag :#refinementchecker
Registration info

一般

6000 (Pre-pay)

FCFS
0/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. トレース比較器の実装(セミナー後)

セミナーでの解説を元にデッドロック発見器をトレース比較器にバージョンアップします。 しくみおよび実装に関する質問は基本メールにてお受けします。

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

  • PC
  • 使用するプログラミング言語での開発環境(サンプル実装を動かすためには OCaml または C コンパイラが必要です.OCaml のサンプル実装は version 4.08.0 で確認しています)
  • Graphviz (dot コマンド):状態遷移グラフを可視化するために使用します.
  • Zoom ミーティングに参加するための機材(マイク・イヤホン等)

Zoom URL

CONNPASS のメッセージにてお知らせします。

配布物

スライド資料(PDF)とサンプル実装のソースコード(C言語と OCaml)を 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.

Feed

hatsugai

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

03/30/2020 20:12

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

Ended

2020/05/03(Sun)

14:00
18:00

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

Registration Period
2020/03/30(Mon) 00:00 〜
2020/05/03(Sun) 11:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(0)

No attendees yet.

Attendees (0)