Not All Threads are Started During Invocation

[kevinly01]

Hi I have a use case where I have operations that depend on each other in order to proceed. I've tested the below code using Lincheck 2.23 and 2.18. While running my tests I noticed that despite me specifying the number of actors for the test run, there are some invocations during a iteration where operations are completely skipped. This results in the test eventually hanging due to a dependency on the other operation.

I've replicated a simple scenario below. As you can see during one of the invocations releasing lock is never called. And during the next iteration it hangs and gets stuck on Acquiring the lock. Is there a way to enforce LinCheck calling all actors during a invocation?

import java.util.concurrent.Semaphore

class Test {

    private val semaphore = Semaphore(0)

    init {
        println("Initializing")
    }

   @Operation(nonParallelGroup = "acquire")
    fun acquireLock() {
        println("Acquire lock")
        semaphore.acquire()
    }

    @Operation(nonParallelGroup = "release")
    fun releaseLock() {
        println("Release lock")
        semaphore.release()
    }

    @Test
     fun test() = ModelCheckingOptions()
        .threads(2)
        .actorsPerThread(1)
        .actorsBefore(0)
        .actorsAfter(0)
        .logLevel(LoggingLevel.INFO)
        .check(this::class)
}

  Test > test() STANDARD_OUT
  Initializing

    = Iteration 1 / 100 =
    | ----------------------------- |
    |   Thread 1    |   Thread 2    |
    | ----------------------------- |
    | releaseLock() | acquireLock() |
    | ----------------------------- |

    Initializing
    Acquire lock
    Initializing
    Acquire lock
    Release lock
    Initializing
    Release lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock
    Initializing
    Release lock
    Acquire lock

    = Iteration 2 / 100 =
    | ----------------------------- |
    |   Thread 1    |   Thread 2    |
    | ----------------------------- |
    | acquireLock() | releaseLock() |
    | ----------------------------- |

    Initializing
    Release lock
    Acquire lock
    Initializing
    Acquire lock.   <---------- Release is skipped here
    Initializing
    Acquire lock
    Release lock
    Initializing
    Acquire lock
   <----------------HANGS HERE

[btwilk]

It looks like it is hanging during the linearizability checking phase, which makes sense because it executes operations sequentially to generate valid linearizations. It would be useful if lincheck were able to detect and report this kind of deadlock in linearizability verification.

We need to provide a separate sequential spec that doesn't have these dependencies between operations. E.g., fixing the minimal example:

import org.jetbrains.kotlinx.lincheck.LoggingLevel
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
import org.junit.Test
import java.util.concurrent.Semaphore

class Test {

    private val semaphore = Semaphore(0)

    init {
        println("init")
    }

    @Operation(nonParallelGroup = "acquire")
    fun acquire(): Int {
        println("acquire")
        semaphore.acquire()
        return 1
    }

    @Operation(nonParallelGroup = "release")
    fun release(): Int {
        println("release")
        semaphore.release()
        return 2
    }

    @Test
    fun test() = ModelCheckingOptions()
        .sequentialSpecification(SequentialSpec::class.java)
        .threads(2)
        .actorsPerThread(1)
        .actorsBefore(0)
        .actorsAfter(0)
        .logLevel(LoggingLevel.INFO)
        .check(this::class)

    class SequentialSpec {

        fun acquire(): Int {
            return 1
        }

        fun release(): Int {
            return 2
        }
    }
}

[ndkoval]

Hi, @kevinly01, thanks for the issue. Lincheck does not support blocking operations for threads at the moment. We are going to fix it under #167. Thus, I'm closing the issue as a duplicate.