Аргументы операций

В этом руководстве вы узнаете, как настроить аргументы операций.

Рассмотрим простое MultiMap реализацию ниже. Она основана на ConcurrentHashMap, внутренне хранящем список значений:

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()
}

Является ли эта MultiMap реализация линеаризуемой? Если нет, некорректное перекрестное выполнение, скорее всего, будет обнаружено при доступе к небольшому диапазону ключей, что увеличит вероятность одновременной обработки одного и того же ключа.

Для этого настройте генератор для параметра key: Int:

1. Объявите аннотацию @Param.

2. Укажите класс генератора целых чисел: @Param(gen = IntGen::class). Lincheck поддерживает генераторы случайных параметров для почти всех примитивов и строк «из коробки».

3. Определите диапазон генерируемых значений с конфигурацией строки @Param(conf = "1:2").

4. Укажите имя конфигурации параметра (@Param(name = "key")) для совместного использования для нескольких операций.

   Ниже представлен стресс-тест для MultiMap, генерирующий ключи для операций add(key, value) и get(key) в диапазоне [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.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)
   }
   

5. Запустите stressTest() и увидите следующий вывод:

   = Invalid execution results =
   Parallel part:
   | add(1, 1): void | add(1, 4): void |
   Post part:
   [get(1): [4]]
   

6. Наконец, запустите modelCheckingTest(). Он завершается сбоем со следующим выводом:

   = Invalid execution results =
   Parallel part:
   | add(1, 6): void | add(1, -8): void |
   Post part:
   [get(1): [-8]]
   = The following interleaving leads to the error =
   Parallel part trace:
   |                      | add(1, -8)                                               |
   |                      |   add(1,-8) at MultiMapTest.add(MultiMapTest.kt:61)      |
   |                      |     get(1): null at MultiMap.add(MultiMapTest.kt:38)     |
   |                      |     switch                                               |
   | add(1, 6): void      |                                                          |
   |   thread is finished |                                                          |
   |                      |     put(1,[-8]): [6] at MultiMap.add(MultiMapTest.kt:40) |
   |                      |   result: void                                           |
   |                      |   thread is finished                                     |
   

Из-за небольшого диапазона ключей Lincheck быстро выявляет гонку: когда два значения добавляются одновременно по одному и тому же ключу, одно из значений может быть перезаписано и потеряно.