新機能 イベント予約公開機能を追加しました!詳しくはこちらをご覧ください

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

Jul

14

並行システムの設計検証 第3回 デッドロック

Organizing : 株式会社 PRINCIPIA

Hashtag :#SyncStitch
Registration info

一般

3000 (Pre-pay)

FCFS
8/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申し込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.お支払いいただくのは資料(スライド資料とモデルファイル)の代金です.

Print receipt data:

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

Description

セミナーの内容

第3回のテーマはデッドロックです.並行システムに特徴的なデッドロックはなぜ発生するのか,そのメカニズムを解説します.ツール SyncStitch にはデッドロックを検出する機能があります.その使い方を解説します.

第3回 プログラム

  • 相互作用のモデル化2:共有メモリ(共有変数)
  • ミューテックスによる排他制御
  • デッドロック
  • デッドロック検査

シリーズの構成

  • 第1回 プロセスのモデル化
  • 第2回 相互作用と並行合成
  • 第3回 デッドロック
  • 第4回 part 1: 内部遷移・隠蔽・非決定性・発散,part 2: 振る舞いとは何か
  • 第5回 part 1: 正当性,part 2: トレース集合による安全性検査
  • 第6回 安定失敗集合による正当性検査

講師について

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

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

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

セミナー参加の前提条件

前提知識

前提として必要な知識は,プログラミングの知識と状態遷移モデル(オートマトン)の知識です.マルチスレッド(プロセス・タスク)のプログラムを書いたことがあるという程度の知識を仮定します.排他制御といった概念やミューテックス,セマフォといった同期のための機構についての知識を仮定します.

一部,発展的な内容に関する部分では,高校で習う程度の集合の記法(要素 x ∈ A,部分集合 A ⊆ B など)を使います.

必要なもの

Zoom URL

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

配布物

スライド資料(PDF)とモデルファイルを CONNPASS のメッセージにて配布します.

使用するツール

CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します.このツールで学んだ考え方と記法は他のツール(FDR, PAT, LTSA, ProB)でも活用できます(※これらのツール間でも細かい差異はあります).

注意事項

  • 配布スライド資料の公開は禁止です.
  • 各回を2回ずつ開催します.都合の良い回を選んで参加してください.申し込み後に都合が悪くなってもう一方の回に参加したい場合,別の曜日の回には申し込まずにご連絡ください.もう一方の回に参加できるよう調整します.2重に申し込みをしても一方はキャンセルできません.

参考書

連絡先

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

Media View all Media

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

Ended

2020/07/14(Tue)

21:00
22:30

Registration Period
2020/06/21(Sun) 00:00 〜
2020/07/14(Tue) 20:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(8)

tukejonny

tukejonny

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

niszet

niszet

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

kikuyuta

kikuyuta

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

TakeshiHori

TakeshiHori

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

kubota_junshi

kubota_junshi

I joined 並行システムの設計検証 第3回 デッドロック!

Nobu19800

Nobu19800

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

Tute

Tute

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

minekoa (みねこあ)

minekoa (みねこあ)

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

Attendees (8)