coroutine finishing early

[btwilk]

Version: 2.15
I'm model checking some code that uses Mutex. I ran into a case where lincheck incorrectly considers a coroutine that should still be running to have finished. Here is a minimal example:

class CoroutineLinTest {

    private var x = AtomicInteger()
    private val mutex = Mutex()

    @Operation(cancellableOnSuspension = false, allowExtraSuspension = true)
    suspend fun getAndInc(): Int {
        while (true) {
            val snapshot = x.get()
            mutex.withLock {
                if (snapshot == x.get()) {
                    return x.getAndIncrement()
                }
            }
        }
    }

    @Test
    fun test() = ModelCheckingOptions().check(this::class)
}

Here is the assertion error: coroutine-assertion-error.txt

In contrast, the equivalent code with thread synchronization model checks as expected (no counterexamples found):

class ThreadLinTest {

    private var x = AtomicInteger()
    private val mutex = Object()

    @Operation
    fun getAndInc(): Int {
        while (true) {
            val snapshot = x.get()
            synchronized(mutex) {
                if (snapshot == x.get()) {
                    return x.getAndIncrement()
                }
            }
        }
    }

    @Test
    fun test() = ModelCheckingOptions().check(this::class)
}

[ndkoval]

@btwilk Unfortunetely, we do not support multiple suspensions at the moment, but we are considering imrpoving this part later.

[alefedor]

@btwilk
Suprisingly, we did not have applications with multiple suspension points per operation.
Coroutine-based data structures (like queues or channels) mostly have only one natural suspension point.
I opened a more general issue, so I am closing this one