PRINCIPIA
ProductsDocumentationsAbout Us

並行システムの設計 トレーニングプログラム

弊社では並行システムの設計トレーニングプログラムを提供しています.

特に以下の分野の方々に,ご専門の技術をブーストする技術を習得していただけます.

キーワード

トレーニングのお申込み・ご相談は isaac@principia-m.com まで,お気軽にお尋ねください.


トレーニング資料公開中!

現在,トレーニング資料を公開しています.

トレーニング資料ページサンプル

トレーニング資料使用条件

資料はすべて PDF です.


並行システム設計トレーニングプログラム詳細

目的

本トレーニングの目的は

要求を満たす信頼性の高い並行システムを設計できるようになること

です.ここでいう設計とは次の3つの作業を意味します:

  1. 並行システムの振る舞いを表すモデルを作成すること
  2. 作成したモデルが与えられた要求や仕様を満たしていることを検証すること
  3. 検証されたモデルに基づいてシステムを実装すること

この目的を達成するために,本トレーニングでは以下の4つのサブゴールを設定しています:

  1. 並行システムについて学ぶ
  2. 並行システムの理論であるCSP 理論を学ぶ
  3. 並行システムの振る舞いをモデル化し CSP 理論に基づいて検証するツールの使い方を学ぶ
  4. 並行システムの実装方法について学ぶ

以下,4つのサブゴールについて説明します.

1. 並行システムについて学ぶ

並行システムとは何かをひとことでいうと次のようになります:

「複数の構成要素からなるシステムで,各構成要素が並行に動作し,互いに作用を及ぼしあいながら全体として目的の仕事をするシステムのこと」

設計する立場から並行システムを考えると,それ以外のシステムとは異なる点が大きく分けて2つあります.

相互作用と振る舞い

1つはシステムの構成要素がお互いに影響を及ぼしあうことです.これを相互作用といいます.一般には構成要素間だけでなくシステムそれ自身もユーザや他のシステムと相互作用をします.システムを外から観た場合,システムの振る舞いとはどのような相互作用をするかということであって,システム内部の作りや計算などには直接は関係しません.したがってシステムに対する要求やシステムの仕様は相互作用に基づいて記述することになります.同じことが相互作用をする構成要素に対してもいえます.並行システムの設計者はシステムや構成要素の振る舞いを相互作用に基づいて記述したり比較したりできる必要があります.入出力の関係としてとらえることのできるシステムでは主に計算ロジックの正しさが問題でしたが,並行システムでは内部計算ロジックの正しさに加えて相互作用としての振る舞いの正しさが問題になるということです.

並行性から生じる問題

並行システムがそれ以外のシステムとは異なるもう1つの点は,構成要素が並行に動作するというまさにその点から出てくる特徴的な性質があることです.厳密にいえばこれらは必ずしも並行システムに特有のものというわけではありませんが,並行システムではよく表れる性質であり,設計において考慮が必要となります.

性質は4つあります:

  1. 状態数の組み合わせ爆発
  2. 非決定性
  3. デッドロック
  4. ライブロック(発散)

(1) 状態数の組み合わせ爆発

状態数がそれぞれ m, n である構成要素2つからなるシステムの全状態数は,相互作用による制約がなければ m × n になります.このことからわかるようにシステムの状態数は構成要素の数に対して指数関数的に増えていきます.これを状態数の組み合わせ爆発,あるいは単に状態爆発といいます.

莫大な数の状態があるということは設計段階での考慮やテストによる網羅的な検証が難しくなるということを意味します.

(2) 非決定性

2つ以上の構成要素が並行に動作する場合,全体としての処理の実行順序に任意性があります.その結果としてシステムが同じ状態にあり,かつ外界も同じ状況にあるにも関わらず,実行のたびに振る舞いが異なるという性質が現れます.システムが持つこのような性質のことを非決定性といいます.

非決定性はシステムの検証に重大な影響を及ぼします.同じ状況設定をしても振る舞いが異なる場合があるのですから,1度のテストが成功しても検証できたとはいえません.非決定性は確率的な現象ではないこともあるので,テストの回数を増やしても信頼性を高めることができない場合があります.たとえばテスト環境で1万回テストして発生しない問題が,リリース環境では100%発生するなどということがありえます.

(3) デッドロック

2つ以上の構成要素が相互作用を行う場合,応答待ちの要求が循環してどれも動けなくなるという現象が起こりえます.これをデッドロックといいます.

(4) ライブロック(発散)

2つ以上の構成要素が進捗のない相互作用を繰り返し続ける状況が発生し,結果としてそれ以外の構成要素やシステム外部からの要求を受け付けなくなるという現象が起こりえます.これをライブロックまたは発散(divergence)といいます.

§ § §

以上のように並行システムには他のシステムとは異なる特徴があります.要求を満たす信頼性の高い並行システムを設計できるようになるためには,これらの特徴について学ぶ必要があります.

2. 並行システムの理論である CSP を学ぶ

並行システムの設計を行うにあたっては,計算とは別に相互作用に基づいて振る舞いを記述したり比較したりするという新しい側面と,非決定性やデッドロックのように問題となりうる性質とに対処するための理論が必要になります.ここでいう理論の役割は文章問題に対する方程式,あるいは物理学の問題に対する微分方程式のようなものです.問題を記述し,解を導出し,結果を吟味するための理論です.

並行システムを記述し,その性質を議論するための理論には,オートマトン,ペトリネット,プロセス代数などさまざまなものがあります.本トレーニングではプロセス代数の中の1つであるCSP (Communicating Sequential Processes) を採用します.

