search

JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
589 stars 34 forks source link

`IllegalStateException`: Trying to switch the execution to thread 0 #403

Open de-shyt opened 1 month ago

de-shyt commented 1 month ago 
java.lang.IllegalStateException: Trying to switch the execution to thread 0,
but only the following threads are eligible to switch: [2]
    at org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingStrategy.chooseThread(ModelCheckingStrategy.kt:306)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.doSwitchCurrentThread(ManagedStrategy.kt:524)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread(ManagedStrategy.kt:500)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.switchCurrentThread$default(ManagedStrategy.kt:493)
    at org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy.newSwitchPoint(ManagedStrategy.kt:402)
    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 com.deshyt.buffered.ChannelSegment.getState$kotlin_channels(ChannelSegment.kt:40)
    at com.deshyt.buffered.BufferedChannel.updateCellOnSend(BufferedChannel.kt:87)
    at com.deshyt.buffered.BufferedChannel.send(BufferedChannel.kt:74)
    at com.deshyt.ChannelTestBase.send(ChannelTestBase.kt:22)
    at org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution1.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:1583)

The final part of the stack trace where the unsuccessful attempts to switch are:

|    updateCellOnSend(2,ChannelSegment#2,0,<cont>): true at BufferedChannel.send(BufferedChannel.kt:74)                                      |
|      ChannelSegment#2.getState$kotlin_channels(0): IN_BUFFER at BufferedChannel.updateCellOnSend(BufferedChannel.kt:87)                    |
|        data.READ: AtomicReferenceArray#2 at ChannelSegment.getState$kotlin_channels(ChannelSegment.kt:40)                                  |
|        switch                                                                                                                              |
|        AtomicReferenceArray#2[1].get(): IN_BUFFER at ChannelSegment.getState$kotlin_channels(ChannelSegment.kt:40)                         |
|      switch                                                                                                                                |
|      bufferEnd.READ: 3 at BufferedChannel.updateCellOnSend(BufferedChannel.kt:88)                                                          |
|      switch                                                                                                                                |
|      receiversCounter.READ: 2 at BufferedChannel.updateCellOnSend(BufferedChannel.kt:89)                                                   |
|      switch                                                                                                                                |
|      ChannelSegment#2.casState$kotlin_channels(0,IN_BUFFER,BUFFERED): true at BufferedChannel.updateCellOnSend(BufferedChannel.kt:93)      |
|        data.READ: AtomicReferenceArray#2 at ChannelSegment.casState$kotlin_channels(ChannelSegment.kt:46)                                  |
|        switch                                                                                                                              |
|        AtomicReferenceArray#2[1].compareAndSet(IN_BUFFER,BUFFERED): true at ChannelSegment.casState$kotlin_channels(ChannelSegment.kt:46)  |
|  result: void                                                                                                                              |

The code is stored here and can be reproduced by running Buffered1ChannelTest. I am using blocking operations, and for this purpose I created a blockingActor method in the Lincheck library. The corresponding PR is here.

Lincheck version: 2.34 Lincheck plugin version: 0.9 Intellij IDEA version: 2024.2.3