So-net無料ブログ作成
検索選択

ScalaCheckへの疑念 [Scala]

「プロパティベースのテスト」について初めて知ったのは Fun of Programmingという本で、 それを読んだ当時ScalaにもScalaCheckがあることを知って少しさわっていたんだけど 結果的には「なんか微妙」という感想を持ってやめてしまった。[^1]

その後特にScalaCheckをさわってはおらず、Scalaからもかなり離れてしまったので感想も変わっていないんだけど Scalaのユーザーが増えるとともにScalaCheckも使われているようで、よく聞くようになった。

それで思い出したのでScalaCheckへの疑念を言語化することにした。 タイトルはScalaCheckとしたけれどもQuickCheckやその他の同様のフレームワークにも該当すると思う。

普通にテストケースを書いたほうがいいのではないか

ScalaCheckでは例えば「任意の1024以上の整数nについてP(n)が成立する」のような性質から、 nを例えば100通り自動生成してテストケースを実行してくれる。 人間がテストケースを書く場合、おそらく2,3個のケースを書くにとどまるだろう。

ここで「50倍ものケースを自動実行するのだからより大きい確証が得られるだろう」 ということが言えるだろうか。

人間が書くテストケースにおけるnはおそらく1024と、MAX_INTと、ひょっとしたらその間の適当な値である。[^2]

自動生成されるケースは1024以上MAX_INT以下のランダムな100個で、 1024とMAX_INTはそこに含まれるかもしれないし含まれないかもしれない。

この例で1024とMAX_INTはバグを見つけてくれそうなテストケースである。それは仕様の境界値だから。[^3] プログラムは「以上」と「より大きい」を勘違いしているかもしれないし、オーバーフローを考慮していないかもしれない。

これに対して1025からMAX_INT-1までの値はせいぜい1つ選べばよく、残りは無駄なテストである。 無駄なテストケースは100個あっても10000個あっても品質の向上に貢献しない。 ランダムに100回実行したから1回実行したよりも99回分多くの確信が得られると思うのは偽の確信である。 偽の確信はテストにおける害悪だ。

これらに対して「それはジェネレーターの定義次第だ」という反論があるかもしれない。 でもそれを意識してジェネレータを作るならば、 それは人間がテストケースを決めるのを遠回りにしただけではないだろうか。

ランダムな組み合わせはどうか

複数の変数に対する組み合わせテストを自動生成してくれる点が ScalaCheckなどの方法の有利な点だという考えがあるかもしれない。 これは確かに手で書くのは煩雑だ。

でも同じ自動生成するのでも直交表やPairwise法などの、経験的な研究に裏付けられた、 バグ検出に効率的な組み合わせの自動生成方法があり、 ランダムな生成が有利だという根拠はない。

確率的なものは難しい

以前ScalaCheckをさわっていた時の記事で、 確率的な分布を意識していないと有効なテストが生成されないことがあるという注意点を取り上げていた。

テストの中に確率的なものが現れるのは悪いことだと思う。 おそらく多くの開発者にとって確率はプログラムよりずっと理解しにくいからだ。 プログラムコードの結果を予測するよりもテストコードの結果を予測するほうが難しいというのは、 明らかに望ましい状況ではない。

再帰的なデータ構造についてはどうか

再帰的なデータ構造に対するテストデータの生成はScalaCheckのような方法が活躍できる領域かもしれない。 再帰的なデータ構造では変数の数自体が固定的でなく、 そのような問題に対して既存の組み合わせ技法をどう適用すればいいかはあまりはっきりしないからだ。

これについてもしかし、ランダムである必要があるのかという点についてはやはり疑問が残る。 (有界モデル検査のようにある決まった範囲を全網羅するような方法が代わりに考えられる)


以上ScalaCheckや類似の手法についての疑念を書いた。

大体においては 「同値分割や境界値分析やPairwiseなどの既存のテスト技法でテスト設計したほうがいいのでは」 と感じているということだ。

一方で「ScalaCheckは駄目だと思っている」かというとあまりそこは断言できない。

1つにはこれだけ皆使っているので自分の理解が何か間違っているのではないかという不安がある。 (上記に書いたようなことを補填するような洗練されたやり方が考案されているのかもしれない)

もう1つはテスト手法の良しあしは経験的に決まるものだという点で、 例えば「実際にプロパティベースのテストのほうが既存のテスト手法より良くバグを見つけるのだ」 という経験的研究結果があればなるほどそういうものかと思って納得するかもしれない。 (読んでいる人でご存知の人がいたら教えてください)

  • [^1] 左下の「ScalaCheckを試す」のリンク集を参照
  • [^2] n=1023でP(n)が成立しないこともテストするかもしれないが、比較のためここでは取り上げない
  • [^3] MAX_INTは「暗黙の」境界値であるともいえる

YokohamaUnitの紹介 (5) スタブ [YokohamaUnit]

YokohamaUnit はスタブ作成のための文法を提供する。

一般的には次の形式をとり、式が現れる場所に置かれる。

