Параметры выполнения операций
Lincheck предоставляет набор параметров, позволяющих управлять выполнением отдельных операций: например, запускать операции в одном потоке, выполнять операцию только один раз, помечать операцию как блокирующую и многое другое.
В этой статье вы узнаете о различных параметрах выполнения и о том, как их задавать.
Группы операций в одном потоке
Некоторые операции не должны выполняться параллельно, например операции в очередях с одним производителем и одним потребителем.
Чтобы создать группу операций, которые никогда не выполняются параллельно, используйте параметр nonParallelGroup при объявлении операций:
@Operation(nonParallelGroup = "consumers")
fun poll(): Int? = queue.poll()
@Operation(nonParallelGroup = "consumers")
fun peek(): Int? = queue.peek()
@Operation(nonParallelGroup = "producer")
fun offer(x: Int) = queue.offer(x)
@Operation
fun isEmpty(): Boolean = queue.isEmpty()
Lincheck гарантирует, что операции из непараллельной группы никогда не выполняются параллельно друг с другом. Однако они по-прежнему могут выполняться параллельно с операциями, не входящими в эту группу:
| --------------------- | | Thread 1 | Thread 2 | | --------------------- | | poll() | offer(0) | | peek() | offer(0) | | poll() | isEmpty() | | poll() | isEmpty() | | isEmpty() | isEmpty() | | --------------------- |
Операции, выполняемые один раз
Используйте параметр runOnce, чтобы выполнять операцию только один раз за вызов теста:
@Operation(runOnce = true)
fun singleOp() = struct.singleOp()
@Operation
fun regularOp() = struct.regularOp()
Пример сгенерированного сценария:
| ----------------------------- | | Thread 1 | Thread 2 | | ----------------------------- | | regularOp() | singleOp() | | regularOp() | regularOp() | | ----------------------------- |
Блокирующие операции
Используйте параметр blocking, если операция должна блокировать выполнение. Если тест проверяет неблокирующие гарантии, Lincheck не завершает тест с ошибкой, если выполнение останавливается на операции, помеченной параметром blocking:
@Operation(blocking = true)
fun put(key: Int, value: Int) = map.put(key, value)
Отменяемые операции
Используйте параметр cancellableOnSuspension, если операцию можно отменить при приостановке:
@Operation(cancellableOnSuspension = true)
suspend fun receive() = ch.receive()
Рассмотрим следующий тест канала:
@Param(name = "value", gen = IntGen::class, conf = "1:3")
class CancellableOnSuspensionTest {
private val ch = Channel<Int>()
@Operation
suspend fun send(@Param(name = "value") value: Int) = ch.send(value)
@Operation(cancellableOnSuspension = true)
suspend fun receive() = ch.receive()
@Test
fun test() = ModelCheckingOptions()
.iterations(50)
.invocationsPerIteration(1000)
// Report the scenarios even if the test has not failed
.logLevel(LoggingLevel.INFO)
.check(this::class)
}
|
|
|---|---|
|
Если | ----------------------------------- | | Thread 1 | Thread 2 | | ----------------------------------- | | send(3) | send(3) + cancel | | receive() | send(2) + cancel | | receive() | receive() | | receive() | receive() | | send(1) + cancel | receive() | | ----------------------------------- | |
Lincheck исследует сценарии, в которых | --------------------------------------- | | Thread 1 | Thread 2 | | --------------------------------------- | | send(3) | send(3) + cancel | | receive() + cancel | send(2) + cancel | | receive() + cancel | receive() | | receive() + cancel | receive() + cancel | | send(1) + cancel | receive() + cancel | | --------------------------------------- | |
Немедленная отмена
Если включен параметр cancellableOnSuspension и операция должна поддерживать немедленную отмену, можно также задать для promptCancellation значение true:
@Operation(cancellableOnSuspension = true, promptCancellation = true)
suspend fun receive() = ch.receive()
Рассмотрим следующий тест канала:
@Param(name = "value", gen = IntGen::class, conf = "1:3")
class PromptCancellationTest {
private val ch = Channel<Int>()
@Operation
suspend fun send(@Param(name = "value") value: Int) = ch.send(value)
@Operation(cancellableOnSuspension = true, promptCancellation = true)
suspend fun receive() = ch.receive()
@Test
fun test() = ModelCheckingOptions()
.iterations(50)
.invocationsPerIteration(1000)
// Report the scenarios even if the test has not failed
.logLevel(LoggingLevel.INFO)
.check(this::class)
}
|
|
|---|---|
|
Lincheck может попытаться отменить операцию только после того, как она действительно была приостановлена. Если операция возобновилась до попытки отмены Lincheck, отмена не срабатывает, и операция завершается обычным образом: | --------------------------------------- | | Thread 1 | Thread 2 | | --------------------------------------- | | send(2) | send(2) | | send(2) + cancel | receive() + cancel | | receive() + cancel | receive() | | receive() | send(3) + cancel | | send(2) | receive() | | --------------------------------------- | |
Lincheck может отменить операцию, даже если она уже возобновилась, но еще не успела выполниться. Это моделирует поведение в реальных условиях, когда сопрограмма может быть отменена между моментом возобновления и моментом фактической обработки результата: | ---------------------------------------------- | | Thread 1 | Thread 2 | | ---------------------------------------------- | | send(2) | send(2) | | send(2) + cancel | receive() + cancel | | receive() + cancel | receive() + prompt_cancel | | receive() | send(3) + cancel | | send(2) | receive() | | ---------------------------------------------- | |
См. также
© 2010–2026 JetBrains s.r.o. and Kotlin Programming Language contributors
Licensed under the Apache License, Version 2.0.
https://kotlinlang.org/docs/lincheck-operation-execution-options.html
