Halting problem when using I/O

[I-Gleb]

Lincheck version 2.34

After adding debug output to the data structure testing is not finishing.

DS under test:

package day1

import kotlinx.atomicfu.*

interface MyQueue<E> {
    fun enqueue(element: E)
    fun dequeue(): E?
    fun validate() {}
}

class MSQueue<E> : MyQueue<E> {
    private val head: AtomicRef<Node<E>>
    private val tail: AtomicRef<Node<E>>

    init {
        val dummy = Node<E>(null)
        head = atomic(dummy)
        tail = atomic(dummy)
    }

    override fun enqueue(element: E) {
        val newTail = Node(element)
        while (true) {
            val currentTail  = tail.value
            if (currentTail.next.compareAndSet(null, newTail)){
                tail.compareAndSet(currentTail, newTail)
                println("Enqueue $element" + toString())
                return
            } else {
                tail.compareAndSet(currentTail, currentTail.next.value!!)
            }
        }
    }

    override fun dequeue(): E? {
        while (true) {
            val currentHead = head.value
            val currentNext = currentHead.next.value ?: return null

            if (head.compareAndSet(currentHead, currentNext)){
                val result = currentNext.element
                println("Dequeued $result" + toString())
                return result
            }
        }
    }

    private class Node<E>(
        var element: E?
    ) {
        val next = atomic<Node<E>?>(null)
    }

    override fun toString(): String {
        val builder = StringBuilder(" | ")
        var current = head.value
        while (current != tail.value) {
            builder.append(current.element)
            builder.append(" ")
            current = current.next.value!!
        }
        builder.append(" | ${hashCode()}")
        return builder.toString()
    }
}

Test class:

package day1

import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.paramgen.*
import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.junit.*
import org.junit.runners.*
import kotlin.reflect.*

@Param(name = "element", gen = IntGen::class, conf = "0:3")
abstract class AbstractQueueTest(
    private val queue: MyQueue<Int>,
    checkObstructionFreedom: Boolean = true,
    threads: Int = 3,
    actorsBefore: Int = 1
) : TestBase(
    sequentialSpecification = IntQueueSequential::class,
    checkObstructionFreedom = checkObstructionFreedom,
    threads = threads,
    actorsBefore = actorsBefore
) {
    @Operation
    fun enqueue(@Param(name = "element") element: Int) = queue.enqueue(element)

    @Operation
    fun dequeue() = queue.dequeue()

    @Validate
    fun validate() = queue.validate()
}

class IntQueueSequential {
    private val q = ArrayList<Int>()

    fun enqueue(element: Int) {
        q.add(element)
    }

    fun dequeue() = q.removeFirstOrNull()
    fun remove(element: Int) = q.remove(element)
}

@FixMethodOrder(MethodSorters.NAME_ASCENDING)
abstract class TestBase(
    val sequentialSpecification: KClass<*>,
    val checkObstructionFreedom: Boolean = true,
    val scenarios: Int = 150,
    val threads: Int = 3,
    val actorsBefore: Int = 1
) {
    @Test
    fun modelCheckingTest() = try {
        ModelCheckingOptions()
            .iterations(scenarios)
            .invocationsPerIteration(10_000)
            .actorsBefore(actorsBefore)
            .threads(threads)
            .actorsPerThread(2)
            .actorsAfter(0)
            .checkObstructionFreedom(checkObstructionFreedom)
            .sequentialSpecification(sequentialSpecification.java)
            .apply { customConfiguration() }
            .check(this::class.java)
    } catch (t: Throwable) {
        throw t
    }

    protected open fun Options<*, *>.customConfiguration() {}
}

class MSQueueTest : AbstractQueueTest(MSQueue())

[ndkoval]

Thanks for the issue! I suppose we need to ignore println calls in Lincheck.