P3Sを使った検証実験の結果
前述の手法とそれを実現するP3Sライブラリの検証実験として、まず、リアルタイムOSが動作するArm社のMbedボードで実機の並行システムを構築します。次に、同じ並行システムをP3Sでモデル化します。実機とモデルで同じシナリオを実行し、性能を検証します。
Mbedによる実機並行システム
MbedはArm社の提供するマイコンボードの総称で、「mbed OS 5」というリアルタイムOSベースのOSが動作します。プログラムはC言語/C++で実装し、オンラインIDEでコンパイルすることができるため、さまざまなプラットフォームで利用可能です。
対象とするシステムでは、mbed LPC1768というボードを2枚用意し、1枚はCPUとして複数のタスクを走らせ、もう1枚はハードウェアアクセラレータとして利用します。互いにGPIOピンで接続し、並行システムを構築します（図5）。
対象としている並行システムについて簡単に説明します。図6は並行システムの全体像です。
CPU側では、3つのタスク優先度の異なるタスクとISR（ハードウェアアクセラレータ側からの割り込みハンドラ）を走らせ、共有資源としてメモリプール、タスク間の通信用にメッセージキューを用意します。3つのタスクと1つのISRの動作シナリオとして、それぞれ表1の通り定義しました。
| タスク | 動作 |
|---|---|
| タスク1 | メモリプールからメモリを確保して、適当なデータをコピーしタスク2にメッセージキュー経由でデータ（ポインタ）を渡す。 |
| タスク2 | タスク1からデータを受け取り、ハードウェアドライバとしてハードウェアアクセラレータ側にGPIO経由で処理依頼をして、ISRから完了通知を受けるとタスク3にメッセージキュー経由でデータを渡す。 |
| タスク3 | タスク2からデータを受け取り、データのメモリを解放する。 |
| ISR | ハードウェアアクセラレータ側からGPIO経由で処理の完了通知を受けると、タスク2に完了通知を送る。 |
ハードウェアアクセラレータ側では、CPU側から処理依頼を受けると任意のデータに対して特定の処理、今回はTCPのチェックサム演算のような処理をさせ、処理が終わるとCPU側にGPIO経由で完了通知信号を出します。なお、検証用のシステムなので、並行性の点で互いに関連はしていますが、処理の内容にはあまり意味はありません。
メモリプールサイズやメッセージキューサイズ、データサイズ、処理させる回数、各タスクのタスク優先度等をパラメータとし、これらのパラメータを変えながら複数のパターンで実行時間を計測します。
P3Sによる並行システムのモデル化
P3SではこのMbed2枚の並行システムをモデル化します。モデル化の一例を示します。
まず、ソフトウェアタスクをモデル化します。ソフトウェアタスクをモデル化する際に、連続的に処理する区間（OSから強制的にディスパッチはされ得るが、タスク内では状態を変えない処理区間）をひとつの遷移とします。例えば、メモリプールに空きがあるかどうかによって処理を継続する（RUNNING状態を維持する）か、待つ（WAITING状態に変化する）かが決定されるようなポイントでは新たな状態を設けて、前後の処理を異なる遷移として分けます。
遅延時間については、あらかじめ実機でプリミティブな処理（データサイズに応じたメモリコピー時間やチェックサム演算の計算時間等）の時間を計測しました。性能検証において、状態遷移時の遅延時間の設定は大きな課題のひとつです。実際の開発現場では、過去の実機のデータやクロック周波数等から推測した値を使います。今回は実機の計測値を使うため、少しズルいと感じられるかもしれませんが、並行性検証の実証実験と考えてご理解ください。
図7はタスク1のメモリプールからメモリを確保し、確保できたらデータをコピー、メッセージキューが空いていればタスク2にデータを渡す、という処理部分のプログラム（左側）とそれをモデル化した時間オートマトン（右側）の一部です。
時間オートマトンにおけるFreePoolやFreeQueueといった変数はプログラム中には出てきませんが、それぞれメモリプールの空き領域数とメッセージキューの空きキュー数を表しています。これらは、パラメータとしてあらかじめ設定しておきます。
メモリプールからメモリを確保する状態でFreePoolが0の場合や、タスク2にデータを渡す状態でFreeQueueが0の場合はWait状態に入ります。遷移の上の青い数字は遷移にかかる遅延時間（マイクロ秒）です。
次に、モデル化した時間オートマトンをP3Sでモデルコードとして実装します。ハードウェアアクセラレータモデルを例に説明します。
図8はハードウェアモデルの時間オートマトン（左側）と、その中の遷移をP3Sで実装したモデルコード（右側）です。
前述した通り、遷移クラス（Trans）はあらかじめP3Sライブラリでテンプレートのクラスとして定義されており、それを継承して遷移クラスを作成します。遷移にかかる時間や遷移条件、同期処理等必要な機能をオーバーライドして実装していきます。P3Sモデルコードでは、チェックサム演算処理の機能については一切実装する必要はありません。必要なことは演算にかかる時間を設定することだけです。これが機能の捨象です。
作成したモデル、3つのタスクモデルと1つのISRモデル、ハードウェアモデルの計5個のプロセスをシミュレータ部で走らせ、実機環境と同様にパラメータを変えながら複数のパターンで実行時間を計測します。
実機とP3Sでのシミュレーション結果との違い
パラメータのパターンに対応する実機とP3Sモデルの計測結果を表2にまとめました。
精度は実機の計測結果を100とした際のモデルの計測結果の割合（％）を示します。誤差は最大でも10％未満に抑えられており、計測対象システムが単純で小規模である点を考慮してもそれなりの精度が確保できました。特にタスク優先度の変化にうまく追随できているため、並行性の検証といった点で本手法の有効性が確認できたと考えています。
P3Sは機能としてはまだまだ不十分です。UPPAALのようにタイミングを時刻の範囲で指定できませんし、形式検証等の機能もありません。それでも、開発の初期段階での簡易的な性能検証を低コストで実施できる点では役に立つといえます。今回の実証実験で実装したモデルコードやMbedでの実行コード、P3SライブラリはGitHubで公開 しています。
設計プロセスにモデル化による検証を組み入れる
本稿では、ハードウェアアクセラレータの開発や導入時に、事前に並行システムの性能を検証する必要性と課題、時間オートマトンを用いたソフトウェアとハードウェアのモデル化および検証する手法、それを具現化するライブラリについて紹介しました。本手法やツールは、複数のプロセスが走るシステムでプロセスの優先度やイベント等に応じてプロセスの切り替えが発生するようなシステムであれば、ハードウェアを含めないソフトウェアの事前検証だけでも用いることができます。
今回紹介した手法では、性能を検証するという目的に合わせ、機能を捨象しました。オートマトンはシステムをあらゆるレベルの抽象度でモデル化できる非常に有効なツールですが、モデルで何を検証したいか、何を表現したいかといった目的に合わせ、捨象すべき要素と残すべき要素をはっきりと決めることが重要です。
本稿を読んで、性能検証に限らず何かをモデル化することに興味を持っていただき、モデル化する際のヒントとなればうれしいです。
トップエスイーについて
「トップエスイー」は、国立情報学研究所で提供している、社会人エンジニア向けのソフトウェア工学に関する教育プログラムです。トップエスイーでは講義や制作課題を通して、最先端の研究成果や現場で得られた知見が蓄積されてきました。その「アウトカム」、つまり成果やそこに至る過程を紹介し、現場のエンジニアの方々に活用していただける記事を連載しています。トップエスイーでは、モデル検査の基礎から応用までを学習できる講義を用意しています。数学的な基礎や記述言語等の習得はもちろんですが、現場で使えるモデル検査の事例や知識も含めて習得できます。
