Hi, I have received the following error when using lincheck 2.34 :
= Validation function validate has failed =
| ------------------------------------- |
| Thread 1 |
| ------------------------------------- |
| dequeue(): 0 |
| ------------------------------------- |
| validate(): IndexOutOfBoundsException |
| ------------------------------------- |
java.lang.IndexOutOfBoundsException: Index 1 out of bounds for length 1
at java.base/jdk.internal.util.Preconditions.outOfBounds(Preconditions.java:64)
at java.base/jdk.internal.util.Preconditions.outOfBoundsCheckIndex(Preconditions.java:70)
at java.base/jdk.internal.util.Preconditions.checkIndex(Preconditions.java:266)
at java.base/java.util.Objects.checkIndex(Objects.java:361)
at java.base/java.util.ArrayList.get(ArrayList.java:427)
at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.getCurrentActorIsBlocking(ManagedStrategy.kt:306)
at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.failIfObstructionFreedomIsRequired(ManagedStrategy.kt:295)
at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPoint(ManagedStrategy.kt:368)
at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPointOnAtomicMethodCall(ManagedStrategy.kt:964)
at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.beforeMethodCall(ManagedStrategy.kt:903)
at sun.nio.ch.lincheck.Injections.beforeMethodCall(Injections.java:249)
at day2.DummyQueue.validate(DummyQueue.kt:14)
at MyLinCheckTest.validate(MyLinCheckTest.kt:30)
at org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution67.run(Unknown Source)
at org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.testThreadRunnable$lambda$10(FixedActiveThreadsExecutor.kt:172)
at java.base/java.lang.Thread.run(Thread.java:840)
Simplified datastructure under test:
Also, the issue seems to disappear with smaller array sizes..
import java.util.concurrent.atomic.AtomicReferenceArray
class DummyQueue {
private val atomicArray = AtomicReferenceArray<Any?>(1024)
fun dequeue(): Int? {
return 0
}
fun validate() {
for (i in 0 until atomicArray.length()) {
check(atomicArray[i] == null) {
"bla"
}
}
}
}
Test case:
class MyLinCheckTest {
private val queue = DummyQueue()
@Test
fun modelCheckingTest() = ModelCheckingOptions()
.iterations(150)
.invocationsPerIteration(10_000)
.actorsBefore(1)
.threads(3)
.actorsPerThread(3)
.actorsAfter(0)
.checkObstructionFreedom(true)
.check(this::class.java)
@Operation
fun dequeue() = queue.dequeue()
@Validate
fun validate() = queue.validate()
}
Hi, I have received the following error when using lincheck 2.34 :
Simplified datastructure under test: Also, the issue seems to disappear with smaller array sizes..
Test case: