Тестирование на стресс и проверка моделей

Тестирование на стресс

import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.junit.*

class CounterTest {
    private val c = Counter() // Initial state
    
    // Operations on the Counter
    @Operation
    fun inc() = c.inc()

    @Operation
    fun get() = c.get()

    @Test // Run the test
    fun stressTest() = StressOptions().check(this::class)
}

Как работает тестирование на стресс

Сначала Lincheck генерирует набор одновременных сценариев, используя операции, помеченные @Operation. Затем он запускает нативные потоки, синхронизируя их в начале, чтобы гарантировать, что операции стартуют одновременно. Наконец, Lincheck выполняет каждый сценарий в этих нативных потоках несколько раз, ожидая столкновения с ситуацией, приводящей к неверным результатам.

На рисунке ниже представлена общая схема того, как Lincheck может выполнять сгенерированные сценарии:

Проверка моделей

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

Тест проверки модели строится так же, как и тест на стресс. Просто замените StressOptions(), которые определяют стратегию тестирования, на ModelCheckingOptions().

import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.junit.*

class CounterTest {
    private val c = Counter() // Initial state

    // Operations on the Counter
    @Operation
    fun inc() = c.inc()

    @Operation
    fun get() = c.get()

    @Test // Run the test
    fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
}

Какая стратегия тестирования лучше?

Стратегия проверки моделей предпочтительнее для поиска багов в рамках модели памяти последовательной согласованности, поскольку она обеспечивает лучшую покрываемость и предоставляет трассировку некорректного выполнения, если ошибка найдена.

Хотя тестирование на стресс не гарантирует покрываемость, проверка алгоритмов на наличие багов, введённых низкоуровневыми эффектами, например, пропущенным модификатором volatile, по-прежнему полезна. Тестирование на стресс также очень помогает в обнаружении редких багов, для воспроизведения которых требуются многочисленные переключения контекста, и их невозможно проанализировать из-за текущих ограничений в стратегии проверки моделей.

Настройка стратегии тестирования

Для настройки стратегии тестирования задайте параметры в классе <TestingMode>Options.

1. Установите параметры для генерации и выполнения сценариев для CounterTest:

   import org.jetbrains.kotlinx.lincheck.annotations.*
   import org.jetbrains.kotlinx.lincheck.check
   import org.jetbrains.kotlinx.lincheck.strategy.stress.*
   import org.junit.*
   
   class CounterTest {
       private val c = Counter()
   
       @Operation
       fun inc() = c.inc()
   
       @Operation
       fun get() = c.get()
   
       @Test
       fun stressTest() = StressOptions() // Stress testing options:
           .actorsBefore(2) // Number of operations before the parallel part
           .threads(2) // Number of threads in the parallel part
           .actorsPerThread(2) // Number of operations in each thread of the parallel part
           .actorsAfter(1) // Number of operations after the parallel part
           .iterations(100) // Generate 100 random concurrent scenarios
           .invocationsPerIteration(1000) // Run each generated scenario 1000 times
           .check(this::class) // Run the test
   }
   

2. Запустите stressTest() снова, Lincheck сгенерирует сценарии, похожие на приведенный ниже:

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

   Здесь две операции до параллельной части, два потока для каждой из двух операций, а затем одна операция в конце.

Вы можете настроить тесты проверки моделей аналогичным образом.

Минимизация сценариев

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

Вот минимизированный сценарий для теста счётчика выше:

= Invalid execution results =
| ------------------- |
| Thread 1 | Thread 2 |
| ------------------- |
| inc()    | inc()    |
| ------------------- |

Поскольку анализ более мелких сценариев проще, минимизация сценариев включена по умолчанию. Чтобы отключить эту функцию, добавьте minimizeFailedScenario(false) в конфигурацию [Stress, ModelChecking]Options.

Ведение логов состояний структуры данных

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

Для этого определите метод, который не принимает аргументы и отмечен аннотацией @StateRepresentation. Метод должен быть потокобезопасным, неблокирующим и никогда не изменять структуру данных.

1. В примере Counter, представление String — это просто значение счётчика. Таким образом, чтобы отобразить состояния счётчика в трассировке, добавьте функцию stateRepresentation() в CounterTest:

   import org.jetbrains.kotlinx.lincheck.annotations.*
   import org.jetbrains.kotlinx.lincheck.check
   import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
   import org.junit.Test
   
   class CounterTest {
       private val c = Counter()
   
       @Operation
       fun inc() = c.inc()
   
       @Operation
       fun get() = c.get()
   
       @StateRepresentation
       fun stateRepresentation() = c.get().toString()
   
       @Test
       fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
   }
   

2. Запустите modelCheckingTest() сейчас и проверьте состояния Counter , напечатанные в точках переключения, которые изменяют состояние счётчика (они начинаются с STATE:) :

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

В случае тестирования на стресс Lincheck отображает представление состояния непосредственно перед и после параллельной части сценария, а также в конце.

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

Узнайте, как настроить аргументы, передаваемые операциям, и когда это может быть полезно.