kotlinx-lincheck icon indicating copy to clipboard operation
kotlinx-lincheck copied to clipboard

Published 20 hours ago • verified publisher icon Kotlin

IllegalStateException: Trying to switch the execution...

Open durban opened this issue 1 year ago • 3 comments

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 avatar Apr 19 '24 01:04 durban

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)

durban avatar Apr 19 '24 17:04 durban

Hi @durban! Thank you for this bug report! I've started working on it, but it requires some additional and complicated debugging actions, which can be done far more conveniently and rapidly in the Lincheck project. That's why I kindly ask you to provide the fat jar with the class from the failed test with exposed public operations. I'll use it this way in Kotlin: image

Thank you for the collaboration!

avpotapov00 avatar Jul 07 '24 14:07 avpotapov00

I've tried setting up building a fat JAR on this branch: https://github.com/durban/choam/tree/lc307

A fat JAR can be built like this:

git clone https://github.com/durban/choam.git
cd choam
git checkout 8bbe6475  # the current head of the lc307 branch
sbt "lcdebug/assembly"

It should produce the fat JAR in the stress/lcdebug/target/scala-2.13/ directory (should be called like choam-stress-lcdebug-assembly-0.4-3b50561-20240711T201726Z-SNAPSHOT.jar or similar). The fat JAR has a class dev.tauri.choam.lcdebug.ChoamInstance, which should be possible to use from Kotlin (or Java, or whatever) like you show it in the screenshot.

Let me know if this works for you.

durban avatar Jul 11 '24 20:07 durban