YokohamaUnitの紹介 (3) リテラル

YokohamaUnit のGroovy式の中では当然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 で入力値と出力値だけが異なるようなテストケースをたくさん作りたい場合、 テストデータを表に抽出することができる。

# 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では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

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

単体テストを専ら関数やメソッドに対するテストであると定義した場合、 言語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の処理系のC言語インターフェイスをCのヘッダから自動生成するツールを作った。

Mling: ML FFI Interface Generator

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

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

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

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

NuSMVを試す

モデル検査ツールの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の違い

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

チルダの後に続く（スラッシュまでの）文字がユーザー名である場合、 そのユーザーのログインディレクトリに置換される。 たとえば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=... command と env 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 ~:~'
~:~

初めて再帰モジュールが必要になった話

入力ストリームの実装から独立したパーサーを定義したい。 そこでまずは入力ストリームのデータ型を定義する。

module type INSTREAM = sig
  type instream
  (* 本当はinstreamに対する色々な操作を含むつもり *)
end

実際の入力元はチャネルだったりメモリ上の文字列だったりする。

module ChanIns = struct
  type instream = in_channel
end

module StringIns = struct
  type instream = string
end

パーサーのシグニチャと実装はこんな感じになる。

module type PARSE = sig
  type instream
  type result
  val parse : instream -> result
end

module Parse(I: INSTREAM): PARSE with type instream = I.instream
  = struct
  type instream = I.instream
  type result = unit
  let parse ins = ()
end

module StringParse = Parse(StringIns)
module ChanParse = Parse(ChanIns)

ここでparse関数の中で、 「ストリームから読み込んだデータをいったん文字列にしてparse関数自身でパースする」 という処理がしたい。 文字列が変数sだとして、その内部のparse関数の呼び出しはどのように書けばよいか。

単にlet rec parse ins = ...としてparse (s : string)では駄目そうだ。 parseの型はinstream -> resultなのだがinstreamはI.instreamであって、 stringであるとは限らない。

じゃあ StringParse.parse (s : string) では？というとこれもだめだ。 Parseの実装の中ではまだStringParseは定義されていない。 もちろんStringParseはParseに依存するのでParseより前に移動するわけにもいかない。

ということは…あ、再帰か。 ということで初めて実際に再帰モジュールというものが必要になる場面に出くわしたのだった。

結論から書くと、次のように書くことでコンパイルが通るようになる。

module Parse(I: INSTREAM)(S: PARSE with type instream = StringIns.instream)
  : PARSE with type instream = I.instream
  = struct
  type instream = I.instream
  type result = unit
  let parse ins = (ignore (S.parse ""); ())
end

module rec StringParse : PARSE with type instream = StringIns.instream =
        Parse(StringIns)(StringParse)
module ChanParse = Parse(ChanIns)(StringParse)

ファンクターは新しい引数Sをとる。 Sのモジュール型から、S.instreamはStringIns.instreamであるという想定がおけるので、 問題のparseの呼び出しはこのSに定義されたparseを呼ぶことでよくなる。

S.parseは結果的にはStringParse.parseを呼んでいることにしたい、 つまりS = StringParseであるということにしたいので、 ファンクターを適用するときに第2引数をStringParseにする必要がある。

これはChanParseのときは簡単な話で、普通に適用すればよい。 しかしStringParseを作るときは自分自身を使って自分自身を作るということになる。 これは再帰だ。ということでrecが付く。 再帰モジュール定義の場合はStringParseのモジュール型を明示する必要があるようだ。

後書き

実際にはSMLを書いていてこの問題に遭遇したのでこのように解決することはできませんでしたが、 そういえばOCamlには再帰モジュールって有ったと思い出して問題を翻訳しました。

シェルのコマンド置換の内部でのコメント

シェルのパーサーを書こうとしていていたのだけどマニュアルから読み取れないところはどうしても動かして実地調査するしかない。 シェルのコマンド置換の内部にコメントを書いて、そのコメントの中にコマンド置換の終端記号が来た場合、終端記号が勝つのかコメントが勝つのかという問題を調べた。

つまりこういうのを試す。

echo $(echo hello # comment)

echo $(echo hello
# comment)

echo `echo hello # comment`

echo `echo hello
comment`

結果

$ echo $(echo hello # comment)
> )
hello
$ echo $(echo hello
> # comment)
> )
hello
$ echo `echo hello # comment`
hello
$ echo `echo hello
> # comment`
hello

つまりダラーの場合はコメントのほうが勝って、バッククォートの場合はバッククォートのほうが勝つ。 bashでもksh93でもzshでも同様の動き。

めんどくさい… 忘れないようにメモしておく。

ブログをもう1つ始めた

ブログをもう1つ始めました。

wonderful cool something -- http://wcs.hatenablog.com/

使い分けはあまり考えていませんが、向こうではとりあえずProcessingで遊んだことなどを書き記していこうと思います。