Начало работы с Lincheck

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

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

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

Чтобы использовать Lincheck в проекте, добавьте соответствующие зависимости в конфигурацию сборки:

// build.gradle.kts
repositories {
    mavenCentral()
}

dependencies {
    testImplementation("org.jetbrains.lincheck:lincheck:3.7")
    testImplementation(kotlin("test"))
}

// build.gradle
repositories {
    mavenCentral()
}

dependencies {
    testImplementation "org.jetbrains.lincheck:lincheck:3.7"
    testImplementation "org.jetbrains.kotlin:kotlin-test"
}

<!-- pom.xml -->
<project>
    <dependencies>
         <dependency>
             <groupId>org.jetbrains.lincheck</groupId>
             <artifactId>lincheck</artifactId>
             <version>3.7</version>
             <scope>test</scope>
         </dependency>
         <dependency>
             <groupId>org.jetbrains.kotlin</groupId>
             <artifactId>kotlin-test</artifactId>
             <scope>test</scope>
         </dependency>
    </dependencies>
    ...
</project>

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

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

1. В каталоге src/test создайте файл CounterTest.kt.

2. Импортируйте библиотеки org.jetbrains.lincheck, kotlinx.concurrent и kotlin.test:

   import org.jetbrains.lincheck.Lincheck
   import kotlin.test.*
   import kotlin.concurrent.thread

3. Напишите тест, который создаёт переменную и два потока, изменяющих её:

   class CounterTest {
       @Test // Test function declaration
       fun test() = Lincheck.runConcurrentTest {
           var counter = 0
   
           // Increments the counter concurrently
           val t1 = thread { counter++ }
           val t2 = thread { counter++ }
   
           // Waits for the threads to finish
           t1.join()
           t2.join()
   
           // Checks that both increments have been applied
           assertEquals(2, counter)
       }
   }
   

4. Запустите тест. Lincheck создаёт отчёт с чередованием потоков, которое привело к некорректному поведению:

   | ------------------------------------------------------------------------------- |
   |                   Main Thread                   |   Thread 1    |   Thread 2    |
   | ------------------------------------------------------------------------------- |
   | thread(block = Lambda#2): Thread#1              |               |               |
   | thread(block = Lambda#3): Thread#2              |               |               |
   | switch (reason: waiting for Thread 1 to finish) |               |               |
   |                                                 |               | run()         |
   |                                                 |               |   counter ➜ 0 |
   |                                                 |               |   switch      |
   |                                                 | run()         |               |
   |                                                 |   counter ➜ 0 |               |
   |                                                 |   counter = 1 |               |
   |                                                 |               |   counter = 1 |
   | Thread#1.join()                                 |               |               |
   | Thread#2.join()                                 |               |               |
   | counter.element ➜ 1                             |               |               |
   | assertEquals(2, 1): threw AssertionFailedError  |               |               |
   | ------------------------------------------------------------------------------- |
   

   Lincheck обнаружил чередование потоков, при котором одна из операций inc() перезаписывает значение counter.

   Пояснение отчёта по шагам

   1. В потоке 2 JVM считывает исходное значение counter.

   2. Выполнение переключается с потока 2 на поток 1.

   3. В потоке 1 JVM увеличивает счётчик. Все шаги операции inc() выполняются без прерываний: считывание значения из переменной, увеличение значения и запись значения обратно в переменную.

   4. Выполнение переключается обратно на поток 2.

   5. В потоке 2 JVM увеличивает значение, полученное на шаге 1, и записывает результат в переменную counter.

Напишите тест для структуры данных

Помимо простых тестов для параллельного выполнения, Lincheck поддерживает декларативный подход к тестированию параллельных структур данных.

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

В этом разделе вы протестируете простой счётчик:

1. В каталоге src/test создайте файл CounterStructureTest.kt.

2. Импортируйте библиотеки lincheck.datastructures и kotlin.test:

   import org.jetbrains.lincheck.datastructures.*
   import kotlin.test.*

3. Создайте структуру Counter:

   class Counter {
       var value = 0
   
       fun inc(): Int = ++value
       fun dec(): Int = --value
   }
   

4. Создайте класс CounterStructureTest. Задайте начальное состояние структуры и отметьте параллельные операции структуры аннотацией @Operation:

   class CounterStructureTest {
       private val c = Counter()
   
       @Operation
       fun inc() = c.inc()
   
       @Operation
       fun dec() = c.dec()
           .iterations(100) // Specify the number of generated scenarios

5. В классе CounterStructureTest объявите тестовую функцию с помощью ModelCheckingOptions():

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

6. Запустите тест. Lincheck создаёт отчёт об ошибке, содержащий параллельный сценарий и конкретное чередование потоков, которое привело к некорректному поведению:

   | ------------------- |
   | Thread 1 | Thread 2 |
   | ------------------- |
   | inc(): 1 | inc(): 1 |
   | ------------------- |
   

   | ------------------------ |
   | Thread 1 |   Thread 2    |
   | ------------------------ |
   |          | inc(): 1      |
   |          |   c.inc(): 1  |
   |          |     value ➜ 0 |
   |          |     switch    |
   | inc(): 1 |               |
   |          |     value = 1 |
   |          |     value ➜ 1 |
   |          |   result: 1   |
   | ------------------------ |
   

Что дальше

Узнайте о декларативном подходе к тестированию параллельных структур данных в Lincheck.