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

Контролируемые источники недетерминизма

При запуске теста со стратегией проверки модели Lincheck контролирует следующие источники недетерминизма:

• Переключение потоков. Вместо того чтобы полагаться на JVM при переключении потоков, Lincheck вставляет явные инструкции переключения потоков в точках доступа к общей памяти (read и write) или в точках синхронизации, например при захвате и освобождении блокировки, park/unpark, wait/notify и в других случаях.

• Генераторы случайных чисел. Lincheck фиксирует начальное значение генератора случайных чисел.

• Хеш-коды идентичности. Lincheck фиксирует хеш-коды идентичности объектов.

• Вызовы API времени. Lincheck перехватывает вызовы API времени и возвращает детерминированные результаты.

• Свойства верхнего уровня и companion object. При каждом запуске теста с проверкой модели Lincheck сбрасывает значения свойств var верхнего уровня и свойств companion object (эквивалентов глобальных переменных в Kotlin):

  @TestMethodOrder(MethodOrderer.OrderAnnotation::class)
  class VariableResetTest {
      companion object {
          private var atomicInt = AtomicInteger(0)
      }
  
      @Test
      @Order(1)
      fun modelCheckingTest() = Lincheck.runConcurrentTest {
          val t1 = thread { atomicInt.getAndIncrement() }
          val t2 = thread { atomicInt.getAndIncrement() }
  
          t1.join()
          t2.join()
  
          check(atomicInt.get() == 2)
      }
  
      @Test
      @Order(2)
      fun resetAfterModelCheckingTest() {
          // Verify `atomicInt` has been reset to 0 after `modelCheckingTest()`
          check(atomicInt.get() == 0)
      }
  
      @Test
      @Order(3)
      fun regularIncTest() {
          atomicInt.getAndIncrement()
          check(atomicInt.get() == 1)
      }
  
      @Test
      @Order(4)
      fun valuePersistsAfterRegularIncTest() {
          // Verify `atomicInt` still holds 1 after `regularIncTest()`
          check(atomicInt.get() == 1)
      }
  }
  

Неконтролируемые источники недетерминизма

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

Каждый неконтролируемый источник недетерминизма подробно описан в отдельном разделе:

• Переменные, локальные для потока

• Слабые ссылки

• Вызовы API ввода-вывода

Пример: расписания с одним переключением потоков

Посмотрите, как Lincheck моделирует расписания выполнения с одним вытесняющим переключением потоков в сценарии с двумя потоками:

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

Ослабленная модель памяти Java

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

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

Большинство ошибок конкурентного выполнения можно обнаружить даже при предположении о последовательной согласованности модели памяти. Однако Lincheck может пропустить некоторые ошибки, вызванные низкоуровневыми эффектами. Например, отсутствие модификатора @Volatile может привести к ошибке из-за буфера записи или переупорядочивания компилятором, которую средство проверки модели Lincheck обнаружить не сможет:

class RelaxedMemoryModelTest {
    var x = 0 // Not @Volatile
    var y = 0 // Not @Volatile

    @Test
    fun modelCheckingTest() = Lincheck.runConcurrentTest {
        thread {
            x = 1
            y = 1
        }
        thread {
            if (y == 1 && x == 0) {
                // Code in this block might be executed on real hardware because of
                // store buffer and compiler reordering.
                // Lincheck cannot model this behavior with model checking.
                error("Unreachable under sequential consistency")
            }
        }
    }
}

Потоки, созданные вне сценария

Lincheck может отслеживать только потоки, созданные внутри конкурентного сценария. Он может пропустить ошибки, возникающие во внешне созданных потоках, например при использовании диспетчера по умолчанию для корутин или общего пула потоков с Java ForkJoinPool.

class FixedThreadPoolDispatcherTest {
    @Test
    fun test() = Lincheck.runConcurrentTest {
        val dispatcher = Executors.newFixedThreadPool(nThreads).asCoroutineDispatcher()
        dispatcher.use {
            runBlocking(dispatcher) {
                val counter = AtomicInteger(0)
                val coro = launch {
                    while (isActive) { counter.getAndIncrement() }
                }
                coro.cancel()
                coro.join()
            }
        }
    }
}

