お知らせ 【重要なお知らせ】iOSアプリの運用および提供を2024年6月3日(月)を以て終了いたします。詳細は お知らせをご覧ください。

お知らせ connpassではさらなる価値のあるデータを提供するため、イベントサーチAPIの提供方法の見直しを決定しました。2024年5月23日(木)より 「企業・法人」「コミュニティ及び個人」向けの2プランを提供開始いたします。ご利用にあたっては利用申請及び審査がございます。詳細はヘルプページをご確認ください。

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

Jun

22

CTL モデル検査器を作って学ぶマルチスレッドプログラミング

条件を満たす状態や実行パスを探索するツールを作りましょう

Organizing : 株式会社 PRINCIPIA

CTL モデル検査器を作って学ぶマルチスレッドプログラミング
Hashtag :#形式手法
Registration info

一般

6000 (Pre-pay)

FCFS
1/10

Attendees
negi23
View Attendee List
Start Date
2024/06/22(Sat) 13:00 ~ 18:00
Registration Period

2024/04/13(Sat) 00:00 〜
2024/06/22(Sat) 12:30まで

Location

Zoom

オンライン

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

発行しない (詳しくはこちら)
出席登録
(イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます)

Description

お知らせ

都合により、開催日が 5/25(金) から 6/22(金) に変更されました。ご注意ください。

セミナーの内容

デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」の続編です.

デッドロック発見器では各スレッドの振る舞いを状態遷移として記述し,それらを合成してシステム全体の状態遷移を計算しました.その過程で遷移のない状態,すなわちデッドロック状態を発見することができました.

システムの状態遷移全体が可視化できるようになると,デッドロック以外にもいろいろ気づく点があります.例えば想定していなかった遷移や分岐があるとか,変数の値がおかしな状態があるなどの点です.さらに状態遷移の流れを追って動作を確認したくなります.

状態遷移グラフが小さいうちは,画面上で追ったり,印刷をしてマークしながら確認したりすることができます.しかし実践的なモデルは状態数がとても多くなるので,グラフ上を目視で追うことは難しくなります.

そこでこのセミナーでは再びこの仕事を計算機にやってもらうという戦略をとります.データベースのクエリーのように,条件を指定してそれを満たす状態や実行パスを探すツールを作ります.このようなツールをモデル検査器といいます.

このセミナーで作っていただくモデル検査器では次のような条件を指定することができます:

  • 変数の値についての条件:(例)x = 0, x > 3,リストに指定要素が含まれている,など.
  • 条件の結合: 否定(not),かつ(and),または(or)
  • 次の状態で条件が成り立つような状態:(例)次の状態で変数 x が 0 になる.
  • 実行パス上で常に条件が成り立つかどうか:(例)p と q が同時に 1 になることは決してない.
  • 実行パス上でいつか条件が成り立つかどうか:(例)いつかは必ず off になる.

セミナーのゴールは,自分で作成したデッドロック発見器を拡張し,条件を満たす状態に色を付けた,以下のような出力を得ることです.この例では3つのスレッドがロック獲得で競合しており,あるスレッドが要求しているにもかかわらずロックを獲得できない状態をマークしています.状態には成り立つ条件式も示しています.条件を様々に変えながらマークの付く状態を観察するのは実に楽しく,そうしているうちにシステムの振る舞いや性質がよくわかるようになります.

状態遷移図

条件を表す式としては計算木論理(Compulation Tree Logic, CTL)というものを使います.世にあるモデル検査器でも使われている表現の1つで,プログラマにとっても親しみやすいものだと思います.計算木論理についてはセミナーの中で説明しますので予備知識は必要ありません.

計算木論理を学ぶとプログラムの実行について理解を深めることができます.システムが可能な実行パスという考え方を獲得できるからです.抽象的な条件式を形式的に知るだけでなく,実際に条件を満たす状態や実行パスを求めるプログラムを書いて使ってみると,それらがどういうものであるかということを深く理解することができます.

自らプログラムを書いた経験があれば,計算木論理をサポートした強力な既存のツールも習得しやすくなります.プログラムを書くことで背景のしくみを理解し,実際の応用では強力なツールを使うというのは効率的な習得の方法だと思います.

さらに,実行パスという考え方はテストで応用できる可能性があります.状態遷移上の実行パスからテストケースを作るというのが1つのアイデアです.もう1つは実システムを実行させたときのログを取り,これを状態遷移上の実行パスと比較するというアイデアです.状態遷移モデルを持っているとこのような可能性が広がります.

プログラム

A. 計算木論理(CTL)とモデル検査器のしくみ

  1. 計算木論理(CTL)
  2. モデル検査器のしくみ:マーキングアルゴリズム

B. モデル検査器の設計と実装

はじめに OCaml と C による実装例を元にモデル検査器の設計を解説します.それを参考に自分のモデル検査器を設計・実装します.

  1. 条件式の表現
  2. マーキングアルゴリズム
  3. モデル検査器のテスト

C. 応用:検査と分析

モデル検査器の典型的な使い方を紹介します.

  1. モデル検査器でデッドロックを発見する
  2. さまざまな条件による状態の探索
  3. 安全性の検査(おかしな状態が含まれていないこと)
  4. ライブネスの検査(いつか条件を満たす状態に至ること)

D. 実装

各自、モデル検査器を好きな言語で設計・実装します。

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

講師について

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

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

国立情報学研究所トップエスイープロジェクト「モデル検査特論」講師.

セミナー参加の前提条件

前提知識

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

必要なもの

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

Zoom URL

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

配布物

スライド資料(PDF)とサンプル実装のソースコード(C言語と OCaml)を CONNPASS のメッセージにて送付します.

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

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

  • OCaml 約200行
  • C言語 約300行

注意事項

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

参考書

連絡先

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

Media View all Media

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

Group

PRINCIPIA

Number of events 117

Members 260

Public

2024/06/22(Sat)

13:00
18:00

Please login to register

Registration Period
2024/04/13(Sat) 00:00 〜
2024/06/22(Sat) 12:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(1)

negi23

negi23

CTL モデル検査器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

Attendees (1)