CSP理論を学ぶと次のことができるようになります:

  1. 並行システムやその構成要素の振る舞いを相互作用に基づいて記述することができるようになります.
  2. 2つの振る舞いを相互作用に基づいて比較できるようになります.典型的には仕様とシステムの振る舞いを比較することができるようになります.
  3. 前項で説明した問題となりうる非決定性等の性質に対して,理論的に対処することができるようになります.具体的には非決定性があっても問題がないことを論証したり,デッドロックが存在しないことを証明したりすることです.

2番目の項目について補足をします.「仕様とシステムの振る舞いを相互作用に基づいて比較する」ということは自明なことではありません.第1にシステムの振る舞いが仕様を満たしているということは,仕様で規定された振る舞いとシステムの振る舞いが同じであるという意味ではありません.一般に仕様では許容範囲としての意図的な選択の幅が用意されており,システムの実装ではその範囲から選択を行うことになります.したがって仕様と実装の振る舞いの関係は対称ではありません.CSP理論ではこの関係が数学的に厳密に定義されており,詳細化関係といいます.

第2に比較をどのような基準で行うかという点でいくつかの選択肢があります.言い換えると詳細化関係にはいくつか種類があるということです.本トレーニングではこれらのうちで応用上重要な2つの基準について解説します.1つはシステムの振る舞いを外から観たときに観測できる相互作用の系列に基づいて比較を行う方法で,トレース方式1といいます.この基準を使うと,システムの振る舞いが仕様で規定されている振る舞いの範囲に収まっているかどうかを確認することができます.平たくいえば「仕様がやってもよいということだけをやっているかどうか」を確認できます.システムがもつこの性質を安全性 (safety) といいます.トレース方式では安全性の確認ができるということです.

もう1つは非決定性まで考慮したより精密な基準で比較を行う方法で,安定失敗方式といいます.この基準を使うと「仕様がやらなければならないということをやっているかどうか」を確認できます.システムが持つこの性質を活性 (liveness) といいます.安定失敗方式では安全性に加えて活性の確認ができるようになります.

まとめると,CSP理論を学ぶことによって,並行システムを開発する上で重要な概念である詳細化関係および安全性・活性という性質と,それを確認するための2つの方式であるトレース方式・安定失敗方式を習得することができます.

3. 並行システムの振る舞いをモデル化し CSP 理論に基づいて検証するツールの使い方を学ぶ

CSP理論があれば原理的には設計の問題を机上で解決することができます.しかし現実のシステム設計では作業の量が膨大ですから,すべてを手作業で実行することは困難です.量が多ければ手作業では間違いを犯す可能性もあります.

加えてCSP理論は数学的な理論なので,形式的な記号操作に慣れていない人にとってはシステム開発とのギャップがあり,とっつきにくいところがあります.

この2つの課題を解決するために本トレーニングでは SyncStitch というツールを使います.SyncStitch は CSP 理論に基づいたツールで,以下のことができます:

  1. システムや構成要素の振る舞いを状態遷移図として記述することができます.
  2. CSP 理論に基づくトレース方式・安定失敗方式の2つの方式で振る舞いを比較することができます.
  3. デッドロックやライブロックがあるかどうかを調べる機能があります.

本トレーニングでは,一般によく知られた状態遷移図という表現形式を用いて,ツールを使いながらCSP理論の概念を学んでいくというアプローチを採ります.そして概念を習得できた後で,CSP理論本来の形を解説し,より理解を深めてもらいます.

4. 並行システムの実装方法について学ぶ

本トレーニングでは並行システムを実装する3つの方法について説明します:

  1. CSPライブラリを使った実装
  2. 同期プリミティブを使った実装
  3. 不可分操作を使った実装

CSPライブラリを使った実装

CSP理論に基づいて設計した並行システムを実装するもっとも直接的な方法は,CSPをサポートするプログラミング言語やライブラリを使うことです.この方法の利点は考え方が1つに統一できること,設計モデルから実装への変換がほぼ機械的であり容易であること,対応関係が明確なので実装の際に問題が混入する可能性が少ないことです.欠点としては,既存システムの構成が制約となって採用できない場合があります.

本トレーニングではMCCSPというC言語用のCSPライブラリを使います.このライブラリの特徴はシンプルな実装で内部を理解しやすく,改造して実験できるなど教育向けに適しているという点にあります.構成が簡単なMCCSPで1度実装方法を習得すれば,より高速で高度な機能を持つライブラリにステップアップすることはそれほど難しくないので,効率のよい学習順序であると考えます.

同期プリミティブを使った実装

共有メモリ型のアーキテクチャ上でオペレーティングシステムが提供するミューテックスやセマフォといった同期プリミティブを使って並行システムを実装するという手法は広く使われています.したがってそのような実装方法においても信頼性の高いシステムが構築できるようにすることが重要です.そこで,同期プリミティブの振る舞いをCSPでモデル化し,それを使ってシステムの検証を行った後に実装をするという方法を解説します.

不可分操作を使った実装

マルチコア/メニーコア時代に入り,システムの並列性を高めて全体のパフォーマンスを上げる技術は今後ますます重要になります.そのためのプリミティブとして Test and Set (TAS), Compare and Swap (CAS), Transactional Memoryなどのいわゆる不可分操作(アトミック操作)の利用が重要になります.その応用の1つとしてロックフリーアルゴリズムを例にとり,不可分操作をモデル化し,検証してから実装する方法について解説します.

© 2013-2017 PRINCIPIA Limited