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

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

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

Для соблюдения ограничения одного потребителя убедитесь, что все poll() и peek() операции потребления вызываются из одного потока. Для этого объявите группу операций для последовательного выполнения:

1. Объявите аннотацию @OpGroupConfig, чтобы создать группу операций для последовательного выполнения, укажите имя группы и установите параметр nonParallel в значение true.

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

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

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

// Declare a group of operations that should not be executed in parallel:
@OpGroupConfig(name = "consumer", nonParallel = true)
class MPSCQueueTest {
    private val queue = MpscLinkedAtomicQueue<Int>()

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

    @Operation(group = "consumer") 
    fun poll(): Int? = queue.poll()

    @Operation(group = "consumer")
    fun peek(): Int? = queue.peek()

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

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

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

= Iteration 15 / 100 =
Execution scenario (init part):
[offer(1), offer(4), peek(), peek(), offer(-6)]
Execution scenario (parallel part):
| poll()   | offer(6)  |
| poll()   | offer(-1) |
| peek()   | offer(-8) |
| offer(7) | offer(-5) |
| peek()   | offer(3)  |
Execution scenario (post part):
[poll(), offer(-6), peek(), peek(), peek()]

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