テスト戦略の設定
Lincheck は、シナリオ生成、実行のスタール（停滞）検出、検証など、テスト戦略のためのさまざまな設定オプションをサポートしています。
オプションを有効にする方法
テスト戦略のオプションを有効にするには、戦略クラスで設定を行います。
@Test
fun modelCheckingTest() = ModelCheckingOptions()
.iterations(100) // 生成されるシナリオの数を指定
.check(this::class)シナリオの最小化
デフォルトでは、Lincheck はテストの動作を変更しない操作を削除することで、失敗したシナリオの最小化を試みます。
失敗したシナリオの全容を確認するには、minimizeFailedScenario オプションを false に設定します。
シナリオの生成
| オプション | デフォルト値 | 説明 |
|---|---|---|
iterations | 100 | 生成される並行シナリオの数。 |
invocationsPerIteration | 10_000 | 各並行シナリオごとの呼び出し回数。 |
threads | 2 | 各シナリオにおけるスレッドの数。 |
actorsBefore | 5 | シナリオの並列セクションの前に呼び出される操作の数。 |
actorsPerThread | 5 | シナリオの並列セクションにおける、各スレッド内の操作の数。 |
actorsAfter | 5 | シナリオの並列セクションの後に呼び出される操作の数。 |
customScenarios | – | カスタム並行シナリオのリスト。カスタムシナリオは、ランダムに生成されたシナリオの前に実行されます。 |
カスタムシナリオの定義
Lincheck は、カスタムシナリオを定義するために ドメイン特有言語 (DSL) を使用します：
@Test
fun test() = StressOptions()
.customScenarios {
initial {
actor(SomeClass1::foo)
}
parallel {
thread {
actor(SomeClass1::buzz, 1)
actor(SomeClass1::buzz, 2)
}
thread {
actor(SomeClass1::buzz, 3)
}
}
post {
actor(SomeClass1::foo)
}
}
.check(this::class)各シナリオは、3 つのオプションセクションで構成されます：
initial– 並列部分の前に実行される操作。parallel– スレッドの定義。スレッドはthreadブロックを使用して定義されます。 並列セクションには複数のthreadブロックを含めることができます。post– 並列部分の後に実行される操作。
操作は actor(function, arg1, arg2, ...) 関数を使用して定義されます。単一のブロック内の操作は順次実行されます。
実行のスタール検出
| オプション | デフォルト値 | 説明 |
timeoutMs | 3000 | Lincheck が実行のスタール（停滞）を報告するまでの呼び出しタイムアウト（ミリ秒単位）。 |
loopBound | 50 | Lincheck が実行のスタールを報告するまでのループ反復回数。 長いループに対して Lincheck が誤って実行のスタールを報告する場合は、 loopBound の値を増やしてください。このオプションは モデルチェック にのみ適用可能です。 |
recursionBound | 20 | Lincheck が実行のスタールを報告するまでの再帰呼び出し回数。loopIterationsBeforeThreadSwitch の値は loopBound 未満である必要があります。このオプションは モデルチェック にのみ適用可能です。 |
ループ内でのスレッド切り替え
| オプション | デフォルト値 | 説明 |
loopIterationsBeforeThreadSwitch | 10 | 別のスレッドへの切り替えを試みる前に、スレッドが実行できるループ反復回数。loopIterationsBeforeThreadSwitch の値は、loopBound 未満である必要があります。このオプションは モデルチェック にのみ適用可能です。 |
検証
| オプション | デフォルト値 | 説明 |
verifierClass | LinearizabilityVerifier | 検証プロセス中に使用される検証クラス：
|
sequentialSpecification | テスト対象のデータ構造と同じ。 | テスト対象のデータ構造の逐次（シーケンシャル）バージョン。この構造は 検証プロセス で使用されます。 |
進捗保証
| オプション | デフォルト値 | 説明 |
checkObstructionFreedom | false | データ構造操作の 障害自由 (obstruction-freedom) 保証 を検証するには、このオプションを true に設定します。このオプションは モデルチェック にのみ適用可能です。 |
ライブラリ解析
| オプション | デフォルト値 | 説明 |
stdLibAnalysisEnabled | false | デフォルトでは、Lincheck は標準ライブラリの操作をスレッドセーフとして扱い、その動作を検証しません。標準ライブラリの関数やクラスの解析を有効にするには、このオプションを true に設定します。このオプションは モデルチェック にのみ適用可能です。 |
addGuarantee | – | addGuarantee オプションを使用して、スレッドセーフなメソッドや解析に無関係なメソッドの 保証を定義 し、それらをモデルチェックから除外します。このオプションは モデルチェック にのみ適用可能です。 |
保証の定義
保証を定義するには、ビルダーチェーンを使用します。クラスを選択し、次にメソッドを選択し、最後に保証タイプを選択します。
@Test
fun modelCheckingTest() = ModelCheckingOptions()
.addGuarantee(
forClasses("java.util.concurrent.ConcurrentHashMap")
.allMethods()
.treatAsAtomic()
)
.check(this::class)forClassesのオーバーロードのいずれかを使用してクラスを選択します：forClasses(vararg fullClassNames: String)—fullClassNames文字列に完全修飾名が含まれているクラスに一致します。forClasses(vararg classes: KClass<*>)— 参照によってクラスを一致させます。forClasses(classPredicate: (fullClassName: String) -> Boolean)— 完全修飾名に対する述語（プレディケート）を使用してクラスを一致させます。
保証を適用するメソッドを選択します：
methods(methodNames: String)–methodNames文字列にメソッド名が含まれている場合に一致します。methods(methodPredicate: (methodName: String) -> Boolean)– 述語を使用してメソッドを一致させます。allMethods()– 選択されたクラスのすべてのメソッドを一致させます。
保証タイプを選択します：
treatAsAtomic()— 各メソッドをアトミックな操作として扱います。Lincheck はメソッド呼び出しの内部にスイッチポイントを挿入しませんが、呼び出しの前後にスイッチポイントを追加する場合があります。スレッドセーフであることが既知のメソッドには
treatAsAtomic()を使用してください。ignore()— メソッドを解析から除外します。Lincheck は、メソッド呼び出しの内部、前、後のいずれにもスイッチポイントを挿入しません。メソッドが内部で同期プリミティブ（例：
synchronizedブロック）を使用している場合、メソッドを無視すると Lincheck がデッドロックを引き起こす可能性があります。ロギングやデバッグユーティリティなど、解析に無関係なメソッドには
ignore()を使用してください。
次のステップ
Lincheck の実行シナリオで使用される操作の 引数生成の設定 方法について学びます。