Explicit-time method

(1)

2011 年度修士論文

Explicit-time method に基づくモデル検査器 SLIM の

リアルタイムシステムモデル検査器への拡張

提出日： 2012 年 1 月 27 日指導：上田和紀教授

早稲田大学大学院基幹理工学研究科情報理工学専攻

学籍番号： 5110B063-9

清水涼子

(2)

概要

リアルタイムシステムは，システムの挙動に関して実時間制約をもつことを特徴としている．これらの多くは手作業による検証が容易でないことから，検証ツールによるサポートが重要視されている．リアルタイムシステムへのモデル検査の適用は従来，時間オートマトンをベースとしたモデル検査の研究が主になされてきた．既存の主要なリアルタイムシステムに対応したモデル検査器は，システムを時間オートマトンで表現するための特別なモデリング言語を用意しており，モデル検査のアルゴリズムもそれに対応したものとなっている．

一方，explicit-time method とは，リアルタイムシステム向けでない通常の並行言語・

論理・モデル検査器の上で，リアルタイムシステムを記述・検査するための手法である．

これは，モデリング言語上で現在時刻を明示的に表す変数とそれをインクリメントしていくプロセスを用意することで，システムのクロックをプログラム上に実装するというものである．これは，時間オートマトンをベースとした手法で現在時刻が隠蔽されている点と対照的であることからこう呼ばれている．

LMNtalは多重集合による階層グラフの書き換えに基づく並行言語モデルである．グラ

フ構造は，アトム・リンク・膜・リンクから構成される．リンクはアトム同士を接続し，

膜で階層構造をなすことができる．この階層グラフ構造をルールが書き換えていくことにより，処理が進行する．

SLIMはLMNtalの実行時処理系であり，共有メモリ並列計算機向け並列モデル検査機

能を有する．この並列モデル検査機能が近年備わったことにより，大規模なモデル検査が可能になっており，SLIMの検証分野への応用が期待されている．しかし現在のLMNtal またはSLIMでは，言語仕様上でリアルタイム性のモデリングの為の言語環境の整備や，

リアルタイムシステム向けのモデル検査はサポートされていない．

今回の研究では，explicit-time methodを使用してLMNtalでリアルタイムシステムの例題を記述して，SLIMでモデル検査が行えることを確認した．その結果，この手法を

LMNtalに適用する際に現在のLMNtal言語仕様では記述できない部分があることがわ

かった．そこで，explicit-time methodを使用したリアルタイムシステムをLMNtal で簡潔に記述するためのLMNtalの拡張言語を設計・実装した．最後に，既存のリアルタイムシステム向けモデル検査ツールや，他のモデル検査器と同様の例題を用いて時間性能を比較することにより，SLIMへのこの手法の適用を評価した．

(3)

図目次

2.1 LMNtalの構文 . . . 3

5.1 拡張言語処理系の処理 . . . 16

6.1 ﬁscher.lmn . . . 18

6.2 Fischerのアルゴリズム . . . 18

6.3 FischerのアルゴリズムのTickアルゴリズム . . . 20

6.4 leader.lmn . . . 24

6.5 Leader election protocolのTickアルゴリズム . . . 24

7.1 Fischerのアルゴリズムのsafetyの実行時間 . . . 26

7.2 Fischerのアルゴリズムのlivenessの実行時間 . . . 28

7.3 Leader election protocolのsafetyの状態数と実行時間[s] . . . 29

iv

(6)

表目次

7.1 実験環境 . . . 25

7.2 Fischerのアルゴリズムのsafetyの状態数と実行時間[s] . . . 26

7.3 Fischerのアルゴリズムのlivenessの状態数と実行時間[s] . . . 27

7.4 Leader election protocolのsafetyの状態数と実行時間[s] . . . 29

v

(7)

1

第 1 _章

序論

1.1 研究の背景と目的

リアルタイムシステム（リアルタイムアルゴリズムやリアルタイムプロトコル等を含む）は，システムの挙動（反応時間や計算時間等）に関して実時間制約をもつことを特徴としている．ミッションクリティカルシステムの多くが実時間制約をもつことや，実時間を巧みに利用したアルゴリズムやプロトコルの手作業による検証が容易でないことから，

リアルタイムシステムを扱うには，適切なモデリング・検証ツールの支援がきわめて重要である．

リアルタイムシステムのモデリングには，大きく分けて implicit-time method と explicit-time method とがある．Implicit-time method とは，時間の概念が組み込まれた表現体系を利用するものである．時間オートマトンがその代表格であり，既存のリアルタイムシステムをサポートしているモデル検査ツールの多くは時間オートマトンをベースとしたモデル検査を行っている．一方，explicit-time method とは，リアルタイムシステム向けでない通常の言語・論理・モデル検査器の上で，現在時刻を明示的に表す変数を用いてモデリングや検証を行うものであり，時間オートマトンをベースとした手法で現在時刻が隠蔽されている点と対照的である．DIVINEへの適用・改造例[15]や，NuSMV に適用して産業界で実際に使用された例[14]もある．

これらの中間に位置する手法として，リアルタイムシステム向けでない通常の言語・モデル検査器でリアルタイムシステムの記述をサポートする試みも行われてきた．例として，代表的なモデル記述言語と検査器であるPromelaとSpinのいくつかのリアルタイム拡張があげられる[12][3][11]．この中で，DTSpin[3]は，タイマー変数とそれをインクリメントするプロセスの導入という簡易な実装からなっている点が explicit-time method

(8)

1.2 論文構成 2 と類似している．

本論文の目的は，著者のグループで開発されてきたモデリング言語LMNtal[13]とそのモデル検査器SLIM[4]の上でのexplicit time methodによるリアルタイムモデル検査について，方式の検討と評価を行うことである．Explicit time methodによるモデル検査については，Lamport がモデリング言語TLA+とモデル検査器TLCを用いて詳しく検討しており[5]，本論文ではLamportの結果との比較検討ができる形で例題選択や性能評価を行うこととする．

1.2 論文構成

本論文では第2章に LMNtal 言語の概要に付いて述べ，第3章で LMNtal 実行時処理系であるSLIMとそのモデル検査機能について述べる．第 4章でexplicit-time method についてモデルへの導入方法とモデル検査への適用についての考え方を説明する．第5章では，explicit-time methodをLMNtalプログラムで記述するために用意したLMNtal 拡張言語の仕様を説明する．そして，第6章で，explicit-time methodを使用したリアルタイムシステムの例題のLMNtalへのエンコードを紹介する．第7章でLMNtalで記述したリアルタイムシステムの例題の時間性能を他のツールとの比較により評価する．最後に第8章で本研究のまとめと今後の課題について述べる．

(9)

3

第 2 _章

LMNtal _言語解説

ここではモデル検査器SLIMのモデリング言語であるLMNtal言語について解説する．

ここでは本論文を読むに当たって必要な事項についてのみ説明する．

2.1 LMNtal の基本構成要素

アトムはアトム名と 0個以上の順序のついた引数からなり，この引数がリンクを通じて他のアトムに繋がっている．リンクとはこのアトムの引数を一対一に接続するものである．膜はアトムの多重集合を囲むことができる．また膜は入れ子構造をなすことができ，

アトム，リンク，膜によって階層グラフが形成される．この改装グラフ構造をLMNtal ではプロセスと呼ぶ．プロセスの書き換え規則をルールと呼び，構造を動的に再構成できる．

2.2 LMNtal の基本構文

(プロセス) P := 0 | p(X1, . . . , Xm) | P, P | {P} | T:-T

(プロセステンプレート) T := 0 | p(X1, . . . , Xm) | T, T | {T} | T:-T | @p | $p

図2.1 LMNtalの構文

LMNtalの構文は図2.1のように定義される．ただし本論文で使用しない構文要素は省

いている．Xi はリンク名，pはアトム名であり，P はプロセスである．具象構文ではリンクは大文字から始まる識別子，アトム名はそれ以外の識別子で表現する．T はプロセス

(10)

2.3 LMNtalの省略構文 4 の書換え規則の表現に用いるプロセステンプレートであり，局所文脈 (特定のセルの内部での文脈) を扱う機能をもつ．

0 は中身のないプロセス，p(X₁, . . . , X_m) はm価のアトム，P, P はプロセスの並列合成である．{P}はセルと呼び，プロセスを膜 { } によってグループ化したものである．

ルールT :-T は，膜が形成する階層構造の同じ場所に置かれたプロセスを適用対象とする．

プロセスは，同じリンク名が2回を超えて出現してはならないというリンク条件tを満たさなければならない．さらに，個々のルールの各リンク名は，そのルール内にちょうど 2回出現しなければならない．

予約アトム名=はコネクタと呼ばれ，X=Y はリンクX の一端とY の一端とを相互接続する．ルール文脈は膜の中のすべてのルールの多重集合とマッチし，プロセス文脈は膜の中のルール以外のプロセスのうち，明示的に指定されていないもの全体とマッチする．

2.3 LMNtal の省略構文

LMNtalでは階層グラフ構造やルールが簡潔に記述できるように，いくつかの省略構文

を用意している．

• 0価のアトムの括弧()は省略できる．たとえばa()はaと略記できる．

• 木構造のデータを他言語と同様に記述するための項記法が用意されており，アトム aの第k 引数として，(リンク名のかわりに) 最終引数を省略したアトムbを書くと，aの第k 引数とbの最終引数とがリンク接続されているものとみなす．たとえばf(a,b)はa(A),f(A,B),b(B) と等しい．

さらにLMNtalの意味論はa(A),f(A,B),b(B)はa(A),f(A,B),B1=B,b(B) と等価であると定めているので，これに省略記法を3回適用することでb=f(a)もこれらと同じ構造を表すことがわかる．

2.4 LMNtal の拡張構文

2.4.1 ルールの拡張

LMNtalはルールに対して以下の構文の拡張を施している．

(11)

2.4 LMNtalの拡張構文 5

• ルールは以下の構文のようにガードをもつことができる．

Head:−Guard|Body

• ^{ルールの先頭に}rulename@@の形を付加してルールに名前をつけることができる．

2.4.2 型付きプロセス文脈

実用プログラミング言語では、数値型をはじめとする基本的な型とその基本演算を提供することは不可欠である．LMNtalにおける数値は，8(X)のような1価アトムで表現する．引数はその数値を参照するプロセスにつながる．LMNtalでは，数値もプロセスであり，数値型をはじめとする基本型はプロセス型(プロセスに対する型)の一種である．アトムが整数型などの基本型に属するかどうかの検査や基本型に対する演算をを指定するた

めに，LMNtalでは，型付きプロセス文脈という拡張構文を導入している．通常のプロセ

ス文脈のマッチする相手が膜(階層構造)によって決まるのに対し，型付きプロセス文脈のマッチする相手はグラフ構造 (接続構造) とグラフ中のアトム名によって決定される．

マッチする相手を指定するには，ガード付きルールを使用して，ルールの適用のための付帯条件を指定する．ガードを持つルール，

p(X), $n[X] :- int($n), $n>0 | p(Y), $n[Y], p(Z), $n[Z]

は，1価アトムpが正整数アトムにつながっている場合，その構造の複製を作る．ガード条件int($n)は，$n[X]が整数アトムを表す型付きプロセス文脈(int型)であることを求めている．ガード条件にはプロセス型以外のものも書くことができ，上の例では$n>0 はその整数値が正であることを求めている．条件$n>0は条件int($n)を含意するので後者は省くことができる．さらに型付きプロセス文脈をリンクと同じ記法で書くことも認めているので，上記のルールは p(N) :- N>0 | p(N),p(N)と書いてもよい．

ガード部に指定できる int 型に対する制約として，プロセス型の他に，‘=:=’，‘=\=’

制約がある．‘=:=’制約は二つのプロセス文脈に対して等しい数値のときのみ適用され，

‘=\=’ 制約は等しくないときのみ適用される．さらに大小比較演算として‘<’，‘=<’，

‘>’，‘>=’があり，両辺には四則演算も記述できる．

(12)

6

第 3 _章

LMNtal _処理系と SLIM _モデル検

査器

3.1 LMNtal 処理系概要

LMNtal処理系はコンパイラと実行時処理系からなる．

コンパイラは与えられたソースコードを後述する LMNtal 中間命令列へと変換する．

この中間命令列を入力とし，解釈実行するのが，LMNtal実行時処理系である．現在は Java 言語による処理系と C言語によるSLIM が存在する．

3.1.1 Java 言語による処理系

Java言語による処理系はコンパイラと実行時処理系が一体となった処理系である．この処理系はJavaで書かれているため，入出力，ソケット通信，GUI等の機能を提供するモジュールが標準ライブラリとして提供されている．また，多言語インターフェースとしてJavaのコードが書けるなどの拡張機能がつけられている．

3.1.2 SLIM モデル検査器

Java言語による処理系に対し，軽量かつ高速なLMNtal実行処理系としてC言語で開発したSLIM(Slim Lmntal IMplimentation)が存在する．SLIMは，並列実行や検証への応用を見据え，高速かつ軽量な実効性能を目的としている．SLIMには，LMNtalプログラムに対して網羅的な実行経路の取得や状態遷移グラフに対するグラフ探索として定式化したオートマトンベースのモデル検査手法を採用し，LMNtalの通常のプログラム実行

(13)

3.2 中間命令列 7 を状態遷移グラフ構築処理へ拡張することで実現した．

オートマトンベースのモデル検査手法とは，状態遷移系モデル(プログラム)の各状態を頂点，状態変化を枝とした状態遷移グラフに対してグラフ探索を行うことで，満たすべき仕様に対する反例検出を行う検査手法である．システムが満たすべき性質の記述に線形

時相論理(LTL)を使用可能であり，LTL式で与えられた性質をシステムが満たすか否か

を検査できる．安全性(safety)の検証では，危険な状態を示す頂点への到達可能性を探索

し，活性(liveness)の検証では，目標となる頂点へ到達しない閉路の探索を行う．

さらに，近年モデル検査の大規模化と高速化が重要課題となるなか，SLIMは共有メモリ計算機向けの並列化が施された．この並列化により，検証可能な規模は約10倍拡大すると共に，約88倍の高速化が達成されている[4]．

3.2 中間命令列

前述したように LMNtalコンパイラはLMNtalプログラムをルール毎にLMNtalの中間命令列へと変換する．この中間命令列はLMNtalプログラムのルールと一対一に対応され，一本の中間命令列は階層グラフの書き換えの手順を示している．実行時処理系はこの中間命令語を一語づつ実行することにより，LMNtalプログラムを実行している．

中間命令語は制御命令と非制御命令の 2つに分けられる．制御命令は中間命令列の実行の準備，制御の移動，終了処理などをつかさどる．非制御処理はアトムや膜の取得，生成，除去，リンクの繋ぎ直し，型検査などを行う．LMNtalコンパイラには，中間命令列に対する最適化器が実装されており，本論文で中間命令列を取り上げる場合は，原則としてこの最適化器によるレベル3の最適化(実行時オプション-O3)を施した命令列とする．

次節にて，本論文にて取り上げる制御命令についてのみ説明する．

制御命令spec [formals, locals]

アトムや膜を保持する配列のサイズを仮引数を formals ，実引数をlocals として設定する．初期化作業であるため，spec 命令は命令列の先頭部に生成される．

commit [name, lineno]

ルールの適用に成功したことを意味する．

proceed []

命令列が実行に成功したことを示す．主に命令列の最後に出現する．

(14)

3.3 他言語インターフェース 8

branch [instructions]

命令列instructions を実行し，成功したら適用可能となる．失敗した場合は次の命

令があればその実行に移り，なければ適用不可となる．

3.3 他言語インターフェース

SLIM の他言語インターフェースは，LMNtal プログラムからC言語で実装した関数を呼び出すことができる．これによりLMNtalの構文規則だけでは実現できない，または実現に手間のかかる処理を拡張機能として追加することができる．

3.3.1 atomic ruleset

他言語インターフェースで実装された SLIM の機能の一つにatomic rulesetがある．

これは，複数のルール書き換え処理をインターリーブさせずに1ステップで処理することが可能になる．

(15)

9

第 4 _章

Explicit-time Method

第1.1節で述べたように，explicit-time methodの基本的な考え方は，現在時刻を表す変数nowと，そのnowをインクリメントするプロセスをシステムへ導入し，これらにより時間の経過を制御するというものである．そして，システム中の時間の制約の表現については，システム中のトランジション発生に関する時間の上限値・下限値の場合に分けて以下のように制御する．

• ^{下限値について，}nowの値が下限値より大きいときにトランジション発生を許可する．

• ^{上限値について，}nowの値が上限値を超えるようなインクリメントを許可しない．

4.1 モデルへの時間制約の導入

前節で説明した考え方をいかにモデル中に組み込むかを説明する．

まず，上述のように，モデル中に現在時刻を表す変数 nowを用意する．nowの値はプ

ロセスT ick によってインクリメントされる．T ick の増分は連続時間の仕様の場合は任

意の正の実数であり，離散時間の場合は1である．

時間制約はタイマー変数をすることで表現される．具体的に述べると，τ 秒以内またはそれ以降にあるアクションを発生しなければならないという制約はタイマー変数をτ にセットすることで表現される．タイマーには3種類あり，それぞれexpiration timer, countdown timer, count-up timerと呼ばれる．Expiration timer は，タイマーの値は

T ick によって変化することはなく，now の値とnow +τ の値が等しくなったときにタ

イムアウトとする．Countdown timer はTickによって値がデクリメントされていくタ

(16)

4.2 Explicit-time methodを使用したモデルのモデル検査 10 イマーでその値が0になったときに，タイムアウトとする．Count-up timerはT ick によって値がインクリメントしていくタイマーである．このタイマーは0にセットされ，値がτ と等しくなったときに，タイムアウトが起きる．タイマーは使用されないときは非アクティブ化される．無効化されたcount-up timerとcountdown timerはT ick により更新されない．非アクティブ状態を示す値としては，0，∞,−∞が使用される．選択するタイマーの種類は，モデル検査器によってはcountdown timerかcount-up timerである必要があると述べられてる[5].

あるシステム中のアクション(トランジション・イベント)に関する時間制約は上限制約と下限制約の2種類からなる．下限制約は，アクションA に関する発生条件が最低τ 単位時間真でありつづけるまで，アクションAが起きてはいけない．上限制約は，A の発生条件がτ 単位時間真でありつづけるならば，Aが起きなくてはいけない．

下限制約は，Aの発生条件にタイマーがタイムアウトしていることを条件に含め τ 秒より早く実行されないようにする．非アクティブを示す値を0とすれば，τ 秒またはそれ以上経過したときに実行するという制約を表現するのに便利である．上限制約は，T ick のインクリメントによりその上限制約を侵さないようにT ickの実行条件を加える．つまり，nowの値を現在のcount-down timerの値より小さい値でインクリメントするようにする．上限制約に関してはタイマーの非アクティブ値は∞^{を使用する．}

タイマーの値のセットと非アクティブ化については，T ick のアクションに含める方法と通常のシステムのアクションに含めるの2通りあるが，通常のアクションに含める方が容易であると述べられている[5]．

4.2 Explicit-time method を使用したモデルのモデル検査

モデル検査は状態空間中の状態数が有限である必要があるが，リアルタイムシステムは時刻が上限なく増加し，状態が無限に増え続けてしまう．そこで，Explicit-time method で記述したプログラムに対して，対称性に基づく状態空間削減手法を適用する．多くのリアルタイムシステムは絶対時間ではなく，あるシステムのイベントが発生してからの経過時間に依存しているため，この手法が適用できる．

4.2.1 対称性に基づく状態空間削減手法

対称とは状態空間上の状態の同値関係である．さらに状態の同値関係を拡張して，状態空間中の遷移，ふるまい，ふるまいについての性質についても同値関係を定義することが

(17)

4.2 Explicit-time methodを使用したモデルのモデル検査 11 できる．対称性に基づく状態空間削減手法 (symmetry reduction)とは，ある状態空間S 上に同値関係が定義されているとき，状態の同値類をとることによってより小さい状態空間E を構築し，E に対してモデル検査を行うことである．E の構築は，ある状態について，その状態と同値な状態がまだE に存在しないときのみ，その状態をE に追加することで行われる．このE に対するモデル検査は，次の性質を満たすとき通常のモデル検査と等しい．

S1. (a) 対称な状態sとtについてsが初期条件を満たせばば，tも初期状態を満たす. (b) または,初期条件を満たす状態はただひとつである．

S2. 対称な状態sとs2について，sの遷移先tがあれば, s2 の遷移先でありtと対称な t₂ が必ず存在する．

4.2.2 Time Translation 対称性

いま，time-translation symmetryという対称性を導入する．これは，「状態空間上の2 つの状態について，絶対時間(now)を除いた変数の組全ての値が等しいとき，またそのときに限り，対称であるとする」というものである．まず，状態空間S 上に関数T_d を定義する．Td は全ての状態sと全ての実数dとeについて次の性質をみたす．

• Td(s).now=s.now+d

• T0(s) =s

• T_d+e(s) =T_d(T_e(s))

これを使用してtime translationによる対称性は「ある実数dについてs=T_d(t)を満たすとき，またそのときに限りsとtは対称である」と定義できる．節4.2.1よりこの対称性に対応する通常のモデル検査と等しくなるための条件は次のようになる．

T1. (a) Td(s)が初期条件を満たすならば，またそのときに限りsも満たす (b) 初期条件を満たす任意の状態sとtに関してs.now=t.now

T2. sとT_d(s)について，sの遷移先tがあれば，T_d(s)の遷移先でありtと対称なT_d(t) が必ず存在する．

関数 T d について，Explicit-time であるモデル中の全ての変数に対して定義をしなくてはいけない．変数はnow，タイマー，そしてT ick により更新されない通常の変数がある．通常の変数の値を変えることはないので，T_d(s).v = s.v でなくてはならない．

(18)

4.2 Explicit-time methodを使用したモデルのモデル検査 12 Countdown timerや count-up timer の値ct は，タイムアウトまでの時間を示すため T_d(s).ct = s.ctである必要がある．Expiration timer etの場合はタイムアウトまでの時間はet−nowで表される．T_d がT_d(s).et = s.et+dを満たすとき，またそのときに限り，Td はetがタイムアウトする時間を対称な状態においても維持する．

以上のT_d の定義により，リアルタイム性の要件が絶対時間に依存せず，タイマー変数のみで表せるならば，対称性に基づく状態空間削減手法を行っても通常の状態空間S に対するモデル検査と結果が変わらないと言える．v1, . . . , vmを通常の変数とcountdown timer変数とcount-up timer変数として，et1, . . . , etnをexpiration timerとすれば，time translation対称性による状態空間削減は変数の値hv₁, . . . , v_m, et₁−now, . . . , et_n−nowi から構築される状態空間と等しい．

(19)

13

第 5 _章

lmntal _言語拡張

Explicit-time method を使用したリアルタイムシステムをLMNtalで記述する上で，

便利なLMNtal拡張言語を設計・実装した．このLMNtal拡張言語は機能で分けて2種

類あり，一つは，同一構造のプロセスの記述を簡略化する集合記法風な機能である．二つ

目は，LMNtalプログラムとして記述された複数のルールを中間命令列に変換後，想定し

たように書き変えるマクロ制御構造である．

5.1 LMNtal 拡張言語仕様 5.1.1 集合記法

4.1で説明したT ick は多数のタイマー変数の値を参照したり更新したりすることになるが，その場合に同一構造のLMNtalプロセスを繰り返し記述することになる．そういったときに，この集合記法を使うとプログラムコードが簡略化できる．この集合記法は次のように記述する．

##[[ process | set ]]##

process は任意のLMNtalプロセスで，置換指定子を含めて記述する．set では，同じ名前の置換指定子を使用して集合の定義をする．process に書かれたプロセス中の置換指定子の部分を，set の要素で置換したプロセスを全ての要素について並べる．展開されたプロセスの区切り文字はカンマ,を使用する．置換指定子は任意の英小文字からなる文字列であり，process 中では頭に%をつけて記述する．set は置換指定子をspeciﬁer，集合の要素をe1, . . . , enとすると，

(20)

5.1 LMNtal拡張言語仕様 14 speciﬁer in {e1, . . . , em}

のように記述することができる．整数の集合の場合，比較演算子=<,<,>=,>を用いて n1