a stub of `クラス名` such that method `メソッドシグニチャ` returns ...

例えばMapクラスのスタブであり、 getメソッドに対して42を返却するスタブは次のように書く。

a stub of `java.util.Map` such that method `get(java.lang.Object)` returns 42

テスト全体としてはたとえばこのように書ける。

# Test: Collections.unmodifiableMap preserves lookup
 
Assert `unmodifiableMap.get("answer")` is 42
 where map is a stub of `java.util.Map`
              such that method `get(java.lang.Object)` returns 42
   and unmodifiableMap is `java.util.Collections.unmodifiableMap(map)`.

こうした記述はMockitoのメソッドを呼ぶようなバイトコードにコンパイルされる。

スタブ/モック機能を言語機能としてどのように取り入れるかのバランスは難しいところであり、 どのように発展させるか(させないか)は模索している段階にある。

ある程度高機能なスタブを作るための表記は結局のところある種のプログラミング言語になる。 JavaGroovyで書くのでなく、 スタブ/モック用の言語を使う利点があるスイートスポットは(もしあるとしたら)どの位の用途なのか。 自然言語として読み下せることはスタブ/モックにとってどの程度重要なのだろうか。

またYokohamaUnitについて言えば、バイトコードを自分で生成できる前提なので、 あえてMociktoを使用する必然性も実はあまりないかもしれない。


YokohamaUnitの紹介 (4) 4フェーズテスト [YokohamaUnit]

YokohamaUnit で4フェーズテストを書く方法を取り上げる。

4フェーズテストはテスト対象のメソッドや関数を呼んだ後のオブジェクト (やその他の)状態の変化を確かめるテストの一般的なパターンで、 事前準備(setup)、実行(exercise)、検証(verify)、事後処理(teardown)からなる。

YokohamaUnitでは見出しをつかってそれぞれのフェーズを表す。

# Test: AtomicInteger.incrementAndGet increments the content
## Setup
Let i be `new java.util.concurrent.atomic.AtomicInteger(0)`.
 
## Exercise
Do `i.incrementAndGet()`.
 
## Verify
Assert `i.get()` is `1`.

Setupでは主にLet文を使って変数の束縛を行う。 Let文は複数並べてもよいし、andでつなげてもよい。

Let x be 1 and y be 2.

beでなく=でもよい。

Let x = 1 and y = 2.

ExerciseではDo文を使ってテスト対象のメソッドの実行を行う。 Do文は式言語の(副作用を起こすことが期待される)式をとる。

これも複数並べてもよいし、andでつなげてもよい。

## Exercise
Do `i.incrementAndGet()` and `i.incrementAndGet()`.
Do `i.incrementAndGet()`.

Verifyフェーズは4フェーズでない関数的なテストの場合と同様だが、 複数並べた場合やfor allを使った場合の実行単位が異なる。

Assertを複数並べたり、テーブルを参照した場合、 関数的なテストでは複数のJUnitテストメソッドにコンパイルされたが、 4フェーズテストの中でそのように書いた場合は、 1つのメソッドの中で続けて実行されるようなコードにコンパイルされる。

4フェーズテストをパラメタ化する方法については別の記事で紹介する。

次の例はTeardownフェーズを含むテストの例である。 Teardownフェーズの中でもExerciseフェーズと同様、Do文を使う。

# Test: The size of a new temporary file is zero
## Setup
Let temp be `java.io.File.createTempFile("prefix", null)`.
 
## Verify
Assert `temp.length()` is `0L`.
 
## Teardown
Do `temp.delete()`.

Teardownフェーズはテストの成否にかかわらず必ず実行される。


YokohamaUnitの紹介 (3) リテラル [YokohamaUnit]

YokohamaUnitGroovy式の中では当然Groovyのリテラルが使える。 リストのリテラルなどはJavaにはないリテラルだ。

Assert that `Arrays.asList("a", "b", "c")` is `["a", "b", "c"]`.

文字列などの基本的なリテラルもGroovyのものを利用できる。

Assert that `sut.toString()` is `"hello"`.

しかしこのようにバッククォートとダブルクォートを重ねて書くのはうるさいと感じるかもしれない。 そこでYokohamaUnitは基本型については独自にリテラルを用意している。

Assert that `sut.toString()` is "hello".

YokohamaUnitの基本型リテラルはほとんど厳密にJavaの基本型リテラルを踏襲している。 GroovyはおおむねJavaを踏襲しているが、違いに注意しなければならない点もある。 例えばシングルクォートはGroovyでは文字ではなく文字列として解釈される。

Assert that `'c'` is "c".
Assert that `'c' as char` is 'c'.

他にも浮動小数点リテラルの16進数表記などで違いがあるが、 普通に使う範囲で注意するのは文字リテラルくらいだろう。

Javaになく、YokohamaUnitにあるリテラルとして複数行文字列リテラルがある。 複数行文字列リテラルは見出しの後にバッククォート3つ(から5つ)で囲んで定義する。 使用する際はその見出しを使って参照する。

# Test: Test Multi-line literal
 
Assert `"cheer\n".multiply(3).denormalize()` is [Three cheers].
 
### Three cheers
 
```
cheer
cheer
cheer
```

バッククォートの後にスペース区切りで任意の識別子を書くことができるが、 この識別子を使って改行コードや文字列末尾に改行が付くかどうかを制御することができる。

lfという識別子を置くと改行コードがLFになる。

# Test: Code block with lf
 
Assert `s.length()` is 2 where s is [lf].
 
### lf
 
```text lf
a
```

この例でtextという識別子に特に意味はなく、無視される。

crlfという識別子を置くと改行コードがCRLFになる。

# Test: Code block with crlf
 
Assert `s.length()` is 3 where s is [crlf].
 
### crlf
 
```text crlf
a
```

chopという識別子を置くと末尾の改行コードが付かなくなる。

# Test: Code block with chop
 
Assert `s.length()` is 1 where s is [chop].
 
### chop
 
```text crlf chop
a
```

文字列リテラルや複数行文字列リテラルの後に "as クラス名" を書くことで 任意のオブジェクトに変換できる。 これは複雑なテストデータの準備に活用できる。

YokohamaUnit自身のテストコードから例を示す。

文字列Sourceが次のように定義されているとする。

### Source
```
# Test: test
Assert `x < 4` is true where x = any of 1, 2 or 3.
 
# Test: test 2
## Setup
Let y = any of 4, 5 or 6.
 
## Verify
Assert `y < 4` is true.
```

テストデータとしてはこれを文字列ではなくASTデータ型であるGroupオブジェクトに変換したい。 そこでSourceを参照する箇所では次のように書く。

[Source] as `yokohama.unit.ast.Group`

このようにするとYokohamaUnitはクラスパス中からyokohama.unit.annotations.As というアノテーションがついたクラスを検索し、 そのクラスの中から「文字列を引数として取り、Groupを戻すメソッド」を探す。

@As
public class DataConverters {
    public static Group asAst(String input) {
      ...
    }
}

そしてそのメソッドを使ってデータ変換を行うようなバイトコードを生成する。 変換を行うメソッドが定義されたクラスはテストコンパイル時とテスト実行時の両方でクラスパス中になければならない。


YokohamaUnitの紹介 (2) パラメタ化テスト [YokohamaUnit]

YokohamaUnit で入力値と出力値だけが異なるようなテストケースをたくさん作りたい場合、 テストデータを表に抽出することができる。

# Test: String.endsWith
 
Assert `sut.endsWith(suffix)` is `expected`
for all sut, suffix and expected in Table [Test data for endsWith].
 
| sut           | suffix  | expected |
| ------------- | ------- | -------- |
| "hello world" | ""      | true     |
| "hello world" | "world" | true     |
| "hello world" | "hello" | false    |
[Test data for endsWith]

表のキャプションは表の前でもよい。

[Test data for endsWith]
| sut           | suffix  | expected |
| ------------- | ------- | -------- |
| "hello world" | ""      | true     |
| "hello world" | "world" | true     |
| "hello world" | "hello" | false    |

JUnitのTheoryとの大きな違いだが、表の1行が1つのテストメソッドとなる。 つまり、上記のような記述の場合、テストメソッドは3つできる。 したがって、表の一部のテストが失敗しても他のテストは実行されるし、 テストケース数も3件と数えられる。

テストデータをCSVファイルExcelに書くこともできる。

# Test: String.startsWith
Assert `sut.startsWith(prefix)` is `expected`
for all sut, prefix and expected in Excel 'TestExcel.xlsx'.
# Test: String.startsWith
Assert `sut.startsWith(prefix)` is `expected`
for all sut, prefix and expected in CSV 'TestCSV.csv'.

この場合、CSVファイルやExcelファイル読み込みはテスト実行時ではなくて テストコードのコンパイル時に行われ、やはり1行が1つのテストメソッドとなる。


YokohamaUnitの紹介 (1) 関数的なメソッドのテスト [YokohamaUnit]

YokohamaUnitでは1つのソースファイルが1つのJUnitテストクラスにコンパイルされる。) ソースファイルの標準的な拡張子はdocyである。

テストケースを書くには # Test: という文字列に続けて、 そのテストの名前を示す見出しを書く。

# Test: This is my first test

この見出しはJUnitテストクラスにおけるメソッド名の元になるが、 特にJavaのメソッド名の規約の制約を受けない。

最初のハッシュ記号は上の例では1つだが、1つから6つまでの任意の数でよい。

YokohamaUnitのテストケースの書き方は「関数的なメソッドのテスト」と 「4フェーズテスト」の2つに分けられる。今回は前者を取り上げる。

関数的なメソッドとはその結果が引数の値のみによって決定されるメソッドである。[^1] そのようなメソッドはもっともテストがしやすい。

関数的なメソッドをテストするためのAssert文は見出しに続けて直接書くことができる。

# Test: This is my first test
 
Assert that `Integer.valueOf("123")` is 123.

thatは省略してもよい。 ここでは Integer.valueOf がテスト対象のメソッドである。 バッククォートに囲まれた部分 Integer.valueOf("123")Groovyの式として解釈される。

Assert文は1つの見出しの下に複数続けて記述しても構わない。

# Test: This is my first test
 
Assert `Integer.valueOf("123")` is 123.
 
Assert `Integer.valueOf("456")` is not 123.

この場合それぞれのAssert文に対して別々のJUnitテストメソッドが生成される。 したがって一方が失敗してももう一方のテストは実行されるし、2ケースとカウントされる。

次のように書いた場合は1つのメソッドのみが生成される。

Assert `Integer.valueOf("123")` is 123 and `Integer.valueOf("456")` is not 123.

例外の送出をテストしたい場合は次のように書く。

Assert that `Integer.valueOf("xyz")` throws an instance of `NumberFormatException`.

例外を送出しないということをあえてテストとして書きたい場合は次のように書く。

Assert that `Integer.valueOf("123")` throws nothing.

Assert文の副文の主語にあたる部分が長くなると読みにくくなることがある。 そのような場合、where句を使って変数を導入することができる。

Assert that `sut.length()` is 27 where sut is "honorificabilitudinitatibus".

isの代わりに=を使ってもよい。

Assert that `sut.length()` is 27 where sut = "honorificabilitudinitatibus".

複数の変数を導入することもできる。

Assert that `sut.startsWith(prefix)` is true
where sut = "honorificabilitudinitatibus" and prefix = "honor".

[^1] Javaのような言語では「引数と不変なフィールドの値のみによって」 といったほうがいいかもしれない。 そのように定義するならば、メソッドの引数だけでなく、 不変なフィールドを初期化するコンストラクタ引数にも依存してよい。


単体テストのための外部DSL [YokohamaUnit]

プログラムの単体テスト(自動実行されるテストコード)は普通テスト対象となるプログラムと同じ言語で書かれる。 当たり前のようだが必然的にそうでなければならないということではない。

単体テストを専ら関数やメソッドに対するテストであると定義した場合、 言語Aのプログラムの単体テストを記述する言語に求められる最低限の要件は、 「その言語Aの関数やメソッドの呼び出し規約に従ってリンクできる」ということだけだ。 実際Javaの単体テストをGroovyで書くということはおこなわれているようだし、 理論上はC言語の単体テストをSML#で書いたって構わないはずだ。[^1]

それでもテスト対象と同じ言語で単体テストが書かれるのが一般的なのは、

  1. 自明にリンクできる
  2. 開発者自身が単体テストを書くことが多い

といった理由によるだろう。

また、こうした単体テストはある種の内部DSLとして書かれる。 私の理解では、これは単体テストのコードが 単に「言語Aで書かれた別のプログラム」ように見えるのではなく、 「テストの意図をそれにふさわしい見え方で表現したもの」として見えてほしいからだ。

例えばJavaのJUnitであれば、下記のような書き方をする。

assertThat(sut.get(0), is(123));

この書き方は "Assert that sut.get(0) is 123." という英語の文として読み下すことができるので可読性が高いと言われている。 このような考え方はしばしば「ドキュメントとしてのテスト」といわれる。

ところで上記のJUnitの文は詳しく見てみると「2つのレベル」がある。 「テスト対象の呼び出し」に属する部分と「ドキュメント」に属する部分だ。

さっきJUnitの文を英文にパラフレーズするときに sut.get(0) の部分だけは(いわば直接話法のように)そのまま残していた。 この箇所は英文としてそのまま読み下すことができない。 しかしそれはテスト対象の呼び出しの部分だから、 ドキュメントの文法(疑似英語)でなく対象プログラムの文法に属するとみなすことは自然である。

sut.get(0) 以外の部分は「ドキュメント」に属するレベルである。 (123がどちらに属するかについては微妙な点だ)

このドキュメントの部分は「自然」だろうか。 たとえば何故assertとThatの間に空白がなく、ThatのTだけが大文字なのだろうか。 isの前にカンマが来て後に括弧が来るのはなぜだろうか。 つまり結局のところなぜ "Assert that sut.get(0) is 123." と書けないのだろうか。

もちろんその答えはドキュメントのレベルをJavaの内部DSLで記述しているからだ。 しかし、もともとなぜJavaの単体テストをJavaで書いているのかを振り返ってみよう。 それはテスト対象とのリンク要件を容易に満たせるからだった。 しかし先に分割した2つのレベルのうち、 リンク要件を満たす必要があるのは「テスト対象の呼び出し」のレベルだけで、 「ドキュメント」のレベルは別にそうではない。

以上のような考察から、「単体テストのための外部DSL」があってもいいのではないか、 という考えが浮かび上がってくる。 その外部DSLは上述の2つのレベルからなる文法を持ち、 テスト対象とリンクするバイナリにコンパイルされるだろう。

YokohamaUnit はそのようなJava向けの単体テストフレームワークである。 「ドキュメント」部分には独自の文法を持ち、 「テスト対象の呼び出し」の部分にはGroovyを使う。 テストコードは直接JUnitのクラスファイルにコンパイルされる。

次のコードはYokohamaUnitのテストコードとして妥当なものの例である。

*[FizzBuzz]: yokohama.unit.example.FizzBuzz
 
# Test: FizzBuzz test 
 
Assert that `new FizzBuzz().generate(16)` is
`[ "1", "2", "Fizz", "4", "Buzz", "Fizz", "7", "8",
   "Fizz", "Buzz", "11", "Fizz", "13", "14", "FizzBuzz", "16" ]`.
*[StringUtils]: yokohama.unit.example.StringUtils
 
# Test: Test cases for `toSnakeCase`
 
Assert that `StringUtils.toSnakeCase(input)` is `expected`
for all input and expected in Table [1].
 
Assert that `StringUtils.toSnakeCase(null)` throws
an instance of `NullPointerException`.
 
| input           | expected          |
| --------------- | ----------------- |
| ""              | ""                |
| "aaa"           | "aaa"             |
| "HelloWorld"    | "hello_world"     |
| "practiceJunit" | "practice_junit"  |
| "practiceJUnit" | "practice_j_unit" |
| "hello_world"   | "hello_world"     |
[1]

外部DSLの選択は文法の不自然さ以外にもいくつかの内部DSLの制約を解消しうる。 例えば(JUnitにおける)例外のテストやパラメタ化テストの問題などである。

次の記事からYokohamaUnitの機能を紹介していきたい。

[^1] 脱線になるが、結合のレベルが上がるほどこの要件は緩和される。 コマンドのテストで求められるのは、コマンドライン呼び出しができることだけだ。 たとえばDejaGnuはTclベースだが、 テスト対象がTclで書かれていなければならないということはない。 またRESTサービスをテストするのに使うクライアント側の言語の選択肢も、 サービス側の実装言語にほとんど左右されないだろう。


Mling: ML処理系のC言語インターフェイスを自動生成する [SML]

SMLの処理系のC言語インターフェイスをCのヘッダから自動生成するツールを作った。

Mling: ML FFI Interface Generator

現在のところMLtonとPoly/MLに対応していて、cursesを使うサンプルが動くようになっている。

先行するものとしてSML/NJとMLtonにはmlnlffigenというツールがあるようなのだけど、使い方がよくわからなかったのだ。 やりたいのはCの関数の型をMLの型に書き換える機械的な作業なので、いいや自分で作ろうということになった。

C言語の構文解析には紆余曲折の後libclangをPythonから使うことにした。 Ubuntupython-clang-3.3を導入した環境で動作を確認している。

一般的な構文解析ツールでC言語の構文解析をしようとするとtypedef問題などに突き当たってしまって、かなり面倒なことになる。 libclangは何と言ってもCコンパイラが使う真正のC言語パーサーだからそれを使えるのは理想的なはずだ。 でもlibclang自体の使い方もドキュメントが乏しくてよくわからないところが多い。 だから面倒くささということに関しては結局どっちもどっちかもしれない。


NuSMVを試す [SMV]

モデル検査ツールのNuSMVを試してみた。

例題として基本的な排他制御を書いてみる。

MODULE lock
  VAR
    locked-by : {nobody, 0, 1};
  ASSIGN
    init(locked-by) := nobody;

MODULE proc(id, lock)
  VAR
    status: {normal, trying, critical};
  ASSIGN
    init(status) := normal;
    next(status) :=
      case
        (status = normal) : {trying, normal};
        (status = trying) & (lock.locked-by = nobody) : critical;
        (status = critical) : {critical, normal};
        TRUE : status;
      esac;
    next(lock.locked-by) :=
      case
        (next(status) = critical) : id;
        (status = critical & next(status) = normal) : nobody;
        TRUE : lock.locked-by;
      esac;

MODULE main
  VAR
    lock: process lock;
    proc0: process proc(0, lock);
    proc1: process proc(1, lock);
  -- safety: at most one process can enter ciritcal section.
  LTLSPEC G !((proc0.status = critical) & (proc1.status = critical))

lockモジュールはlocked-byという変数だけを持つ。 これはロックを所有しているプロセスID(誰もロックをとっていない場合はnobody)を示す。

procモジュールはプロセスの現在の状態をstatusという変数で持つ。 normalは何もしていない状態、tryingはロックを取得しようとしている状態、criticalはロックを取得した状態である。

statusの初期状態はnormalで、状態遷移はnext(status) := ...で定義される。 normalの場合は、そのままnormalにとどまるか、非決定的にtryingに遷移する。 tryingで、かつロックが誰にも取得されていなければcriticalに遷移する。 criticalの場合は、そのままcriticalにとどまるか、非決定的にnormalに遷移する。

procモジュールの中でロックの状態の更新も行っている。 statusがcriticalの場合は自身のプロセスIDで置き換える。 criticalからnormalに遷移した場合は所有者をnobodyに戻す。

mainはlockと2つのprocを結びつける。procの引数にはプロセスIDとロックを与える。

LTLSPECはこのモデルが満たすべき仕様(最大1つのプロセスしかクリティカルセクションに入れない)を時相論理式で定義している。

$ NuSMV mutex.smv
*** This is NuSMV 2.5.4 (compiled on Sun Aug 24 14:27:46 UTC 2014)
(中略)
WARNING *** Processes are still supported, but deprecated.      ***
WARNING *** In the future processes may be no longer supported. ***

WARNING *** The model contains PROCESSes or ISAs. ***
WARNING *** The HRC hierarchy will not be usable. ***
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

最後の行で仕様が満たされたことがわかる。

このようなモデルの書き方がもう廃止候補になっていることが警告されるのだけど、 その背景や代替の書き方などについて知識がないのでとりあえずこのままいくことにする。

次に新たな仕様として、飢餓状態が起こらないことを表現したい。 これはそれぞれのプロセスについて 「どんな場合でも一度tryingになったらいつかはcriticalに入れる」 と宣言することで表現できる。 そこでMODULE procの最後に次の仕様を記述する。

LTLSPEC G ((status = trying) -> F (status = critical))

これで実行してみると仕様が満たされないことが報告され、その反例が示される。

$ NuSMV mutex.smv
*** This is NuSMV 2.5.4 (compiled on Sun Aug 24 14:27:46 UTC 2014)
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 1.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 1.2 <-
  proc0.status = trying
-> Input: 1.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.3 <-
  proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  lock.locked-by = 1
  proc1.status = critical
