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

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

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

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

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

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

   repositories {
       mavenCentral()
   }
   
   dependencies {
       // Lincheck dependency
       testImplementation("org.jetbrains.kotlinx:lincheck:2.22")
       // 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.22"
       // This dependency allows you to work with kotlin.test and JUnit:
       testImplementation "junit:junit:4.13"
   }
   

Написание конкурентного счётчика и запуск теста

1. В директории src/test/kotlin, создайте файл BasicCounterTest.kt и добавьте следующий код с ошибочным конкурентным счётчиком и тестом Lincheck для него:

   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() и get() операциями.

   • Выполняет большое количество вызовов для каждого сгенерированного сценария.

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

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

   = Invalid execution results =
   | ------------------- |
   | Thread 1 | Thread 2 |
   | ------------------- |
   | 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.junit.*
   
   class Counter {
       @Volatile
       private var value = 0
   
       fun inc(): Int = ++value
       fun get() = value
   }
   
   class BasicCounterTest {
       private val c = Counter()
   
       @Operation
       fun inc() = c.inc()
   
       @Operation
       fun get() = c.get()
   
       @Test
       fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
   }
   

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

   = Invalid execution results =
   | ------------------- |
   | Thread 1 | Thread 2 |
   | ------------------- |
   | inc(): 1 | inc(): 1 |
   | ------------------- |
   
   The following interleaving leads to the error:
   | --------------------------------------------------------------------- |
   | Thread 1 |                          Thread  2                         |
   | --------------------------------------------------------------------- |
   |          | inc()                                                      |
   |          |   inc(): 1 at BasicCounterTest.inc(BasicCounterTest.kt:18) |
   |          |     value.READ: 0 at Counter.inc(BasicCounterTest.kt:10)   |
   |          |     switch                                                 |
   | inc(): 1 |                                                            |
   |          |     value.WRITE(1) at Counter.inc(BasicCounterTest.kt:10)  |
   |          |     value.READ: 1 at Counter.inc(BasicCounterTest.kt:10)   |
   |          |   result: 1                                                |
   | --------------------------------------------------------------------- |
   

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

   • 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 =
| ---------------------------------------- |
|      Thread 1     |       Thread 2       |
| ---------------------------------------- |
| addLast(22): void |                      |
| ---------------------------------------- |
| pollFirst(): 22   | addFirst(8): void    |
|                   | peekLast(): 22 [-,1] |
| ---------------------------------------- |

---
All operations above the horizontal line | ----- | happen before those below the line
---
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:
| --------------------------------------------------------------------------------------------------------------------------------- |
|                                                Thread 1                                                    |       Thread 2       |
| --------------------------------------------------------------------------------------------------------------------------------- |
| pollFirst()                                                                                                |                      |
|   pollFirst(): 22 at ConcurrentDequeTest.pollFirst(ConcurrentDequeTest.kt:17)                              |                      |
|     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: 22 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917)                       |                      |
|     prev.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:919)                     |                      |
|     switch                                                                                                 |                      |
|                                                                                                            | addFirst(8): void    |
|                                                                                                            | peekLast(): 22       |
|     compareAndSet(Node@2,22,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) |                      |
|     unlink(Node@2) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921)                      |                      |
|   result: 22                                                                                               |                      |
| --------------------------------------------------------------------------------------------------------------------------------- |

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

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

См. также

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

• Распространённые ограничения алгоритмов

• Проверка гарантий бе блокирующего прогресса

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