<=specifier<= n₂ (n₁, n₂ ∈ Z) のように変域で記述しても良い．また，整数の変域は, specifier= n₁ ..n₂ のように記述すれば，n₁ <=specifier<= n₂ と同義になる．また，記述の手間を省くため，以下のマクロを設計・実装する予定である．

• 予め集合に名前をつけて定義できる構文を設計した．これにより，集合記法中でその都度集合の定義を書かなくても，集合名を書いて置けばよい．

• リアルタイムシステムの例題では時間制約に使用する値をパラメータとして変化させることが多いため，この値を記号定数として扱えるようなマクロを設計する．

5.1.2 中間命令列の制御構造

プロセスT ick(図6.3，図 6.5，第6章で後述)はLMNtalのルールを複数使えば記述できる．ただし，そのままではルールは非決定的にルールが実行されるため，一連のルールは逐次に実行されない．さらに，不可分操作の単位が変わるため，モデル検査時の状態数を他のモデル検査器と揃えることができなくなってしまう．複数のルールを逐次1step で実行する部分に関してはLMNtalのatomic ruleset 機能を使用することもできたが，

atomic ruleset の実装は現在は性能重視でないので，本論文の目的に適さないと判断し

た．そこで，複数のルールを記述し，T ick アルゴリズムと同様の振る舞いをするように中間命令列を書き換えるアプローチを採用した．その手作業を自動化するために以下のような中間命令列操作のための制御構造を用意した．

#If

guardrule

#Then

rule1

...

rulem(m >0)

#End If

これは式中に書かれたLMNtalルールguardrule,rule0. . .rulemの中間命令列の制御命令を次のように書き変える．まず，rulei(1≤i ≤m))をコンパイルして得られた中間命令列instructions_i に対して次の操作をする．まず,spec命令の仮引数の値を保持しておく．

(21)

5.2 LMNtal拡張言語実装 15 その上で，spec命令，commit命令，proceed命令を取り除いた命令列をbranch命令の引数とする．このbranch 命令をinstructions⁰_i とする．次に，guardrule,rule₀. . .rule_m の中でspec命令の仮引数値が最大であるものでそれぞれ guardruleのspec命令の仮引数値で置換して，最後のproceed命令を除き，guardrule’を得る．最後に，guardrule’

とinstructions₁. . .instructions_mを連結し，最後にproceed命令を加える．

このように，書き変えると，guardrule とrule₁, . . . ,rule_m が全体で1stepで実行される一つのルールように扱われる．その上で，guardrule は全体の実行をガード条件的なルールになり，guardrule の適用に成功するとThen以下のルールが並び順に1回ずつ，

それぞれの成否にかかわらずrule_m まで実行される．

5.2 LMNtal 拡張言語実装

拡張言語処理系の実装について説明する．第 5.1.1節で述べた集合要素の展開機能については，LMNtal 処理系のプリプロセッサとして，LMNtal 集合記法部分を展開し，

LMNtalプログラムへ変換する．なお，集合記法の非展開部に関しては，LMNtal拡張言

語処理系中においては単なる文字列として扱い，LMNtalプロセスであるかの解析はしていない．

第5.1.2節で述べた，中間命令列の書き換え機能に関しては，まず，中間命令列制御構造

が書かれている部分をLMNtalソースコードから抜き出す．抜き出した部分をLMNtal コンパイラに渡し，出力された中間命令列を拡張言語処理系にて構文解析し，書き換える．その後，制御構造を除いたLMNtal プログラムをLMNtalコンパイラに渡し中間命令列に変換したものを受け取り，その末尾に先ほど書き換えた中間命令列を追加する．この操作を図で表したものを図5.1に示す．以上の拡張言語処理系の実装にはScalaを使用した．

(22)

5.2 LMNtal拡張言語実装 16

! "

#$

%'&)(*,+.-/103254368719

:<;<=<><?A@

BDCFE<GIHFJLKNMPO<Q#RLS

TVUXWZY#[\]_^a`cb

dfeghji

kl _mn opq

r_m

dfegjhi

klsutvxwXywztx{| n~}

klwzt{|Vwzt{|x

n

F<L<

BDCFEIG<H

a

^bz

TVUXWZY#[\]_^

a

^ZVuVcb

a

^X,''a,Zbb

k

sVtvxwzywzt {|

¡Z¢£¤

wztx{|Vwztx{|x

_¥Z¤x¦ k

dfegjhi

§¨ª©« £ lXk¬lV®x¯¦ ¯~® £ n

} kl¯~®¬

£_°

¯~®¬

£ ¨ n~n

%&F(*,+±-

²³I´8µ!¶

·X%¸z¹º

図5.1 拡張言語処理系の処理

(23)

17

第 6 _章

Explicit-time method _{を使用した}

LMNtal におけるリアルタイムシス

テムの記述

この章ではリアルタイムシステムの例題をとりあげて，実際に Explicit-time method を適用してLMNtalでどのように記述するかを説明する．

6.1 Fischer のアルゴリズム

Fischerのアルゴリズムは，リアルタイムシステムの代表的な例題であり，n本のスレッ

ドに対する排他制御のアルゴリズムである．これから説明するモデルは，文献[5]で説明されているFischerのアルゴリズムをベースに，UPPAAL[7]の公開版のサンプルプログラムに入っているものと同じ振る舞いをするようにしたものである．各スレッドは図6.2 の4つの命令文(a,b,c,cs)を実行していく．共有変数xは，クリティカルセクションに入るスレッドのIDを表す変数であり，どのスレッドも割り当てられないときは，−1が値として代入される．スレッドがa にあるとき，x = −1であれば，bに移り，xに自分の IDを代入する．そしてcの実行時に，xにまだ自分のIDが割り当てられていれば，クリティカルセクションcsに入る．そうでなければ，a にもどる．命令文の実行に関して以下の時間制約が付く．

• bはaの最大δ秒後に実行される(上限制約)

• cはbの²秒後まで実行されない(下限制約)

(24)

6.1 Fischerのアルゴリズム 18

/*

*

*Fisncer’s algorithm

*6 Thereads, parameter(delta) 3.

*explicit-time method ver.

*

*/

//Thread t(id,current position)

##[[t(%i,a)]]| i in 0..5##.

//ubTimer[N] and lbTimer[N]. 1000 represents infinity.

##[[ubTimer(%i)=1000]]| i in 0..5##.

##[[lbTimer(%i)=0 ]]| i in 0..5##.

//share variable.

x(-1).

stmtA@@

t(ID1,a), ubTimer(ID2)=T1, x(-1):- ID1=:=ID2, int(T1)|

t(ID1,b), ubTimer(ID2)=7, x(-1).

stmtB@@

x(X), t(ID1,b), ubTimer(ID2)=T1, lbTimer(ID3)=T2:- ID1=:=ID2, ID1=:=ID3, int(T1), int(T2), int(X)|

x(ID1), t(ID1,c), ubTimer(ID2)=1000, lbTimer(ID3)=7.

stmtC_A@@

x(X), t(ID1,c), lbTimer(ID2)=0:- ID1=\=X, ID1=:=ID2|

x(X),t(ID1,a), lbTimer(ID2)=0.

stmtC_CS@@

x(X), t(ID1,c), lbTimer(ID2)=0:- ID1=:=X, ID1=:=ID2|

x(X), t(ID1,cs), lbTimer(ID2)=0.

CS@@

x(X), t(ID,cs):- int(X)|

x(-1), t(ID,a).

#If

##[[ubTimer(%i)=T%i]]| i in 0..5 ## , \ :- ##[[T%i>1]]|i in 0..5 ##| .

#Then

##[[ (ubTimer(%i)=T1 :- T1=\=1000, T2=T1-1| ubTimer(%i)=T2), (lbTimer(%i)=T1 :- T1>0, T2=T1-1 | lbTimer(%i)=T2) ]]| i in 0..5##.

#End If

図6.1 ﬁscher.lmn

a : wait until x=−1;

b : x:=ThreadID;

c : if x6=ThreadID then goto a;

cs : critical section; x:=−1; goto a;

図6.2 Fischerのアルゴリズム

(25)

6.1 Fischerのアルゴリズム 19 ただし，δ ≤²とする．以上の制約のもとで，csにおけるスレッドの排他制御が正しく行われているかを検証する．

6.1.1 LMNtal における記述

LMNtal で記述したFischerのアルゴリズムを図6.1に示す. LMNtalでnowのような大域変数を表現するときは，変数名を表す単項アトムと変数値を表す単項数値アトムとを結びつけたnow(now) のような構造を用いることとする．また，各スレッドの制御状態をt(ID,Location). (ID ∈ {0, . . . , n}, Location ∈ {a, b, c, cs})として表す．各スレッド用にubTimerとlbTimerというそれぞれタイミングの上限制約用と下限制約用の

countdown timerであるタイマー変数を用意する．以上のプロセスを使用して，スレッ

ドの各文を実行をLMNtalルールによって表現する．また，TickプロセスはルールTick で記述される．例えば，ステートメントaの実行は以下のようなルール stmtA@@で記述する

stmtA@@

t(ID1,a), ubTimer(ID2)=T1, x(-1) :- ID1=:=ID2, int(T1) |

t(ID1,b), ubTimer(ID2)="δ", x(-1).

このルールでは，あるaを実行をしているスレッドは，次のbの実行がδ秒以内であるという制約があるので，ルールのBody部でスレッドのID番号と等しいubTimerの添字の値にδをセットしている．次にステートメントbを表すルールstmtB@@を示す．

stmtB@@

x(X), t(ID1,b), ubTimer(ID2)=T1, lbTimer(ID3)=T2 :- ID1=:=ID2, ID1=:=ID3, int(T1), int(T2), int(X) |

x(ID1), t(ID1,c), ubTimer(ID2)=1000, lbTimer(ID3)="ε".

ルールのボディ部に注目すると，cの実行には，時間の上限制約はないので，ubTimerは非アクティブを表す値1000でリセットしている．同時に，cの実行まで²秒遅延をとるために，lbTimerに²をセットしている．ステートメントcを実行するルールstmtC_CS@@

を下に示す．

stmtC_CS@@

(26)

6.1 Fischerのアルゴリズム 20 if (∀t ∈Thread(ubTimer[t]> d)) then

atomic {

now =now+d;

foreach(t)

if (ubTimer[t] =∞) then ubTimer[t] =∞;

else ubTimer[t] =ubTimer[t]−d;

foreach(t)

lbTimer[t] = max(lbTimer[t]−d,0);

}

図6.3 FischerのアルゴリズムのTickアルゴリズム

x(X), t(ID1,c), lbTimer(ID2)=0:- ID1=:=X, ID1=:=ID2|

x(X), t(ID1,cs), lbTimer(ID2)=0.

ルールのヘッド部で，lbTimerの値が0のときに適用されるようになっており，ステートメントbが実行されてから，Tickにより²以上デクリメントされてからc実行されるのがわかる．ルールstmtC_A@@は同じくcの実行を表しているが，こちらはxに他のスレッドIDが入っていて，クリティカルセクションに入らずa に戻る場合である．ルール CS@@は，タイマーの値を参照したり更新せずに，xを解放しクリティカルセクションから抜けてスレッドの制御状態を初期状態に戻している．

プロセスTickを表すルールTickを用意する．プロセスTickのアルゴリズムについて 6.3に示す．1行目のガード条件は，上限制約を表している．全てのスレッドのubTimer が0 以下の値をとることのないようにしている．2行目はnowの値を正の実数dでインクリメントしている．このアルゴリズムの仕様では連続時間を扱っているが，モデル検査の際には，離散時間を扱うため，dを1で置き換える．4から6行目は全てのタイマーのデクリメントを意味している．それぞれのタイマーについて，タイマーがリセットを示す値のときはデクリメントせず，そのまま変化させない．

6.1.2 モデル検査対応

図6.1のプログラムをモデル検査にかけるため，対称性に基づく状態空間削減手法を適用する．そのためには，整数アトムnow(now) をプログラム上から消去すれば，now を除いた変数の組に対してモデル検査を行うことと同様になる．図 6.1のプログラム中

(27)

6.2 Leader Election Protocol 21 で，now(now)を参照しているルールは，ルールTick@@の中のnow(now)自身を更新するルールのみであるので，nowの更新部分と整数アトムnow(now) をプログラム上から除いても問題ない．

6.2 Leader Election Protocol

Fischerのアルゴリズムはごくシンプルなリアルタイムシステムの例題であったが，こ

の節ではリアルタイムモデル検査器でも扱うのが難しい分散アルゴリズムの複雑さを特徴とした例題を取り上げる．

この例題は Redia Perlman[8]による分散アルゴリズムにヒントを得て作られたものであり，文献[5]において説明されている．このアルゴリズムは，ネットワーク内の各ノード間をリーダーを伝えるメッセージを転送することで，各ノードにリーダーを周知させる．そして十分な時間が経過したときに，各ノードがリーダーとして最小のIDのノードを認識しているかを検証する．この例題の分散アルゴリズム的な特徴は，転送中のメッセージの集合を持ち，各メッセージがその転送時間に関して，別々の上限制約をもっている点やタイムアウトまでの時間を動的に計算する点が挙げられる．

データ構造について説明する．各メッセージは，次のフィールドを持つ．

src メッセージの送信元ノード dest メッセージの宛先ノード ldr リーダを伝えるフィールド hops ノード間を転送された回数

rcvTimer countdown timerであるタイマーのフィールドまた，各ノードnは次の値を変数に保持している．

ldr 自分がリーダーだと思っているノード dist ldrまでの距離

timer ノードがタイムアウトするまでの値を示すcountdown timer

メッセージmsgを受信したノードはhopフィールドを見て，その時点での自分のldr への最短経路であるとき，または，現在のldr よりmsgのldr が小さいとき，そのメッセージを隣接ノードに転送する．それ以外のメッセージは無視する．ノードはメッセージを送信

後，timerの値を適切な時間にセットする．適切な時間とは，次にリーダーからのメッセー

ジを受け取るべき時間である．タイムアウトしたノードは，ToDelay秒の遅延の後，隣接

(28)

6.2 Leader Election Protocol 22 ノードにフィールドldr が自分のノードIDであるメッセージmsgを送信し，自分のtimer

をP eriodにセットする．このとき，msgがMsgDelay秒内にノードに受信されるように，

msg中のrcvT imerへ値をセットする．以上の説明から計算すると，ノードnがメッセー

ジを受信したときに，timerをPeriod+ToDelay+distanceToLeader(n)×MsgDelay秒以上にセットすれば，アルゴリズムは安定状態になる．

6.2.1 LMNtal での記述

LMNtalで記述したleader election protocolを図6.4に示す. これは，文献[5]に掲載されていた，TLA+によるプログラムコードを LMNtalにエンコードしたものである．

初期プロセスについて，nbrs(i)は隣接ノードを表現しており，3つのノードが環状に繋がったネットワークとなっている．その他の初期プロセスは，節 6.2の各変数名をそのままアトム名として使用している．maxTimeについては後述する．ルールTimeOut@@

はノードがタイムアウトした際の処理を，RcvMsg_i@@はノードがメッセージを受信した際の処理を表している．Leader election protocol の場合，タイミングの制約の上限値と下限値が等しいことから，上界値用タイマーと下界値用タイマーを一つにまとめて使っている．Leader election protocolの場合もFischerのアルゴリズムと同様，ルール

Tickを複数の LMNtal ルールの中間命令列を連結することにより実装した．図 6.5 は

leader election protocolのTickのアルゴリズムである．図 6.4のプログラムに対して，

now(now)がPeriod+ToDelay+distanceToLeader(n)×MsgDelayより大きいとき，全てのノードnに対して，ldr(n)=1 が常に成り立つことを検証する．

6.2.2 モデル検査対応

このモデルではFischerのアルゴリズムと違い時刻を表す変数nowが検証したい性質に関係している．このような場合，同値関係∼を以下のように定義し，性質を対称性に基づく状態空間削減を行って検証する．任意の状態sとtについて，s.now とt.now が等しいかあるいはどちらも Σ より大きいならば，s ∼ tとする．ここでΣはすべてのノードnに対するPeriod+ToDelay+distanceToLeader(n)×MsgDelayの最大値である．

LMNtalでは，時間が Σ + 1 までしか進まなくするために，LMNtalのルールTick@@に now≤Σ + 1という制約を追加している．

(29)

6.3 その他の例題のエンコード 23

6.3 その他の例題のエンコード

Explicit-time methodを用いて，ここで説明した以外にも代表的なリアルタイムシステ

ムの例題についてLMNtalへエンコードを行った．エンコードを行ったのは，train-gate, PAR Protocol, FDDI Protocolである．Train-gateは公開版UPPAAL のサンプルプログラムから，FDDI protocol は同じくUPPAAL のベンチマーク^*1から,PAR Protocol はSpinのリアルタイム拡張であるDTSpin[3] のサンプルプログラムからそれぞれエンコードを行った．いずれもExplicit-time methodを使用してLMNtalにエンコードしたのち，その性質についてLTLモデル検査が適用できることを確認した．その結果，いずれの例題も，エンコードの際に多少の工夫やごまかしがあったとしても，Fischerのアルゴリズムで説明したように，countdown timerを使って時間制約を表現し，絶対時間を表す変数nowを消去してモデル検査を適用することができた．これらの例題は巻末の付録に収録しておく．

*1 http://www.it.uu.se/research/group/darts/uppaal/benchmarks/#benchmarks

(30)

6.3 その他の例題のエンコード 24

leader.lmn

図6.4 leader.lmn

if (∀n∈Node (timer[n] +ToDelay≥d)

∧ ∀ms∈Message (ms.rcvTimer ≥d)) then atomic { now =now +d;

foreach(n) timer[n] =timer[n]−d;

foreach(ms)

ms.rcvTimer =ms.rcvTimer −d;

}

図6.5 Leader election protocolのTickアルゴリズム

(31)

25

第 7 _章

実験による性能評価

LMNtalでexplicit-time methodを使って記述したリアルタイムシステムの例題のうちFishcerのアルゴリズムとleader election protocolについて，SLIMと他のモデル検査ツールで時間性能の測定を行い比較した．比較に使用したモデル検査ツールは，UPPAAL とTLC[17]である．TLC は文献[5]でexplicit-time method の解説に使用されている

TLA+[6]に対応したモデル検査器である．今回の実験は，文献[5]で行われた性能比較実

験結果と並列LMNtalモデル検査器での実験結果とを比較対照できるように行った．

7.0.1 実験環境

実験に使用した環境は，各例題で共通で，表7.1に示してある．実験はコア数48の共有メモリ並列計算機上で行った．SLIMについては，各例題で1コア, 2コア, 12コア, 48 コアを使用した場合について実験を行った．

表7.1 実験環境

OS CentOS 5.4

CPU AMD Opteron(tm) Processor 6176 SE， 48CPUs

メモリ容量 256GB

SLIM version 2.2.0 (leader electionは2.1.6)

TLC version 2.03

UPPAAL version 4.0.13

(32)

26

表7.2 Fischerのアルゴリズムのsafetyの状態数と実行時間[s]

SLIM TLC UPPAAL

δ 状態数 1コア 2コア 24コア 48コア状態数実行時間実行時間

3 155976 10.72 5.74 0.62 0.46 155976 11 0.10

4 450407 31.38 16.97 1.72 1.16 450407 28 0.10

5 1101072 78.85 42.64 4.34 2.87 1101072 66 0.10

6 2388291 177.34 93.10 9.27 6.09 2388291 141 0.10

7 4731824 350.60 186.72 18.62 11.74 4731824 278 0.10 8 8730831 661.29 348.24 35.70 23.04 8730831 518 0.10 9 15208872 1152.07 623.04 61.42 39.14 15208872 954 0.10 10 25263947 1963.40 1061.05 110.33 71.59 25263947 1674 0.10 11 40323576 3123.62 1683.09 168.45 108.67 40323576 2836 0.10

"!"

#$%$ &&('

)%'+*

図7.1 Fischerのアルゴリズムのsafetyの実行時間

7.0.2 Fischer のアルゴリズムの実験

この実験で使用したFischerのアルゴリズムは6.1節で解説したものである．UPPAAL の測定に使用したモデルはUPPAALの配布版のデモに含まれているものである．TLC

(33)

27

表7.3 Fischerのアルゴリズムのlivenessの状態数と実行時間[s]

SLIM TLC UPPAAL

δ 状態数 1コア 2コア 26コア 48コア状態数実行時間実行時間

3 221066 17.49 10.46 2.57 3.07 155976 52 9.33

4 644437 53.69 33.00 8.09 9.84 450407 150 9.33

5 1585794 137.80 84.54 21.79 41.74 1101072 379 9.33 6 3456482 312.07 190.00 49.18 63.90 2388291 890 9.33 7 6874066 639.91 396.80 109.59 139.38 4731824 1966 9.33 8 12721851 1211.93 760.30 211.64 269.81 8730831 6031 9.33

9 22215962 2161.37 1371.13 367.85 516.92 — — 9.33

10 36979984 3659.02 2319.09 651.41 865.87 — — 9.33

11 59127162 5992.05 3685.87 1094.61 1459.43 — — 9.33

の測定に使用したモデルは文献[5]に掲載しているコードを書き起こしたものである．以上のモデルに対してsafetyとlivenessの検証を行った．safetyはcsにおけるスレッドの排他制御が正しく行われていることについて，livenessはbに着いたスレッドがいつか必ずcに至ることについて検証した．[5]と同様の実験を行うため，パラメータは同じものを使用し，モデル中のスレッド数を6本に設定し，δ =²としてδを3から 11の間で動かして検証を行った．safetyの実験結果を表7.2と図7.1に，livenessの実験結果を表7.3 と図7.2に示す．

表7.2より，SLIMとTLCの状態数が一致していることから，LMNtalへのエンコードが正しく行われているといえる．また，図7.1より，TLCとSLIMの実行時間がδ の増加に従い，同様に推移していることから，SLIMへのexplicit-time methodによるリアルタイムシステムのモデル検査が妥当に行われたといえる．リアルタイムモデル検査器であるUPPAALは，δに依存せずごく短い時間で検査できる一方，explicit-time method による検査はδが大きくなると，状態数が増加するので，時間も増加する．TLCとSLIM の逐次性能を比較するとSLIMはTLCの幾何平均0.85倍の時間性能となっている．図 7.1から，SLIM は使用するコア数に大まかに比例した時間性能がでているように見える．SLIMの並列効果は，48コア使用した場合は、1コア使用した場合の幾何平均28倍の時間性能となっている．さらに，スレッドを6本に固定したままδを増加させていき，

SLIMで48コアを使用して時間の測定を続けた結果，最大δ= 18まで測定することができ，このとき状態数は505083291，実行時間は1482.25秒であった．

表7.3と図7.2よりliveness の時間性能を比較する．TLCはδ =9以上では，out of

(34)

28

! #"%$

&

'"%$

##( '"%$

)+**-,.,0/

12/ &

図7.2 Fischerのアルゴリズムのlivenessの実行時間

memoryにより測定不可能であった．SLIMとTLCの状態数が異なるのは，状態数の数

え方の問題であり，SLIMが数え上げている受理状態の数を減算するとTLCの状態数と等しくなる．1コアのSLIMであってもTLCより全体的にかかった時間は短く，幾何平均3.16倍の時間性能で測定できた．SLIMの並列効果をみてみると，safetyに比べ台数効果が低く，48コアで最も高い時間性能となっていない．この例題のLiveness検証について，最も高い時間性能を出す使用コア数をパラメータδ = 3で調べた結果、26コア使用時であった．これは閉路探索を行っているアルゴリズムOWCTY[2]の問題である．

次に，δの値を3で固定し，スレッドの本数を5から10の間で変化させ測定した．(実験結果を書く予定)

7.0.3 Leader election protocol の実験

この実験で使用した leader election protocol は6.2 節で解説したものである．TLC の測定に使用したモデルは，文献 [5]から書き起こしたものである．UPPAAL の測定に使用したモデルは，[9]に掲載しているものを使用した．このモデルは文献[9] におい

ては，UPPAAL-TIGA[16] というUPPAALの拡張ツール用のモデルであるが，通常の

UPPAALでも適用できることを確認した．モデル中のノードはリング状に連結した3つ