-> Input: 1.5 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 1.5 <-
-- specification  G (status = trying ->  F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 2.2 <-
  _process_selector_ = proc1
  running = FALSE
  proc1.running = TRUE
  proc0.running = FALSE
  lock.running = FALSE
-> State: 2.2 <-
  proc1.status = trying
-> Input: 2.3 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.3 <-
-> Input: 2.4 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 2.4 <-
  proc0.status = trying
-> Input: 2.5 <-
  _process_selector_ = main
  running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 2.5 <-
-> Input: 2.6 <-
  _process_selector_ = lock
  running = FALSE
  lock.running = TRUE
-> State: 2.6 <-
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

この反例はちょっとつまらない、NuSMVの使い方に関するともいえるものだ。 この反例ではState: 1.2やState: 2.2で各プロセスがtryingになったあと、一度もそのプロセスに実行権が回ってきていないのである。

ここではOSのスケジューラがプロセスに対してある程度公平な扱いをすることを前提にしたい。 このためには、MODULE procに次の行を追加する。

FAIRNESS running

runningはプロセスが実行されていることを示す暗黙の変数で、先ほどの反例のトレース中にも現れていた。 FAIRNESSというのはその式が「いつも『いつかは成立する』」(その式が永遠に成立しないような経路を排除する)ということを条件として与えるものだ。

これで実行してもまだ反例が見つかる。

$ NuSMV mutex.smv
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 1.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 1.2 <-
  proc0.status = trying
-> Input: 1.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.3 <-
  proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  lock.locked-by = 1
  proc1.status = critical
-> Input: 1.5 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 1.8 <-
-- specification  G (status = trying ->  F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 2.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 2.2 <-
  proc0.status = trying
-> Input: 2.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 2.3 <-
  proc1.status = trying
-> Input: 2.4 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.4 <-
-> Input: 2.5 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 2.5 <-
  lock.locked-by = 0
  proc0.status = critical
-> Input: 2.6 <-
-- Loop starts here
-> State: 2.6 <-
-> Input: 2.7 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 2.7 <-
-> Input: 2.8 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.8 <-
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

これは何かというと、自分がtryingのときにもう一方のプロセスがロックを取得し、そのままずっと離さないことを示している。 我々のモデルには「ロックはいつか解放される」とは表現されていなかったのでこのようなことが起こる。

解決方法はおそらく2通りあり、FAIRNESSを使ってロックが永遠に離されない経路を排除するか、 ロックが有限ステップ内で解放されるようにASSIGNの定義を変えることだ。 ここでは後者の方法を選択することにし、プロセスはロックを取得したら次のステップで解放するようにする。

(status = critical) : normal;

また実行するとまた反例が見つかる。

$ NuSMV mutex.smv
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 1.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 1.2 <-
  proc0.status = trying
-> Input: 1.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.3 <-
  proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  lock.locked-by = 1
  proc1.status = critical
-> Input: 1.5 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 1.7 <-
  lock.locked-by = nobody
  proc1.status = normal
-> Input: 1.8 <-
-> State: 1.8 <-
  proc1.status = trying
-> Input: 1.9 <-
-> State: 1.9 <-
  lock.locked-by = 1
  proc1.status = critical
-- specification  G (status = trying ->  F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
  lock.locked-by = nobody
  proc0.status = normal
  proc1.status = normal
-> Input: 2.2 <-
  _process_selector_ = proc0
  running = FALSE
  proc1.running = FALSE
  proc0.running = TRUE
  lock.running = FALSE
-> State: 2.2 <-
  proc0.status = trying
-> Input: 2.3 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-> State: 2.3 <-
  proc1.status = trying
-> Input: 2.4 <-
  _process_selector_ = main
  running = TRUE
  proc1.running = FALSE
-> State: 2.4 <-
-> Input: 2.5 <-
  _process_selector_ = proc0
  running = FALSE
  proc0.running = TRUE
-- Loop starts here
-> State: 2.5 <-
  lock.locked-by = 0
  proc0.status = critical
-> Input: 2.6 <-
-> State: 2.6 <-
  lock.locked-by = nobody
  proc0.status = normal
-> Input: 2.7 <-
-> State: 2.7 <-
  proc0.status = trying
-> Input: 2.8 <-
-- Loop starts here
-> State: 2.8 <-
  lock.locked-by = 0
  proc0.status = critical
-> Input: 2.9 <-
  _process_selector_ = proc1
  proc1.running = TRUE
  proc0.running = FALSE
-- Loop starts here
-> State: 2.9 <-
-> Input: 2.10 <-
-> State: 2.10 <-
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

これは何かというと、自分がtryingの間もう一方のプロセスがロック取得・解放を延々と繰り返していてずっと割り込めないでいるのだ。

だからOSのスケジューラの公平さとは別に、ロックの動作自体に公平さをもたらす必要があることがわかる。 これはちょっと大仕事になる。

とりあえずtryingからcriticalに遷移していいかどうかの判断をprocから切り離してlockプロセスに移動する。 waitingという配列を導入して、procがtryingになるときにTRUEにする。 procはtrying中にlocked-byが自分自身になったときにcriticalに遷移できるが、locked-byを選ぶのはlockプロセスの仕事にする。 つまり、procはロックに応募するだけで、当選者を決めるのはlockの仕事である。

MODULE lock
  VAR
    locked-by : {nobody, 0, 1};
    waiting : array 0..1 of boolean;
  ASSIGN
    init(locked-by) := nobody;
    next(locked-by) :=
      case
        (locked-by = nobody & waiting[0] = TRUE) : 0;
        (locked-by = nobody & waiting[1] = TRUE) : 1;
        TRUE : locked-by;
      esac;
    next(waiting[0]) :=
      case
        (next(locked-by) = 0) : FALSE;
        TRUE : waiting[0];
      esac;
    next(waiting[1]) :=
      case
        (next(locked-by) = 1) : FALSE;
        TRUE : waiting[1];
      esac;
  FAIRNESS running

MODULE proc(id, lock)
  VAR
    status: {normal, trying, critical};
  ASSIGN
    init(status) := normal;
    init(lock.waiting[id]) := FALSE;
    next(status) :=
      case
        (status = normal) : {trying, normal};
        (status = trying) & (lock.locked-by = id) : critical;
        (status = critical) : normal;
        TRUE : status;
      esac;
    next(lock.waiting[id]) :=
      case
        (status = normal & next(status) = trying) : TRUE;
        TRUE : lock.waiting[id];
      esac;
    next(lock.locked-by) :=
      case
        (status = critical & next(status) = normal) : nobody;
        TRUE : lock.locked-by;
      esac;
  FAIRNESS running
  LTLSPEC G ((status = trying) -> F (status = critical))

MODULE main
  VAR
    lock: process lock;
    proc0: process proc(0, lock);
    proc1: process proc(1, lock);
  -- safety: at most one process can enter ciritcal section.
  LTLSPEC G !((proc0.status = critical) & (proc1.status = critical))

lockプロセスはwaitingがTRUEになっているプロセスのなかからlocked-byにするプロセスを選択するとともに、そのプロセスのwaitingをFALSEに戻す。 ここで next(waiting[0]) := ... と添え字ごとに書いている箇所は添え字部分を変数にしてforeachみたいな構文で書きたいのだが、まだ調査不足でやりかたがわからない。

これを実行するとproc0については仕様が成立し、proc1については成立しない結果となるが、 lockプロセスのプロセス選択が不公平だからだ。このモデルでは両方がtryingのとき必ずproc0を優先することになっている。

ここでturnという変数を導入する。turnはプロセス数を範囲とするカウンタであり、ロックが取得されていないときは1ずつ上がっていく。 waitingからロックを与えるプロセスを決めるときはturnと一致するプロセスがtryingであるかどうかを見る。 つまりプロセスを順番に見て行って一番最初にtryingとして見つかったものにロックを与える。

MODULE lock
  VAR
    locked-by : {nobody, 0, 1};
    waiting : array 0..1 of boolean;
    turn : 0..1;
  ASSIGN
    init(locked-by) := nobody;
    next(locked-by) :=
      case
        (locked-by = nobody & waiting[turn] = TRUE) : turn;
        TRUE : locked-by;
      esac;
    next(waiting[0]) :=
      case
        (next(locked-by) = 0) : FALSE;
        TRUE : waiting[0];
      esac;
    next(waiting[1]) :=
      case
        (next(locked-by) = 1) : FALSE;
        TRUE : waiting[1];
      esac;
    next(turn) :=
      case
        (locked-by = nobody) : (turn + 1) mod 2;
        TRUE : turn;
      esac;
  FAIRNESS running

このモデルを検証するとようやくすべての仕様が満たされた。

$ NuSMV mutex2.smv
(中略)
-- specification  G (status = trying ->  F status = critical) IN proc0 is true
-- specification  G (status = trying ->  F status = critical) IN proc1 is true
-- specification  G !(proc0.status = critical & proc1.status = critical)  is true

調査不足かつ情報もあまり多くないので、まだよくわかっていない部分も多い。 こうかけたらいいのに、という部分はところどころあるが、NuSMV自体の制約かもしれないし知らないだけかもしれない。


チルダ置換のbash, ksh93, zshの違い [sh]

シェルではコマンドや引数がチルダで始まるときに置換が行われる。

チルダの後に続く(スラッシュまでの)文字がユーザー名である場合、 そのユーザーのログインディレクトリに置換される。 たとえばrootのログインディレクトリが/rootのとき、次のようになる。

$ echo ~root
/root

この置換はクォートの内部では働かない。

$ echo "~root"
~root

ここまでの動作はbash, ksh93, zshで共通だ。

チルダに続くのが変数置換のとき、 bashではチルダ置換が行われないが、ksh93とzshでは行われる。

$ sudo bash -c 'echo ~$USER'
~root
$ sudo ksh -c 'echo ~$USER'
/root
$ sudo zsh -c 'echo ~$USER'
/root

チルダに続くのがクォートされた文字列のとき、 bashではチルダ置換が行われないが、ksh93とzshでは行われる。

$ bash -c 'echo ~"root"'
~root
$ ksh -c 'echo ~"root"'
/root
$ zsh -c 'echo ~"root"'
/root
$ bash -c 'echo ~"ro""ot"'
~root
$ ksh -c 'echo ~"ro""ot"'
/root
$ zsh -c 'echo ~"ro""ot"'
/root

チルダに続く文字列がエスケープされているとき、 bashではチルダ置換が行われないが、ksh93とzshでは行われる。

$ bash -c 'echo ~\r\o\o\t'
~root
$ ksh -c 'echo ~\r\o\o\t'
/root
$ zsh -c 'echo ~\r\o\o\t'
/root

チルダに続くのがコマンド置換のとき、3つのシェルのいずれでもチルダ置換が行われる。

$ bash -c "echo ~`echo root`"
/root
$ ksh -c "echo ~`echo root`"
/root
$ zsh -c "echo ~`echo root`"
/root
$ bash -c "echo ~$(echo root)"
/root
$ ksh -c "echo ~$(echo root)"
/root
$ zsh -c "echo ~$(echo root)"
/root

チルダ置換はコマンド、引数の先頭以外にも、変数代入の文脈で値をコロン区切りにした先頭部分でも行われる。

$ PATH=~root:~root
$ echo $PATH
/root:/root

しかし、どこが変数代入の文脈とみなされるかはbashとksh93, zshで異なるようだ。 ksh93とzshではコマンド前のA=Bやexportの文脈のみだが、bashではそれ以外でも変数代入の形をしていればチルダ置換をする。

$ bash -c 'echo PATH=~root:~root'
PATH=/root:/root
$ ksh -c 'echo PATH=~root:~root'
PATH=~root:~root
$ zsh -c 'echo PATH=~root:~root'
PATH=~root:~root

bashは上記のような無関係(?)な箇所でチルダ展開が起こることに注意しなければならない。 一方ksh93やzshでも PATH=... commandenv PATH=... command でチルダ展開の有無が異なることに注意しなければならない。 (前者の...の箇所では起こるが、後者の...の箇所では起こらない)

ここまでの例ではksh93とzshの動作は同じだったが、存在しないユーザーが指定された場合の動作はbash, ksh93とzshで異なる。 zshの場合はエラーとなり、ほかの2つではチルダがそのまま残される。

$ bash -c 'echo ~nosuchuser'
~nosuchuser
$ ksh -c 'echo ~nosuchuser'
~nosuchuser
$ zsh -c 'echo ~nosuchuser'
zsh:1: no such user or named directory: nosuchuser

もう一つ変なものを見つけてしまった。 チルダプレフィクス(チルダからスラッシュが来るまで、またはコマンドや引数が終わるまで)がチルダ単体の場合は自身の$HOMEで置換されるが、 bashとksh93ではコロンでもよい。zshはそうではない。

# bash -c 'echo ~:~'
/root:~
# ksh -c 'echo ~:~'
/root:~
# zsh -c 'echo ~:~'
~:~

この広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。

×

この広告は1年以上新しい記事の更新がないブログに表示されております。