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.ClassCastException
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//day2.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 day2
import kotlinx.atomicfu.*
interface MyQueue<E> {
fun enqueue(element: E)
fun dequeue(): E?
fun validate() {}
}
class FAABasedQueue<E> : MyQueue<E> {
private val SEGM_SIZE = 2
class dumby<E>(val arr: AtomicArray<Any?> = atomicArrayOfNulls(2),
val id: Int = 0) {
val next = atomic<dumby<E>?>(null)
}
private val enqIdx = atomic(0)
private val deqIdx = atomic(0)
private val head: AtomicRef<dumby<E>>
private val tail: AtomicRef<dumby<E>>
init {
val dum = dumby<E>()
head = atomic(dum)
tail = atomic(dum)
}
fun getSegm(start: dumby<E>, id: Int): dumby<E> {
val newDumby = dumby<E>(id = start.id + 1)
if (id > start.id) {
return if (start.next.compareAndSet(null, newDumby)) {
tail.compareAndSet(start, newDumby)
newDumby
} else {
tail.compareAndSet(start, start.next.value!!)
start.next.value!!
}
}
return start
}
fun getSegmBack(start: dumby<E>, id: Int): dumby<E> {
start.next.compareAndSet(null, dumby<E>(id = start.id + 1))
val startNext = start.next.value!!
if (id > start.id) {
if (head.compareAndSet(start, startNext)) {
return startNext
}
}
return start
}
override fun enqueue(element: E) {
while (true) {
val i = enqIdx.getAndIncrement()
val curTail = tail.value
val s = getSegm(curTail, i / SEGM_SIZE)
if (s.arr[i % SEGM_SIZE].compareAndSet(null, element)) {
return
}
}
}
override fun dequeue(): E? {
while (true) {
if (deqIdx.value >= enqIdx.value) {
return null
}
val i = deqIdx.getAndIncrement()
val curHead = head.value
val s = getSegmBack(curHead, i / SEGM_SIZE)
if (s.arr[i % SEGM_SIZE].compareAndSet(null, POISONED)) {
continue
}
return s.arr[i % SEGM_SIZE].value as E?
}
}
}
private val POISONED = Any()
Test class:
package day2
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.jetbrains.kotlinx.lincheck.strategy.stress.*
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 FAABasedQueueTest : AbstractQueueTest(FAABasedQueue())
Lincheck version 2.34
Trace:
DS under test:
Test class: