操作参数
In this tutorial, you’ll learn how to configure operation arguments.
Consider this straightforward MultiMap
implementation below. It’s based on the ConcurrentHashMap
, internally storing a list of values:
import java.util.concurrent.*
class MultiMap<K, V> {
private val map = ConcurrentHashMap<K, List<V>>()
// Maintains a list of values
// associated with the specified key.
fun add(key: K, value: V) {
val list = map[key]
if (list == null) {
map[key] = listOf(value)
} else {
map[key] = list + value
}
}
fun get(key: K): List<V> = map[key] ?: emptyList()
}
Is this MultiMap
implementation linearizable? If not, an incorrect interleaving is more likely to be detected when accessing a small range of keys, thus, increasing the possibility of processing the same key concurrently.
For this, configure the generator for a key: Int
parameter:
- Declare the
@Param
annotation. - Specify the integer generator class:
@Param(gen = IntGen::class)
. Lincheck supports random parameter generators for almost all primitives and strings out of the box. - Define the range of values generated with the string configuration
@Param(conf = "1:2")
. Specify the parameter configuration name (
@Param(name = "key")
) to share it for several operations.Below is the stress test for
MultiMap
that generates keys foradd(key, value)
andget(key)
operations in the range of[1..2]
:import java.util.concurrent.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.paramgen.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.junit.*
class MultiMap<K, V> {
private val map = ConcurrentHashMap<K, List<V>>()
// Maintains a list of values
// associated with the specified key.
fun add(key: K, value: V) {
val list = map[key]
if (list == null) {
map[key] = listOf(value)
} else {
map[key] = list + value
}
}
fun get(key: K): List<V> = map[key] ?: emptyList()
}
@Param(name = "key", gen = IntGen::class, conf = "1:2")
class MultiMapTest {
private val map = MultiMap<Int, Int>()
@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)
@Test
fun stressTest() = StressOptions().check(this::class)
@Test
fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
}
Run the
stressTest()
and see the following output:= Invalid execution results =
| ---------------------------------- |
| Thread 1 | Thread 2 |
| ---------------------------------- |
| add(2, 0): void | add(2, -1): void |
| ---------------------------------- |
| get(2): [0] | |
| ---------------------------------- |
Finally, run
modelCheckingTest()
. It fails with the following output:= Invalid execution results =
| ---------------------------------- |
| Thread 1 | Thread 2 |
| ---------------------------------- |
| add(2, 0): void | add(2, -1): void |
| ---------------------------------- |
| get(2): [-1] | |
| ---------------------------------- |
---
All operations above the horizontal line | ----- | happen before those below the line
---
The following interleaving leads to the error:
| ---------------------------------------------------------------------- |
| Thread 1 | Thread 2 |
| ---------------------------------------------------------------------- |
| | add(2, -1) |
| | add(2,-1) at MultiMapTest.add(MultiMap.kt:31) |
| | get(2): null at MultiMap.add(MultiMap.kt:15) |
| | switch |
| add(2, 0): void | |
| | put(2,[-1]): [0] at MultiMap.add(MultiMap.kt:17) |
| | result: void |
| ---------------------------------------------------------------------- |
Due to the small range of keys, Lincheck quickly reveals the race: when two values are being added concurrently by the same key, one of the values may be overwritten and lost.
Next step
Learn how to test data structures that set access constraints on the execution, such as single-producer single-consumer queues.