Open
Description
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 [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
at [email protected]/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at [email protected]/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 [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
at [email protected]/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at [email protected]/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())
Metadata
Metadata
Assignees
Labels
No labels