class FixedThreadPoolExecutorServiceTest {
    @Test
    fun test() = Lincheck.runConcurrentTest {
        val executorService = Executors.newFixedThreadPool(nThreads)
        try {
            val counter = AtomicInteger(0)
            val task = Runnable { counter.getAndIncrement() }
            val future1 = executorService.submit(task)
            val future2 = executorService.submit(task)
            future1.get()
            future2.get()
        } finally {
            executorService.shutdown()
        }
    }
}

Переменные, локальные для потока

Lincheck не сбрасывает переменные, локальные для потока, при многократном запуске одного сценария (в отличие от свойств var верхнего уровня и свойств companion object). Это приводит к несоответствиям между запусками одного и того же теста.

Пример:

class ThreadLocalVariableTest {
    @Test
    fun modelCheckingTest() = Lincheck.runConcurrentTest {
        var counter = getLocalCounter()
        var t = thread { counter.getAndIncrement() }
        t.join()
        check(counter.get() == 1)
    }

    private fun getLocalCounter() = localCounter.get()
}

// Using ThreadLocal to create a variable leads to a failed test
private val localCounter: ThreadLocal<AtomicInteger> = ThreadLocal.withInitial {
    AtomicInteger(0)
}

Этот тест завершается с ошибкой, поскольку значение счетчика накапливается при запусках сценария:

| ---------------------------------------------------------------------------------------- |
|                   Main Thread                   |                Thread 1                |
| ---------------------------------------------------------------------------------------- |
| getLocalCounter(): AtomicInteger#1              |                                        |
| thread(block = Lambda#1): Thread#1              |                                        |
| switch (reason: waiting for Thread 1 to finish) |                                        |
|                                                 | run()                                  |
|                                                 |   counter ➜ AtomicInteger#1            |
|                                                 |   AtomicInteger#1.getAndIncrement(): 2 |
| Thread#1.join()                                 |                                        |
| counter.element ➜ AtomicInteger#1               |                                        |
| AtomicInteger#1.get(): 3                        |                                        |
| ---------------------------------------------------------------------------------------- |

class ThreadLocalVariableWorkaroundTest {
    var threadLocalCounters = ConcurrentHashMap<Long, AtomicInteger>()

    @Test
    fun modelCheckingTest() = Lincheck.runConcurrentTest {
        var counter = getLocalCounter()
        var t = thread { counter.getAndIncrement() }
        t.join()
        check(counter.get() == 1)
    }

    private fun getLocalCounter() = threadLocalCounters.computeIfAbsent(Thread.currentThread().id) {
        AtomicInteger(0)
    }
}

Слабые ссылки

Lincheck не контролирует, когда сборщик мусора удаляет объекты, на которые ссылаются только слабые ссылки. Вызов get() для таких объектов дает недетерминированные результаты. Тест может успешно пройти, несмотря на использование слабых ссылок, но если Lincheck обнаружит несоответствие между запусками одного и того же теста, он сообщит об ошибке недетерминизма.

Вызовы API времени

Lincheck имитирует вызовы java.lang.System.nanoTime() и java.lang.System.currentTimeMillis(), всегда возвращая заранее заданную константу, чтобы предотвратить несоответствия между запусками одного и того же теста.

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

Вызовы API ввода-вывода

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

Вызовы API ввода-вывода приводят к java.lang.IllegalStateException:

class FilesCreateTempFileTest {
    @Operation
    fun operation(): List<String> = List(10) {
        val tempFile = Files.createTempFile("test-prefix", ".txt")
        require(Files.exists(tempFile)) { "File was not created: $tempFile" }
        tempFile.toString()
    }

    // The test fails with the following error message:
    // "java.lang.IllegalStateException: File operations are not supported in Lincheck"
    @Test
    fun modelChecking() = ModelCheckingOptions().check(this::class)
}

Виртуальные потоки

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