引数生成の制約

並行データ構造をテストするために、Lincheckはオペレーションを異なるスレッドにランダムに配置し、それらをランダムな引数で呼び出すことによって、一連の並行シナリオを生成します。

並行性に関するバグが見つかる確率を高めるために、オペレーション引数の範囲を制約することができます。 例えば、ハッシュマップにおける並行オペレーションでは、可能なキー値の範囲を制限することで、同じキーにアクセスする可能性が高くなります。これにより、Lincheckは競合状態やその他の並行性バグをより効率的に顕在化させることができます。

Lincheckで生成される引数値の範囲を制限するには：

1. @Param アノテーションを使用して引数ジェネレータを宣言します：

   @Param(name = "key", gen = IntGen::class, conf = "1:2")
   class MultiMapTest {
       // テスト
   }

   • name – 引数ジェネレータの名前。
   • gen – ジェネレータの型。
   • conf – ジェネレータの設定文字列。ここでは、Lincheckは1から2までの整数値を生成します。

   Lincheckは、複数の値型に対応したジェネレータを提供しています。型ごとに異なる設定文字列のテンプレートを使用します。

   詳細は ジェネレータの型 セクションを参照してください。

2. オペレーションのパラメータに @Param を付与して制約を適用します：

   @Operation
   fun add(@Param(name = "key") key: Int, value: Int) = map.add(key, value)
   
   @Operation
   fun get(@Param(name = "key") key: Int) = map.get(key)

制約を適用すると、Lincheckは指定された範囲内の値のみを使用してシナリオを生成します：

| ---------------------------------- |
|    Thread 1     |     Thread 2     |
| ---------------------------------- |
| add(2, 0): void | add(2, -1): void |
| ---------------------------------- |
| get(2): [-1]    |                  |
| ---------------------------------- |

ジェネレータの型

Lincheckは、以下の引数ジェネレータ型を提供しています：

ジェネレータ	設定テンプレート	説明
IntGen	"min:max"	min から max までの Int 値（両端を含む）を生成します。 設定文字列が空の場合、Int.MIN_VALUE から Int.MAX_VALUE までの全整数範囲を使用します。 例： "1:3" -> [1, 2, 3]
StringGen	"maxWordLength:alphabet" "maxWordLength" ""	提供された alphabet から、maxWordLength までの長さのランダムな文字列値を生成します。 デフォルトの alphabet は [a-zA-Z\d _] です。 デフォルトの maxWordLength は 15 です。 例：
EnumGen	"Enum.Const1,Enum.Const2,..."	指定された列挙型（enum）値のリストからランダムな値を生成します。 例：
BooleanGen	""	true および false の値を生成します。特定の設定文字列は必要ありません。 例： "" -> [true, false]
DoubleGen	"start:step:end" "start:end" ""	start から end まで、step ずつ増加させた Double 値を生成します。 デフォルトの step 値は (end - start)/100 です。 設定文字列が空の場合、Int.MIN_VALUE から Int.MAX_VALUE までの値を step = 0.1 で生成します。 例： "0.0:0.1:1.0" -> [0.0, 0.1, 0.2, ..., 0.9, 1.0]
FloatGen	"start:step:end" "start:end" ""	DoubleGen と同様ですが、値は Float に変換されます。 例： "0.0:0.1:1.0" -> [0.0, 0.1, 0.2, ..., 0.9, 1.0]
LongGen	"min:max"	IntGen と同様ですが、値は Long に変換されます。 例： "1:3" -> [1, 2, 3]
ShortGen	"min:max"	min から max までの Short 値（両端を含む）を生成します。 設定文字列が空の場合、-32768 から 32767 までの全短整数範囲を使用します。 例： "1:3" -> [1, 2, 3]
ByteGen	"min:max"	min から max までの Byte 値（両端を含む）を生成します。 設定文字列が空の場合、-128 から 127 までの全バイト範囲を使用します。 例： "1:3" -> [1, 2, 3]
ThreadIdGen	""	現在のスレッドのID番号を返します。特定の設定文字列は必要ありません。 例： "" -> [1, 2]

次のステップ

Lincheckで特定のオペレーションを単一スレッドに制限する方法を学びます。

関連項目

• ノンブロッキングな進捗保証のチェック
• アルゴリズムの逐次仕様の定義