Ограничения структуры данных

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

Рассмотрим очередь с одним потребителем из библиотеки JCTools. Напишем тест, чтобы проверить корректность ее poll(), peek(), и offer(x) операций.

В вашем файле build.gradle(.kts) добавьте зависимость JCTools:

dependencies {
    // jctools dependency
    testImplementation("org.jctools:jctools-core:3.3.0")
}

dependencies {
    // jctools dependency
    testImplementation "org.jctools:jctools-core:3.3.0"
}

Чтобы удовлетворить ограничению одного потребителя, убедитесь, что все poll() и peek() операции потребления вызываются из одного потока. Для этого можно установить параметр nonParallelGroup соответствующих аннотаций @Operation на одно и то же значение, например, "consumers".

Вот результат теста:

import org.jctools.queues.atomic.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.junit.*

class MPSCQueueTest {
    private val queue = MpscLinkedAtomicQueue<Int>()

    @Operation
    fun offer(x: Int) = queue.offer(x)

    @Operation(nonParallelGroup = "consumers") 
    fun poll(): Int? = queue.poll()

    @Operation(nonParallelGroup = "consumers")
    fun peek(): Int? = queue.peek()

    @Test
    fun stressTest() = StressOptions().check(this::class)

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

Вот пример сценария, сгенерированного для этого теста:

= Iteration 15 / 100 =
| --------------------- |
| Thread 1  | Thread 2  |
| --------------------- |
| poll()    |           |
| poll()    |           |
| peek()    |           |
| peek()    |           |
| peek()    |           |
| --------------------- |
| offer(-1) | offer(0)  |
| offer(0)  | offer(-1) |
| peek()    | offer(-1) |
| offer(1)  | offer(1)  |
| peek()    | offer(1)  |
| --------------------- |
| peek()    |           |
| offer(-2) |           |
| offer(-2) |           |
| offer(2)  |           |
| offer(-2) |           |
| --------------------- |

Обратите внимание, что все вызовы потребления poll() и peek() выполняются из одного потока, тем самым удовлетворяя ограничению «один потребитель».