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

Тестирование на устойчивость

import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.check
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 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 Counter {
    @Volatile
    private var value = 0

    fun inc(): Int = ++value
    fun get() = value
}

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.jetbrains.kotlinx.lincheck.verifier.*
   import org.junit.*
   
   class Counter {
       @Volatile
       private var value = 0
   
       fun inc(): Int = ++value
       fun get() = value
   }
   
   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 сгенерирует сценарии, похожие на сценарий ниже:

   Init part:
   [inc(), inc()]
   Parallel part:
   | get() | inc() |
   | inc() | get() |
   Post part:
   [inc()]
   

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

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

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

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

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

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

Поскольку анализ меньших сценариев проще, минимизация сценариев включена по умолчанию. Чтобы отключить эту функцию, добавьте 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 Counter {
       @Volatile
       private var value = 0
   
       fun inc(): Int = ++value
       fun get() = value
   }
   
   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 =
   STATE: 0
   Parallel part:
   | inc(): 1 | inc(): 1 |
   STATE: 1
   = The following interleaving leads to the error =
   Parallel part trace:
   |                      | inc()                                                |
   |                      |   inc(): 1 at CounterTest.inc(CounterTest.kt:42)     |
   |                      |     value.READ: 0 at Counter.inc(CounterTest.kt:35)  |
   |                      |     switch                                           |
   | inc(): 1             |                                                      |
   | STATE: 1             |                                                      |
   |   thread is finished |                                                      |
   |                      |     value.WRITE(1) at Counter.inc(CounterTest.kt:35) |
   |                      |     STATE: 1                                         |
   |                      |     value.READ: 1 at Counter.inc(CounterTest.kt:35)  |
   |                      |   result: 1                                          |
   |                      |   thread is finished                                 |
   

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

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

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

См. также

Узнайте, как оптимизировать и увеличить охват стратегии проверки моделей с помощью модульного тестирования.