Напишите свой первый тест с Lincheck

Создание проекта

1. Откройте существующий проект Kotlin в IntelliJ IDEA или создайте новый. При создании проекта используйте систему сборки Gradle.

2. В каталоге src/main/kotlin откройте файл main.kt.

3. Замените код в main.kt следующей реализацией счётчика:

   class Counter {
       @Volatile
       private var value = 0
   
       fun inc(): Int = ++value
       fun get() = value
   }
   

   Ваш тест Lincheck проверит, является ли счётчик потокобезопасным.

Добавление необходимых зависимостей

1. Откройте файл build.gradle(.kts) и убедитесь, что mavenCentral() добавлен в список репозиториев.

2. Добавьте следующие зависимости в конфигурацию Gradle:

   repositories {
       mavenCentral()
   }
   
   dependencies {
       // Lincheck dependency
       testImplementation("org.jetbrains.kotlinx:lincheck:2.16")
       // This dependency allows you to work with kotlin.test and JUnit:
       testImplementation("junit:junit:4.13")
   }
   

   repositories {
       mavenCentral()
   }
   
   dependencies {
       // Lincheck dependency
       testImplementation "org.jetbrains.kotlinx:lincheck:2.16"
       // This dependency allows you to work with kotlin.test and JUnit:
       testImplementation "junit:junit:4.13"
   }
   

Написание и запуск теста

1. В каталоге src/test/kotlin создайте файл BasicCounterTest.kt и добавьте следующий код:

   import org.jetbrains.kotlinx.lincheck.annotations.*
   import org.jetbrains.kotlinx.lincheck.*
   import org.jetbrains.kotlinx.lincheck.strategy.stress.*
   import org.junit.*
   
   class Counter {
        @Volatile
        private var value = 0
   
        fun inc(): Int = ++value
        fun get() = value
   }
   
   class BasicCounterTest {
       private val c = Counter() // Initial state
   
       // Operations on the Counter
       @Operation
       fun inc() = c.inc()
   
       @Operation
       fun get() = c.get()
   
       @Test // JUnit
       fun stressTest() = StressOptions().check(this::class) // The magic button
   }
   

   Этот тест Lincheck автоматически:

   • Генерирует несколько случайных конкурентных сценариев с указанными операциями inc() и dec().

   • Выполняет множество вызовов для каждого из сгенерированных сценариев.

   • Проверяет, что каждый результат вызова корректен.

2. Запустите тест выше, и вы увидите следующую ошибку:

   = Invalid execution results =
   Parallel part:
   | inc(): 1 | inc(): 1 |
   

   Здесь Lincheck обнаружил выполнение, нарушающее атомарность счётчика — два одновременных инкремента завершились одним и тем же результатом 1. Это означает, что один инкремент был утерян, и поведение счётчика некорректно.

Отслеживание некорректного выполнения

Помимо отображения результатов некорректного выполнения, Lincheck также может предоставить интерлевинг, который приводит к ошибке. Эта функция доступна с помощью стратегии тестирования моделирования, которая исследует множество выполнений с ограниченным числом переключений контекста.

1. Чтобы переключиться на стратегию тестирования, замените тип options с StressOptions() на ModelCheckingOptions(). Обновлённый класс BasicCounterTest будет выглядеть следующим образом:

   import org.jetbrains.kotlinx.lincheck.annotations.*
   import org.jetbrains.kotlinx.lincheck.check
   import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
   import org.jetbrains.kotlinx.lincheck.verifier.*
   import org.junit.*
   
   class Counter {
       @Volatile
       private var value = 0
   
       fun inc(): Int = ++value
       fun get() = value
   }
   
   class BasicCounterTest {
       private val c = Counter()
   
       @Operation
       fun getAndInc() = c.getAndInc()
   
       @Operation
       fun get() = c.get()
   
       @Test
       fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
   }
   

2. Запустите тест снова. Вы получите трассировку выполнения, которая приводит к некорректным результатам:

   = Invalid execution results =
   Parallel part:
   | inc(): 1 | inc(): 1 |
   = The following interleaving leads to the error =
   Parallel part trace:
   |                      | inc()                                                      |
   |                      |   inc(): 1 at BasicCounterTest.inc(BasicCounterTest.kt:11) |
   |                      |     value.READ: 0 at Counter.inc(Counter.kt:5)             |
   |                      |     switch                                                 |
   | inc(): 1             |                                                            |
   |   thread is finished |                                                            |
   |                      |     value.WRITE(1) at Counter.inc(Counter.kt:5)            |
   |                      |     value.READ: 1 at Counter.inc(Counter.kt:5)             |
   |                      |   result: 1                                                |
   |                      |   thread is finished                                       |
   

   Согласно трассировке, произошли следующие события:

   • T2: Второй поток начинает операцию inc(), считывая текущее значение счётчика (value.READ: 0) и приостанавливается.

   • T1: Первый поток выполняет inc(), что возвращает 1, и завершается.

   • T2: Второй поток возобновляется и увеличивает ранее полученное значение счётчика, неправильно обновляя счётчик до 1.

Тестирование стандартной библиотеки Java

Теперь давайте найдём ошибку в стандартном классе Java ConcurrentLinkedDeque. Следующий тест Lincheck обнаруживает гонку между удалением и добавлением элемента в начало очереди:

import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.junit.*
import java.util.concurrent.*

class ConcurrentDequeTest {
    private val deque = ConcurrentLinkedDeque<Int>()

    @Operation
    fun addFirst(e: Int) = deque.addFirst(e)

    @Operation
    fun addLast(e: Int) = deque.addLast(e)

    @Operation
    fun pollFirst() = deque.pollFirst()

    @Operation
    fun pollLast() = deque.pollLast()

    @Operation
    fun peekFirst() = deque.peekFirst()

    @Operation
    fun peekLast() = deque.peekLast()

    @Test
    fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
}

Запустите modelCheckingTest(). Тест завершится ошибкой с выводом:

= Invalid execution results =
Init part:
[addLast(4): void]
Parallel part:
| pollFirst(): 4 | addFirst(-4): void       |
|                | peekLast():   4    [-,1] |
---
values in "[..]" brackets indicate the number of completed operations 
in each of the parallel threads seen at the beginning of the current operation
---

= The following interleaving leads to the error =
Parallel part trace:
| pollFirst()                                                                                               |                      |
|   pollFirst(): 4 at ConcurrentDequeTest.pollFirst(ConcurrentDequeTest.kt:39)                              |                      |
|     first(): Node@1 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:915)                    |                      |
|     item.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917)                    |                      |
|     next.READ: Node@2 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:925)                  |                      |
|     item.READ: 4 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917)                       |                      |
|     prev.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:919)                    |                      |
|     switch                                                                                                |                      |
|                                                                                                           | addFirst(-4): void   |
|                                                                                                           | peekLast(): 4        |
|                                                                                                           |   thread is finished |
|     compareAndSet(Node@2,4,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) |                      |
|     unlink(Node@2) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921)                     |                      |
|   result: 4                                                                                               |                      |
|   thread is finished                                                                                      |                      |

Следующий шаг

Выберите стратегию тестирования и настройте выполнение теста.

См. также

• Как сгенерировать аргументы операций

• Популярные ограничения алгоритмов

• Модульное тестирование в моделировании

• Проверка гарантий безналичного прогресса

• Определение последовательной спецификации алгоритма