操作参数

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:

  1. import java.util.concurrent.*
  2. class MultiMap<K, V> {
  3. private val map = ConcurrentHashMap<K, List<V>>()
  4. // Maintains a list of values
  5. // associated with the specified key.
  6. fun add(key: K, value: V) {
  7. val list = map[key]
  8. if (list == null) {
  9. map[key] = listOf(value)
  10. } else {
  11. map[key] = list + value
  12. }
  13. }
  14. fun get(key: K): List<V> = map[key] ?: emptyList()
  15. }

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:

  1. Declare the @Param annotation.
  2. Specify the integer generator class: @Param(gen = IntGen::class). Lincheck supports random parameter generators for almost all primitives and strings out of the box.
  3. Define the range of values generated with the string configuration @Param(conf = "1:2").
  4. Specify the parameter configuration name (@Param(name = "key")) to share it for several operations.

    Below is the stress test for MultiMap that generates keys for add(key, value) and get(key) operations in the range of [1..2]:

    1. import java.util.concurrent.*
    2. import org.jetbrains.kotlinx.lincheck.annotations.*
    3. import org.jetbrains.kotlinx.lincheck.check
    4. import org.jetbrains.kotlinx.lincheck.paramgen.*
    5. import org.jetbrains.kotlinx.lincheck.strategy.stress.*
    6. import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
    7. import org.junit.*
    8. class MultiMap<K, V> {
    9. private val map = ConcurrentHashMap<K, List<V>>()
    10. // Maintains a list of values
    11. // associated with the specified key.
    12. fun add(key: K, value: V) {
    13. val list = map[key]
    14. if (list == null) {
    15. map[key] = listOf(value)
    16. } else {
    17. map[key] = list + value
    18. }
    19. }
    20. fun get(key: K): List<V> = map[key] ?: emptyList()
    21. }
    22. @Param(name = "key", gen = IntGen::class, conf = "1:2")
    23. class MultiMapTest {
    24. private val map = MultiMap<Int, Int>()
    25. @Operation
    26. fun add(@Param(name = "key") key: Int, value: Int) = map.add(key, value)
    27. @Operation
    28. fun get(@Param(name = "key") key: Int) = map.get(key)
    29. @Test
    30. fun stressTest() = StressOptions().check(this::class)
    31. @Test
    32. fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
    33. }
  5. Run the stressTest() and see the following output:

    1. = Invalid execution results =
    2. | ---------------------------------- |
    3. | Thread 1 | Thread 2 |
    4. | ---------------------------------- |
    5. | add(2, 0): void | add(2, -1): void |
    6. | ---------------------------------- |
    7. | get(2): [0] | |
    8. | ---------------------------------- |
  6. Finally, run modelCheckingTest(). It fails with the following output:

    1. = Invalid execution results =
    2. | ---------------------------------- |
    3. | Thread 1 | Thread 2 |
    4. | ---------------------------------- |
    5. | add(2, 0): void | add(2, -1): void |
    6. | ---------------------------------- |
    7. | get(2): [-1] | |
    8. | ---------------------------------- |
    9. ---
    10. All operations above the horizontal line | ----- | happen before those below the line
    11. ---
    12. The following interleaving leads to the error:
    13. | ---------------------------------------------------------------------- |
    14. | Thread 1 | Thread 2 |
    15. | ---------------------------------------------------------------------- |
    16. | | add(2, -1) |
    17. | | add(2,-1) at MultiMapTest.add(MultiMap.kt:31) |
    18. | | get(2): null at MultiMap.add(MultiMap.kt:15) |
    19. | | switch |
    20. | add(2, 0): void | |
    21. | | put(2,[-1]): [0] at MultiMap.add(MultiMap.kt:17) |
    22. | | result: void |
    23. | ---------------------------------------------------------------------- |

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.

Get the full code.

操作参数 - 图1

Next step

Learn how to test data structures that set access constraints on the execution, such as single-producer single-consumer queues.