search

JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
538 stars 31 forks source link

IllegalStateException: Trying to switch the execution... #307

Open durban opened 2 months ago

durban commented 2 months ago

Lincheck version 2.29.

Steps to reproduce (unfortunately I don't know how to minimize):

git clone https://github.com/durban/choam.git
cd choam
git checkout 2711aabe
sbt "stressLinchk/testOnly dev.tauri.choam.core.RxnModelTest"

It runs for a long time, then it fails with Wow! You've caught a bug in Lincheck.

I've got 2 different stacktraces (with 2 different runs), so I'm pasting both of them.

First try:

dev.tauri.choam.core.RxnModelTest:
==> X dev.tauri.choam.core.RxnModelTest.Model checking Rxn  3008.936s 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.IllegalStateException: Trying to switch the execution to thread 2,
but only the following threads are eligible to switch: [1]
        at org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingStrategy.chooseThread(ModelCheckingStrategy.kt:273)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.doSwitchCurrentThread(ManagedStrategy.kt:488)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread(ManagedStrategy.kt:452)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread$default(ManagedStrategy.kt:450)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPointRegular(ManagedStrategy.kt:352)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPoint(ManagedStrategy.kt:329)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.beforeReadField(ManagedStrategy.kt:676)
        at org.jetbrains.kotlinx.lincheck.Injections.beforeReadField(Injections.kt:185)
        at dev.tauri.choam.refs.RefU1.unsafeGetVersionV(RefU1.java:119)
        at dev.tauri.choam.internal.mcas.emcas.Emcas.readValue(Emcas.scala:309)
        at dev.tauri.choam.internal.mcas.emcas.Emcas.readIntoHwd(Emcas.scala:391)
        at dev.tauri.choam.internal.mcas.emcas.EmcasThreadContext.readIntoHwd(EmcasThreadContext.scala:129)
        at dev.tauri.choam.core.Rxn$InterpreterState.entryAbsent(Rxn.scala:738)
        at dev.tauri.choam.core.Rxn$InterpreterState.entryAbsent(Rxn.scala:647)
        at dev.tauri.choam.internal.mcas.Hamt.visit(Hamt.scala:270)
        at dev.tauri.choam.internal.mcas.Hamt.computeOrModify(Hamt.scala:175)
        at dev.tauri.choam.core.Rxn$InterpreterState.loop(Rxn.scala:1203)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSyncWithContext(Rxn.scala:1442)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSync(Rxn.scala:1434)
        at dev.tauri.choam.core.Rxn.unsafePerform(Rxn.scala:255)
        at dev.tauri.choam.package$AxnSyntax2.unsafeRun(package.scala:78)
        at dev.tauri.choam.core.RxnModelTest$TestState.readWrite(RxnModelTest.scala:79)
        at org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution466.run(Unknown Source)
        at org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.testThreadRunnable$lambda$7(FixedActiveThreadsExecutor.kt:172)
        at java.base/java.lang.Thread.run(Thread.java:840)

    at org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt:44)
    at org.jetbrains.kotlinx.lincheck.LinChecker$Companion.check(LinChecker.kt:170)
    at org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt)
    at dev.tauri.choam.core.RxnModelTest.$anonfun$new$1(RxnModelTest.scala:35)
    at dev.tauri.choam.BaseLinchkSpec.$anonfun$test$2(BaseLinchkSpec.scala:41)

Second try:

dev.tauri.choam.core.RxnModelTest:
==> X dev.tauri.choam.core.RxnModelTest.Model checking Rxn  831.217s 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.IllegalStateException: Trying to switch the execution to thread 2,
but only the following threads are eligible to switch: [0]
        at org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingStrategy.chooseThread(ModelCheckingStrategy.kt:273)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.doSwitchCurrentThread(ManagedStrategy.kt:488)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread(ManagedStrategy.kt:452)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread$default(ManagedStrategy.kt:450)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPointRegular(ManagedStrategy.kt:352)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPoint(ManagedStrategy.kt:329)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.beforeReadField(ManagedStrategy.kt:676)
        at org.jetbrains.kotlinx.lincheck.Injections.beforeReadField(Injections.kt:185)
        at dev.tauri.choam.internal.mcas.emcas.GlobalContextBase.getCommitTs(GlobalContextBase.java:68)
        at dev.tauri.choam.internal.mcas.emcas.EmcasThreadContext.start(EmcasThreadContext.scala:138)
        at dev.tauri.choam.core.Rxn$InterpreterState.desc(Rxn.scala:682)
        at dev.tauri.choam.core.Rxn$InterpreterState.loop(Rxn.scala:1203)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSyncWithContext(Rxn.scala:1442)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSync(Rxn.scala:1434)
        at dev.tauri.choam.core.Rxn.unsafePerform(Rxn.scala:255)
        at dev.tauri.choam.package$AxnSyntax2.unsafeRun(package.scala:78)
        at dev.tauri.choam.core.RxnModelTest$TestState.readWrite(RxnModelTest.scala:79)
        at org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution77.run(Unknown Source)
        at org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.testThreadRunnable$lambda$7(FixedActiveThreadsExecutor.kt:172)
        at java.base/java.lang.Thread.run(Thread.java:840)

    at org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt:44)
    at org.jetbrains.kotlinx.lincheck.LinChecker$Companion.check(LinChecker.kt:170)
    at org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt)
    at dev.tauri.choam.core.RxnModelTest.$anonfun$new$1(RxnModelTest.scala:35)
    at dev.tauri.choam.BaseLinchkSpec.$anonfun$test$2(BaseLinchkSpec.scala:41)
durban commented 2 months ago

Some further information: on a third try, I've got 2 exceptions from a single run:

==> X dev.tauri.choam.core.RxnModelTest.Model checking Rxn  1408.437s java.lang.IllegalStateException: Non-determinism found. Probably caused by non-deterministic code (WeakHashMap, Object.hashCode, etc).
== Reporting the first execution without execution trace ==
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.IllegalStateException: Trying to switch the execution to thread 0,
but only the following threads are eligible to switch: [1]
        at org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingStrategy.chooseThread(ModelCheckingStrategy.kt:273)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.doSwitchCurrentThread(ManagedStrategy.kt:488)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread(ManagedStrategy.kt:452)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread$default(ManagedStrategy.kt:450)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPointRegular(ManagedStrategy.kt:352)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPoint(ManagedStrategy.kt:329)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.beforeReadField(ManagedStrategy.kt:676)
        at org.jetbrains.kotlinx.lincheck.Injections.beforeReadField(Injections.kt:185)
        at dev.tauri.choam.internal.mcas.emcas.GlobalContextBase.getCommitTs(GlobalContextBase.java:68)
        at dev.tauri.choam.internal.mcas.emcas.EmcasThreadContext.start(EmcasThreadContext.scala:138)
        at dev.tauri.choam.core.Rxn$InterpreterState.desc(Rxn.scala:682)
        at dev.tauri.choam.core.Rxn$InterpreterState.loop(Rxn.scala:1316)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSyncWithContext(Rxn.scala:1442)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSync(Rxn.scala:1434)
        at dev.tauri.choam.core.Rxn.unsafePerform(Rxn.scala:255)
        at dev.tauri.choam.package$AxnSyntax2.unsafeRun(package.scala:78)
        at dev.tauri.choam.core.RxnModelTest$TestState.readOnly(RxnModelTest.scala:89)
        at org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution273.run(Unknown Source)
        at org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.testThreadRunnable$lambda$7(FixedActiveThreadsExecutor.kt:172)
        at java.base/java.lang.Thread.run(Thread.java:840)

== Reporting the second execution ==
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.IllegalStateException: Trying to switch the execution to thread 0,
but only the following threads are eligible to switch: [1]
        at org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingStrategy.chooseThread(ModelCheckingStrategy.kt:273)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.doSwitchCurrentThread(ManagedStrategy.kt:488)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread(ManagedStrategy.kt:452)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread$default(ManagedStrategy.kt:450)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPointInReplayMode(ManagedStrategy.kt:370)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPoint(ManagedStrategy.kt:322)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPointOnAtomicMethodCall(ManagedStrategy.kt:948)
        at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.beforeAtomicMethodCall(ManagedStrategy.kt:910)
        at org.jetbrains.kotlinx.lincheck.Injections.beforeAtomicMethodCall(Injections.kt:270)
        at dev.tauri.choam.internal.mcas.emcas.EmcasDescriptorBase.cleanWordsForGc(EmcasDescriptorBase.java:122)
        at dev.tauri.choam.internal.mcas.emcas.EmcasDescriptor.wasFinalized(EmcasDescriptor.scala:137)
        at dev.tauri.choam.internal.mcas.emcas.Emcas.MCAS(Emcas.scala:899)
        at dev.tauri.choam.internal.mcas.emcas.Emcas.tryPerformDebug(Emcas.scala:1012)
        at dev.tauri.choam.internal.mcas.emcas.EmcasThreadContext.tryPerformInternal(EmcasThreadContext.scala:123)
        at dev.tauri.choam.internal.mcas.Mcas$ThreadContext.tryPerform(Mcas.scala:185)
        at dev.tauri.choam.internal.mcas.Mcas$ThreadContext.tryPerform$(Mcas.scala:178)
        at dev.tauri.choam.internal.mcas.emcas.EmcasThreadContext.tryPerform(EmcasThreadContext.scala:26)
        at dev.tauri.choam.core.Rxn$InterpreterState.performMcas(Rxn.scala:1080)
        at dev.tauri.choam.core.Rxn$InterpreterState.loop(Rxn.scala:1138)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSyncWithContext(Rxn.scala:1442)
        at dev.tauri.choam.core.Rxn$InterpreterState.interpretSync(Rxn.scala:1434)
        at dev.tauri.choam.core.Rxn.unsafePerform(Rxn.scala:255)
        at dev.tauri.choam.package$AxnSyntax2.unsafeRun(package.scala:78)
        at dev.tauri.choam.core.RxnModelTest$TestState.writeOnly(RxnModelTest.scala:73)
        at org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution278.run(Unknown Source)
        at org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.testThreadRunnable$lambda$7(FixedActiveThreadsExecutor.kt:172)
        at java.base/java.lang.Thread.run(Thread.java:840)

    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.collectTrace(ManagedStrategy.kt:229)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.checkResult(ManagedStrategy.kt:184)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingStrategy.runImpl(ModelCheckingStrategy.kt:72)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.run(ManagedStrategy.kt:123)
    at org.jetbrains.kotlinx.lincheck.LinChecker.run(LinChecker.kt:147)
    at org.jetbrains.kotlinx.lincheck.LinChecker.checkImpl(LinChecker.kt:85)
    at org.jetbrains.kotlinx.lincheck.LinChecker.checkImpl$lincheck(LinChecker.kt:54)
    at org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt:43)
    at org.jetbrains.kotlinx.lincheck.LinChecker$Companion.check(LinChecker.kt:170)
    at org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt)
    at dev.tauri.choam.core.RxnModelTest.$anonfun$new$1(RxnModelTest.scala:35)
    at dev.tauri.choam.BaseLinchkSpec.$anonfun$test$2(BaseLinchkSpec.scala:41)