Busy-wait loop causes OutOfMemoryErrorException in Lincheck

[I-Gleb]

Lincheck version 2.34

After adding busy-wait loop to the data structure an exception in Lincheck appeared.

Trace:

org.jetbrains.kotlinx.lincheck.LincheckAssertionError: 
Wow! You've caught a bug in Lincheck.
We kindly ask to provide an issue here: https://github.com/JetBrains/lincheck/issues,
attaching a stack trace printed below and the code that causes the error.

Exception stacktrace:
java.lang.OutOfMemoryError: Java heap space

	at app//org.jetbrains.kotlinx.lincheck.LinChecker$check$1.invoke(LinChecker.kt:48)
	at app//org.jetbrains.kotlinx.lincheck.LinChecker$check$1.invoke(LinChecker.kt:47)
	at app//org.jetbrains.kotlinx.lincheck.LinChecker.checkImpl$lincheck(LinChecker.kt:67)
	at app//org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt:47)
	at app//org.jetbrains.kotlinx.lincheck.LinChecker$Companion.check(LinChecker.kt:195)
	at app//org.jetbrains.kotlinx.lincheck.LinCheckerKt.check(LinChecker.kt:295)
	at app//day3.TestBase.modelCheckingTest(Unknown Source)
	at java.base@17.0.11/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@17.0.11/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
	at java.base@17.0.11/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@17.0.11/java.lang.reflect.Method.invoke(Method.java:568)
	at app//org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:59)
	at app//org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
	at app//org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:56)
	at app//org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
	at app//org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
	at app//org.junit.runners.BlockJUnit4ClassRunner$1.evaluate(BlockJUnit4ClassRunner.java:100)
	at app//org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:366)
	at app//org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:103)
	at app//org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:63)
	at app//org.junit.runners.ParentRunner$4.run(ParentRunner.java:331)
	at app//org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:79)
	at app//org.junit.runners.ParentRunner.runChildren(ParentRunner.java:329)
	at app//org.junit.runners.ParentRunner.access$100(ParentRunner.java:66)
	at app//org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:293)
	at app//org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
	at app//org.junit.runners.ParentRunner.run(ParentRunner.java:413)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.runTestClass(JUnitTestClassExecutor.java:110)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:58)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:38)
	at org.gradle.api.internal.tasks.testing.junit.AbstractJUnitTestClassProcessor.processTestClass(AbstractJUnitTestClassProcessor.java:62)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.processTestClass(SuiteTestClassProcessor.java:51)
	at java.base@17.0.11/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@17.0.11/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
	at java.base@17.0.11/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@17.0.11/java.lang.reflect.Method.invoke(Method.java:568)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
	at jdk.proxy1/jdk.proxy1.$Proxy2.processTestClass(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$2.run(TestWorker.java:176)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:133)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)

DS under test:

package day3

import kotlinx.atomicfu.*

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

interface MyQueueWithRemove<E> : Queue<E> {
    fun remove(element: E): Boolean
    fun checkNoRemovedElements() {}
}

class MSQueueWithConstantTimeRemove<E> : MyQueueWithRemove<E> {
    private val head: AtomicRef<Node<E>>
    private val tail: AtomicRef<Node<E>>

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

    override fun enqueue(element: E) {
        while (true) {
            val curTail = tail.value
            val node = Node(element, curTail)
            if (curTail.next.compareAndSet(null, node)) {
                tail.compareAndSet(curTail, node)
                if (curTail.extractedOrRemoved) curTail.remove()
                return
            } else {
                tail.compareAndSet(curTail, curTail.next.value!!)
            }
        }
    }

    override fun dequeue(): E? {
        while (true) {
            val curHead = head.value
            val curHeadNext = curHead.next.value ?: return null
            if (head.compareAndSet(curHead, curHeadNext) && curHeadNext.markExtractedOrRemoved())
                return curHeadNext.element
        }
    }

    override fun remove(element: E): Boolean {
        var node = head.value
        while (true) {
            val next = node.next.value
            if (next == null) return false
            node = next
            if (node.element == element && node.remove()) return true
        }
    }

    override fun checkNoRemovedElements() {
        check(head.value.prev.value == null) {
            "`head.prev` must be null"
        }
        check(tail.value.next.value == null) {
            "tail.next must be null"
        }
        var node = head.value
        while (true) {
            if (node !== head.value && node !== tail.value) {
                check(!node.extractedOrRemoved) {
                    "Removed node with element ${node.element} found in the middle of the queue"
                }
            }
            val nodeNext = node.next.value
            if (nodeNext == null) break
            val nodeNextPrev = nodeNext.prev.value
            check(nodeNextPrev != null) {
                "The `prev` pointer of node with element ${nodeNext.element} is `null`, while the node is in the middle of the queue"
            }
            check(nodeNextPrev == node) {
                "node.next.prev != node; `node` contains ${node.element}, `node.next` contains ${nodeNext.element}"
            }
            node = nodeNext
        }
    }

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

        private val _extractedOrRemoved = atomic(false)
        val extractedOrRemoved get() = _extractedOrRemoved.value

        fun markExtractedOrRemoved(): Boolean = _extractedOrRemoved.compareAndSet(false, true)

        fun remove(): Boolean {
            val result = markExtractedOrRemoved()
            if (!result) return false

            val myNext = next.value
            prev.value?.next?.compareAndSet(this, myNext)
            myNext?.prev?.compareAndSet(this, prev.value)

            // Ensure the node is fully removed before nullifying the pointers
            while (next.value != null || prev.value != null) {
                // Busy-wait until the node is fully removed
            }

            next.value = null
            prev.value = null
            return true
        }
    }
}

Test class:

package day3

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: Queue<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() {}
}

abstract class AbstractQueueWithRemoveTest(
    private val queue: MyQueueWithRemove<Int>,
    checkObstructionFreedom: Boolean = true,
) : AbstractQueueTest(
    queue = queue,
    checkObstructionFreedom = checkObstructionFreedom,
    threads = 3,
    actorsBefore = 4
) {
    @Operation
    fun remove(@Param(name = "element") element: Int) = queue.remove(element)
}

@Param(name = "element", gen = IntGen::class, conf = "0:3")
class MSQueueWithLinearTimeNonParallelRemoveTest: TestBase(
    sequentialSpecification = IntQueueSequential::class,
    checkObstructionFreedom = true,
    threads = 2,
    actorsBefore = 5
) {
    private val queue = MSQueueWithLinearTimeNonParallelRemove<Int>()

    @Operation(nonParallelGroup = "removeAndEnqueue")
    fun enqueue(@Param(name = "element") element: Int) = queue.enqueue(element)

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

    @Operation(nonParallelGroup = "removeAndEnqueue")
    fun remove(@Param(name = "element") element: Int) = queue.remove(element)

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

class MSQueueWithConstantTimeRemoveTest : AbstractQueueWithRemoveTest(MSQueueWithConstantTimeRemove())