实参生成约束

为了测试并发数据结构，Lincheck 通过将操作随机放置在不同的线程中并使用随机实参调用它们，来生成一组并发场景。

你可以约束操作实参的范围，以增加发现并发错误的可能性。例如，如果可能键值的范围有限，则哈希映射中的并发操作更有可能访问相同的键。这使 Lincheck 能够更高效地暴露竞态条件和其他并发错误。

要在 Lincheck 中限制生成的实参值范围：

1. 使用 @Param 注解声明一个实参生成器：

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

   • 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,..."	从指定的枚举值列表中生成随机值。 示例：
BooleanGen	""	生成 true 和 false 值。不需要特定的配置字符串。 示例： "" -> [true, false]
DoubleGen	"start:step:end" "start:end" ""	生成从 start 到 end 的 Double 值，按 step 递增。 默认 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 中将某些操作限制在单个线程。

另请参阅

• 检查非阻塞进度保证
• 定义算法的顺序规范