テスト戦略
Lincheckは、並行データ構造をテストするための2つの戦略、モデルチェックとストレス検証を提供します。
この記事では、これらの戦略の違いと、テスト戦略を選択する際に考慮すべき点について説明します。
モデルチェック (Model checking)
モデルチェックでは、Lincheckは起こりうるスレッドのインターリーブ（実行順序の組み合わせ）をシミュレートし、不正な動作の原因となるものを報告します。
データ構造のテストにモデルチェック戦略を使用するには、ModelCheckingOptions() を使用してテスト関数を宣言します。
@Test
fun modelCheckingTest() = ModelCheckingOptions()
.check(this::class)モデルチェック戦略を使用すると、Lincheckは共有メモリアクセス（read および write）や、ロックの取得と解放、park/unpark、wait/notify などの同期ポイントに、明示的なスレッド切り替え命令を挿入します。
スレッドの切り替えを制御することで、Lincheckは以下のことが可能になります。
- プログラムの異なる実行スケジュールの可能性を決定論的に探索する。
- 詳細な実行トレースを提供する。
現在、モデルチェックを使用する場合、Lincheckは実行において逐次一貫性メモリモデル (sequentially consistent memory model)を想定しています。これは、緩和された Java メモリモデル下での命令の並べ替え（リオーダリング）やメモリキャッシュの動作、およびその他の同様のエフェクトに関連するバグはシミュレートされず、検出できないことを意味します。
ストレス検証 (Stress testing)
ストレス検証では、Lincheckはエラーが見つかる可能性を高めるために、各シナリオを複数回実行します。
ストレス検証を使用するには、StressOptions() を使用してテスト関数を宣言します。
@Test
fun stressTest() = StressOptions()
.check(this::class)モデルチェックとは異なり、Lincheckはスレッドの切り替えを制御したり追跡したりしません。これにより、ストレス検証はより高速になり、メモリモデルについての仮定を必要としません。 ただし、ストレス検証ではテストの再現性がなく、Lincheckは実行トレースを提供できません。
戦略の選択
戦略を選択する際は、以下の点を考慮してください。
| モデルチェック | ストレス検証 | |
| 速度 | 遅い。 | 速い。 |
| 再現性 | 入力データが変わらなければ、テストは正確に同じ結果を返します。 | 実行ごとにスレッドのスケジュールが変わる可能性があるため、テスト結果が異なる場合があります。 |
| 前提条件 |
|
|
| 詳細度 | 並行シナリオと、不正な動作に至った実行トレースの両方を報告します。 | 並行シナリオのみを報告します。 |
| 標準ライブラリのサポート |
| あらゆる機能の使用に起因するバグを検出できる可能性があります。 |
次のステップ
シナリオ生成のカスタマイズ、実行停止（ストール）検出の有効化、ライブラリのトレッドセーフ保証の提供など、テスト戦略を構成する方法について学びましょう。