PRINCIPIA
ProductsDocumentationsAbout Us

SyncStitch: 並行システムのモデル化・検査ツール

概要

SyncStitch はソフトウェアシステムの動作に関する設計を支援するツールです。SyncStitch を使うと、開発の対象であるシステムやその構成要素であるコンポーネントの動作をモデル化し、期待通りに動くかどうか検査することができます。

マルチコアの時代に入り、マルチコアを生かしたソフトウェアの需要は高まっています。一方で、マルチコア、マルチスレッドを使用するソフトウェアの設計は難しいといわれています。その理由の1つは、各コアやスレッドが独立して動作するので、システム全体として取りうる状態の数や動作の組み合わせが指数関数的に増えるからです。結果として、想定外の動作が含まれている可能性は高くなり、人手による検査も困難になります。

加えて、シングルスレッドにはない、マルチスレッド特有の問題というものが知られています。デッドロック、ライブロック、あるいは非決定性などです。デッドロックとライブロックはシステムが機能を停止してしまう深刻な問題です。非決定性は再現性の低い、テストでは発見できないバグの原因となります。

SyncStitch を使うと、このような問題に対処することが可能になります。SyncStitch 上で各スレッドの動作を状態遷移モデルとして記述すると、それらを合成したシステム全体として動作を求めることができます。その上で、動作をシミュレーションしたり、デッドロックやライブロックがないことを検査したり、あるいは別途作成した仕様のモデルと比較することで想定外の動作が含まれていないことを検査したりできます。[*1]

より詳しい情報につきましては、SyncStitch ユーザーガイドをご覧ください。

SyncStitch は並行プロセスの理論である CSP [Wikipedia] を基礎にしています。CSP をご存知の方は、このページの下にあるこちらの説明もご覧ください。

SyncStitch の対象範囲

SyncStitch はソフトウェア開発のプロフェッショナル、またはプロフェッショナルを目指す方のためのツールです。SyncStitch は仕様化から設計まで、広い範囲で使うことができます。システム全体の設計だけでなく、コンポーネントの設計のために局所的に使うこともできます。並列アルゴリズム、マルチスレッドアルゴリズムの検証など、実装に関する側面を扱うこともできます。

SyncStitch それ自体は特定の分野に特化したツールではありません。プログラムの動作をモデル化し検査する汎用のツールです。したがって利用する方それぞれの専門領域において、専門的知識と技術を活用する際に、動作の側面に関する品質を向上させるブースターとしてご利用いただけます。

SyncStitch は開発チーム内でのコミュニケーションツールとして利用することができます。例えば、まずシステム全体の設計責任者を中心に、システムをコンポーネントに分割し、それぞれの動作をモデル化します。各動作は、これらの合成系であるシステムの動作が仕様を満たすように定めます。コンポーネント担当者は担当するコンポーネントのモデルを満たすように内部を設計・実装します。なんらかの理由でコンポーネントの動作を修正する必要が生じた場合、修正したモデルの版を作成すれば、SyncStitch を使ってすぐに仕様への影響を調べることができます。チームメンバ全員が最新のモデル全体を持ち、いつでも仕様との整合性を確認できるので、局所的な修正が後になって問題を起こすというようなことを避けることができます。

SyncStitch を次のような方にお勧めします:

SyncStitch の主な機能

SyncStitch の持つ3つの主な機能についてご紹介します。

動作のモデル化

SyncStitch ではコンポーネント、またはプロセス、スレッドなどの動作を、次の2種類の形式でモデル化する(記述する)ことができます。

プロセス式とは、プログラミング言語で記述されたプログラムのように、独自の言語で動作を記述したものです。SyncStitch では、上図のように、プログラミング言語 Scheme(Lisp の方言の1つ)を拡張した言語を使用します。

この言語はイベントの発生やチャネル通信などの言語要素を持っていて、コンポーネントの動作と、コンポーネント間の相互作用を記述することができます。加えて、複数のコンポーネントを合成してシステムの動作を求める演算子を持っています。

モデルのシミュレーション

SyncStitch 上で作成したモデルは、すぐに実行して見ることができます。これを一般にモデルのシミュレーションといいます。モデルのシミュレーションは、いわゆるプログラムの実行と異なり、実行過程をツリー状に表示するという形で行います。こうすることで、実行の前後関係や分岐の様子を俯瞰することができます。

システムやコンポーネントが実行の過程でとりうる各状態において、可能な遷移や変数の値、内部構造などを調べることができます。

モデル検査

SyncStitch は4種類の検査機能を持っています。

デッドロック検査とライブロック検査は、それぞれデッドロック、ライブロックがあるかどうかを調べる検査です。テストと異なり、問題の発生する可能性があれば必ず発見されます。安全性とは、何か悪いことが起こらないという性質です。許容される範囲の動作をモデルとして指定すると、システムの動作がその範囲に収まっているかどうかを検査します。最後のものは文字通り、設計したシステムが仕様を満たしているかどうかの検査です。仕様もまたモデルとして記述します。

いずれの検査においても、SyncStitch は対象として指定されたシステムのすべての状態と動作をチェックします。したがって人手によるテストとは異なり、検査の漏れはありません。[*2][*3]

検査の結果、違反が見つかった場合は、シミュレーションと同様に問題のある箇所を表示し、分析することができます。これによって問題解決のヒントを得ることができます。原因が特定できたならば、モデルを修正し、すぐに再検査を行うことができます。このように SyncStitch を使うと、効率よく設計を行うことができます。

CSP をご存知の方へ

  • SyncStitch は CSP に基づいた、いわゆる詳細化検査ツールの1つです。
  • プロセス記述(モデル化)は状態遷移図またはプロセス式で行うことができます。
  • プロセス式は CSPM ではなく、プログラミング言語 Scheme をベースとした独自のものになります。
  • サポートしている意味論モデルはトレースモデルと安定失敗モデルです。失敗発散モデルはサポートしていません。
  • 詳細化検査の他に、デッドロック検査と発散検査を行うことができます。
  • プロセスのシミュレーションを行うことができます。実行過程は計算木として表示することができます。
  • 検査結果もシミュレーションと同様、計算木として表示することができます。
  • プロセスの終了は distributed termination です。
  • tau 遷移と tick 遷移を両方持つ状態は、 tick 以外を拒否します。
  • 時間を扱うことはできません。(tock 方式を除きます)

ご注意

[*1] SyncStitch 上で作成するモデルは、検査したい動作に着目した抽象モデルです。実際のシステムで使用するプログラムを記述するわけではありません。実際のプログラムは、抽象モデルを参考に、別途作成する必要があります。この作業は SyncStitch の対象外となります。
[*2] 検査は指定された仕様に対する相対的な比較として行われます。したがって検査の結果、違反が見つからなかったとしても、仕様に問題があれば、システムにも問題がある可能性があります。すなわち、違反がないことは必ずしもバグがないことを意味しません。また、検査コードの品質には最大限の努力を払っておりますが、絶対の保証はいたしかねることをご理解の上でご使用くださるようお願いいたします。
[*3] 検査できるモデルの規模はメモリの大きさによって制限されます。検査で使用するメモリの大きさは固定されており、拡張することはできません。すなわち、より多くのメモリをPCに搭載しても、検査できるモデルの規模は変わりません。
© 2013-2017 PRINCIPIA Limited